Matrix algebras are star ordered rings

This file contains the instance of star_ordered_ring for matrix n n ℂ.

Main definitions

• matrix.partial_order: The partial order on matrix n n ℂ induced by the positive semidefinite matrices.
• matrix.pos_semidef.add_submonoid: The additive submonoid of positive semidefinite matrices.
• matrix.star_ordered_ring: The instance of star_ordered_ring for matrix n n ℂ.

You need to open_locale matrix_order to use these instances.

theorem Matrix.eq_zero_iff {n : Type u_1} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} : x = 0 ↔ ∀ (a : n → ℂ), star a ⬝ᵥ x.mulVec a = 0

@[reducible]

def Matrix.LE {n : Type u_1} [Fintype n] [DecidableEq n] : LE (Matrix n n ℂ)

Equations

• Matrix.LE = { le := fun (x y : Matrix n n ℂ) => (y - x).PosSemidef }

def Matrix.NegSemidef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] (x : Matrix n n 𝕜) : Prop

Equations

• x.NegSemidef = (x.IsHermitian ∧ ∀ (a : n → 𝕜), star a ⬝ᵥ x.mulVec a ≤ 0)

def Matrix.NegDef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] (x : Matrix n n 𝕜) : Prop

Equations

• x.NegDef = (x.IsHermitian ∧ ∀ (a : n → 𝕜), a ≠ 0 → star a ⬝ᵥ x.mulVec a < 0)

theorem Matrix.IsHermitian.neg_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] (x : Matrix n n 𝕜) : (-x).IsHermitian ↔ x.IsHermitian

theorem Matrix.negSemidef_iff_neg_posSemidef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] (x : Matrix n n 𝕜) : x.NegSemidef ↔ (-x).PosSemidef

theorem Matrix.negDef_iff_neg_posDef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] (x : Matrix n n 𝕜) : x.NegDef ↔ (-x).PosDef

theorem Matrix.NegDef.re_dotProduct_neg {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] {M : Matrix n n 𝕜} (hM : M.NegDef) {x : n → 𝕜} (hx : x ≠ 0) : RCLike.re (star x ⬝ᵥ M.mulVec x) < 0

theorem Matrix.NegSemidef.nonpos_eigenvalues {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.NegSemidef) (i : n) : ⋯.eigenvalues i ≤ 0

theorem Matrix.NegDef.neg_eigenvalues {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.NegDef) (i : n) : ⋯.eigenvalues i < 0

theorem Matrix.IsHermitian.eigenvalues_eq_zero_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.IsHermitian) : RCLike.ofReal ∘ hx.eigenvalues = 0 ↔ x = 0

theorem Matrix.posSemidef_and_negSemidef_iff_eq_zero {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosSemidef ∧ x.NegSemidef ↔ x = 0

theorem Matrix.not_posDef_and_negDef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] [Nonempty n] (x : Matrix n n 𝕜) : ¬(x.PosDef ∧ x.NegDef)

theorem Matrix.diagonal_posSemidef_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : n → 𝕜) : (diagonal x).PosSemidef ↔ 0 ≤ x

theorem Matrix.diagonal_negSemidef_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : n → 𝕜) : (diagonal x).NegSemidef ↔ x ≤ 0

theorem Matrix.diagonal_posDef_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : n → 𝕜) : (diagonal x).PosDef ↔ ∀ (i : n), 0 < x i

theorem Matrix.diagonal_negDef_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : n → 𝕜) : (diagonal x).NegDef ↔ ∀ (i : n), x i < 0

theorem Matrix.posSemidef_iff_of_isHermitian {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.IsHermitian) : x.PosSemidef ↔ 0 ≤ hx.eigenvalues

