Documentation

LeanPool.Monlib4.LinearAlgebra.Matrix.StarOrderedRing

Matrix algebras as star ordered rings #

This file keeps the upstream monlib4 API around matrix positivity and the MatrixOrder scoped order. Current Mathlib supplies the underlying matrix order and StarOrderedRing instance, so this file restores the Monlib-facing negative definiteness definitions, spectral criteria, and compatibility names.

theorem Matrix.eq_zero_iff {n : Type u_1} [Fintype n] {x : Matrix n n ℂ} :

x = 0 ↔ ∀ (a : n → ℂ), star a ⬝ᵥ x.mulVec a = 0

@[reducible]

def Matrix.LE {n : Type u_1} :

LE (Matrix n n ℂ)

The upstream Monlib order relation, now supplied by Mathlib under MatrixOrder.

Equations

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

Instances For

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

A matrix is negative semidefinite when its Hermitian quadratic form is nonpositive.

Equations

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

Instances For

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

A matrix is negative definite when its quadratic form is negative on nonzero inputs.

Equations

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

Instances For

theorem Matrix.IsHermitian.neg_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] (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.posSemidef_and_negSemidef_iff_eq_zero {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype 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] [Nonempty n] (x : Matrix n n 𝕜) :

¬(x.PosDef ∧ x.NegDef)

theorem Matrix.diagonal_posSemidef_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [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 𝕜] [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] {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]

noncomputable def Matrix.partialOrder {n : Type u_1} :

PartialOrder (Matrix n n ℂ)

The matrix partial order induced by positive semidefinite differences.

Equations

Matrix.partialOrder = inferInstance

Instances For

theorem Matrix.starOrderedRing {n : Type u_1} [Fintype n] :

StarOrderedRing (Matrix n n ℂ)

theorem Matrix.Pi.le_iff_sub_nonneg {ι : Type u_1} {n : ι → Type u_2} [(i : ι) → Fintype (n i)] (x y : PiMat ℂ ι n) :

x ≤ y ↔ ∃ (z : PiMat ℂ ι n), y = x + star z * z

theorem Matrix.PiStarOrderedRing {ι : Type u_1} {n : ι → Type u_2} [(i : ι) → Fintype (n i)] :

StarOrderedRing (PiMat ℂ ι n)

theorem Matrix.negSemidef_iff_nonpos {n : Type u_1} [Fintype 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] {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] {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.

Alias of Matrix.IsHermitian.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✝)