theorem Matrix.posSemidef_iff_isHermitian_and_nonneg_spectrum {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosSemidef ↔ x.IsHermitian ∧ spectrum 𝕜 (toLin' x) ⊆ {x : 𝕜 | 0 ≤ x}

theorem Matrix.posDef_iff_of_isHermitian {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.IsHermitian) : x.PosDef ↔ ∀ (i : n), 0 < hx.eigenvalues i

theorem Matrix.posDef_iff_isHermitian_and_pos_spectrum {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosDef ↔ x.IsHermitian ∧ spectrum 𝕜 (toLin' x) ⊆ {x : 𝕜 | 0 < x}

theorem Matrix.posSemidef_iff_commute {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x y : Matrix n n 𝕜} (hx : x.PosSemidef) (hy : y.PosSemidef) : Commute x y ↔ (x * y).PosSemidef

theorem Matrix.innerAut_negSemidef_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (U : ↥(unitaryGroup n 𝕜)) {a : Matrix n n 𝕜} : ((innerAut U) a).NegSemidef ↔ a.NegSemidef

theorem Matrix.innerAut_negDef_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (U : ↥(unitaryGroup n 𝕜)) {x : Matrix n n 𝕜} : ((innerAut U) x).NegDef ↔ x.NegDef

$f_U(x)$ is negative definite if and only if $x$ is negative definite

theorem Matrix.negSemidef_iff_of_isHermitian {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.IsHermitian) : x.NegSemidef ↔ hx.eigenvalues ≤ 0

theorem Matrix.negDef_iff_of_isHermitian {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.IsHermitian) : x.NegDef ↔ ∀ (i : n), hx.eigenvalues i < 0

theorem Matrix.posDef_of_posSemidef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.PosSemidef) : x.PosDef ↔ ∀ (i : n), ⋯.eigenvalues i ≠ 0

theorem Matrix.negDef_of_negSemidef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.NegSemidef) : x.NegDef ↔ ∀ (i : n), ⋯.eigenvalues i ≠ 0

@[reducible]

def Matrix.partialOrder {n : Type u_1} [Fintype n] [DecidableEq n] : PartialOrder (Matrix n n ℂ)

Equations

• Matrix.partialOrder = PartialOrder.mk ⋯

theorem Matrix.le_iff {n : Type u_1} [Fintype n] [DecidableEq n] {x y : Matrix n n ℂ} : x ≤ y ↔ (y - x).PosSemidef

@[reducible]

noncomputable def Matrix.starOrderedRing {n : Type u_1} [Fintype n] [DecidableEq n] : StarOrderedRing (Matrix n n ℂ)

Equations

• ⋯ = ⋯

theorem Matrix.Pi.le_iff_sub_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ι → Type u_2} [(i : ι) → Fintype (n i)] [(i : ι) → DecidableEq (n i)] (x y : PiMat ℂ ι n) : x ≤ y ↔ ∃ (z : PiMat ℂ ι n), y = x + star z * z

@[reducible]

noncomputable def Matrix.PiStarOrderedRing {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ι → Type u_2} [(i : ι) → Fintype (n i)] [(i : ι) → DecidableEq (n i)] : StarOrderedRing (PiMat ℂ ι n)

Equations

• ⋯ = ⋯

theorem Matrix.negSemidef_iff_nonpos {n : Type u_1} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) : x.NegSemidef ↔ x ≤ 0

theorem Matrix.PosSemidef.conj_by_isHermitian_posSemidef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x y : Matrix n n 𝕜} (hx : x.PosSemidef) (hy : y.IsHermitian) : (y * x * y).PosSemidef

theorem Matrix.IsHermitian.conj_by_isHermitian_posSemidef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x y : Matrix n n 𝕜} (hx : x.IsHermitian) (hy : y.PosSemidef) : (x * y * x).PosSemidef

theorem Matrix.isHermitian_mul_iff {α : Type u_1} {n : Type u_4} [NonUnitalSemiring α] [StarRing α] [Fintype n] {A B : Matrix n n α} (hA : A.IsHermitian) (hB : B.IsHermitian) : Commute A B ↔ (A * B).IsHermitian

Alias of Matrix.commute_iff.

theorem StarAlgEquiv.map_pow {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] [Star A₁] [Star A₂] (e : A₁ ≃⋆ₐ[R] A₂) (x : A₁) (n : ℕ) : e (x ^ n) = e x ^ n

theorem Matrix.innerAut.map_pow {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (U : ↥(unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) (n✝ : ℕ) : (innerAut U) x ^ n✝ = (innerAut U) (x ^ n✝)