The partial order on matrices

This file constructs the partial order and star ordered instances on matrices on 𝕜. This allows us to use more general results from C⋆-algebras, like CFC.sqrt.

Main results

• Matrix.instPartialOrder: the partial order on matrices given by x ≤ y := (y - x).PosSemidef.
• Matrix.PosSemidef.dotProduct_mulVec_zero_iff: for a positive semi-definite matrix A, we have x⋆ A x = 0 iff A x = 0.
• Matrix.PosDef.matrixInnerProductSpace: the inner product on matrices induced by a positive definite matrix M: ⟪x, y⟫ = (y * M * xᴴ).trace.

Implementation notes

Note that the partial order instance is scoped to MatrixOrder. Please open scoped MatrixOrder to use this.

@[reducible, inline]

abbrev Matrix.instPreOrder {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] : Preorder (Matrix n n 𝕜)

The preorder on matrices given by A ≤ B := (B - A).PosSemidef.

Equations

• Matrix.instPreOrder = { le := fun (A B : Matrix n n 𝕜) => (B - A).PosSemidef, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Matrix.le_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] {A B : Matrix n n 𝕜} : A ≤ B ↔ (B - A).PosSemidef

theorem Matrix.nonneg_iff_posSemidef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] {A : Matrix n n 𝕜} : 0 ≤ A ↔ A.PosSemidef

theorem Matrix.LE.le.posSemidef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] {A : Matrix n n 𝕜} : 0 ≤ A → A.PosSemidef

Alias of the forward direction of Matrix.nonneg_iff_posSemidef.

theorem Matrix.PosSemidef.nonneg {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] {A : Matrix n n 𝕜} : A.PosSemidef → 0 ≤ A

Alias of the reverse direction of Matrix.nonneg_iff_posSemidef.

@[reducible, inline]

abbrev Matrix.instPartialOrder {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] : PartialOrder (Matrix n n 𝕜)

The partial order on matrices given by A ≤ B := (B - A).PosSemidef.

Equations

• Matrix.instPartialOrder = { toPreorder := Matrix.instPreOrder, le_antisymm := ⋯ }

theorem Matrix.instIsOrderedAddMonoid {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] : IsOrderedAddMonoid (Matrix n n 𝕜)

theorem Matrix.instNonnegSpectrumClass {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] : NonnegSpectrumClass ℝ (Matrix n n 𝕜)

theorem Matrix.instStarOrderedRing {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] : StarOrderedRing (Matrix n n 𝕜)

@[deprecated CFC.sqrt (since := "2025-09-22")]

noncomputable def Matrix.PosSemidef.sqrt {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) : Matrix n n 𝕜

The positive semidefinite square root of a positive semidefinite matrix

Equations

• hA.sqrt = ↑⋯.eigenvectorUnitary * Matrix.diagonal (RCLike.ofReal ∘ (fun (x : ℝ) => √x) ∘ ⋯.eigenvalues) * star ↑⋯.eigenvectorUnitary

@[deprecated CFC.sqrt_nonneg (since := "2025-09-22")]

theorem Matrix.PosSemidef.posSemidef_sqrt {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} : (CFC.sqrt A).PosSemidef

@[deprecated CFC.sq_sqrt (since := "2025-09-22")]

theorem Matrix.PosSemidef.sq_sqrt {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) : CFC.sqrt A ^ 2 = A

@[deprecated CFC.sqrt_mul_sqrt_self (since := "2025-09-22")]

theorem Matrix.PosSemidef.sqrt_mul_self {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) : CFC.sqrt A * CFC.sqrt A = A

@[deprecated CFC.sq_eq_sq_iff (since := "2025-09-24")]

theorem Matrix.PosSemidef.sq_eq_sq_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) {B : Matrix n n 𝕜} (hB : B.PosSemidef) : A ^ 2 = B ^ 2 ↔ A = B

@[deprecated CFC.sq_eq_sq_iff (since := "2025-09-24")]

theorem Matrix.PosSemidef.eq_of_sq_eq_sq {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a b : A) (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) : a ^ 2 = b ^ 2 → a = b

Alias of the forward direction of CFC.sq_eq_sq_iff.

@[deprecated CFC.sqrt_sq (since := "2025-09-22")]

theorem Matrix.PosSemidef.sqrt_sq {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) : CFC.sqrt (A ^ 2) = A

@[deprecated CFC.sqrt_eq_iff (since := "2025-09-23")]

theorem Matrix.PosSemidef.eq_sqrt_iff_sq_eq {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) {B : Matrix n n 𝕜} (hB : B.PosSemidef) : A = CFC.sqrt B ↔ A ^ 2 = B

@[deprecated CFC.sqrt_eq_iff (since := "2025-09-23")]

theorem Matrix.PosSemidef.sqrt_eq_iff_eq_sq {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) {B : Matrix n n 𝕜} (hB : B.PosSemidef) : CFC.sqrt A = B ↔ A = B ^ 2

@[deprecated CFC.sqrt_eq_zero_iff (since := "2025-09-22")]

theorem Matrix.PosSemidef.sqrt_eq_zero_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) : CFC.sqrt A = 0 ↔ A = 0

@[deprecated CFC.sqrt_eq_one_iff (since := "2025-09-23")]

theorem Matrix.PosSemidef.sqrt_eq_one_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) : CFC.sqrt A = 1 ↔ A = 1

@[deprecated CFC.isUnit_sqrt_iff (since := "2025-09-22")]

theorem Matrix.PosSemidef.isUnit_sqrt_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) : IsUnit (CFC.sqrt A) ↔ IsUnit A

theorem Matrix.PosSemidef.inv_sqrt {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) : (CFC.sqrt A)⁻¹ = CFC.sqrt A⁻¹

theorem Matrix.PosSemidef.dotProduct_mulVec_zero_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) (x : n → 𝕜) : star x ⬝ᵥ A.mulVec x = 0 ↔ A.mulVec x = 0

For A positive semidefinite, we have x⋆ A x = 0 iff A x = 0.

theorem Matrix.PosSemidef.toLinearMap₂'_zero_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) (x : n → 𝕜) : (((toLinearMap₂' 𝕜) A) (star x)) x = 0 ↔ A.mulVec x = 0

For A positive semidefinite, we have x⋆ A x = 0 iff A x = 0 (linear maps version).

@[deprecated CStarAlgebra.nonneg_iff_eq_star_mul_self (since := "2025-09-22")]

theorem Matrix.posSemidef_iff_eq_conjTranspose_mul_self {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] {A : Matrix n n 𝕜} : A.PosSemidef ↔ ∃ (B : Matrix n n 𝕜), A = B.conjTranspose * B

A matrix is positive semidefinite if and only if it has the form Bᴴ * B for some B.

@[deprecated CStarAlgebra.nonneg_iff_eq_star_mul_self (since := "2025-05-07")]

theorem Matrix.posSemidef_iff_eq_transpose_mul_self {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : 0 ≤ a ↔ ∃ (b : A), a = star b * b

Alias of CStarAlgebra.nonneg_iff_eq_star_mul_self.

theorem Matrix.posSemidef_iff_isHermitian_and_spectrum_nonneg {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} : A.PosSemidef ↔ A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}

@[deprecated commute_iff_mul_nonneg (since := "2025-09-23")]

theorem Matrix.PosSemidef.commute_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] {A B : Matrix n n 𝕜} (hA : A.PosSemidef) (hB : B.PosSemidef) : Commute A B ↔ (A * B).PosSemidef

theorem Matrix.PosSemidef.posDef_iff_isUnit {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.PosSemidef) : x.PosDef ↔ IsUnit x

A positive semi-definite matrix is positive definite if and only if it is invertible.

theorem Matrix.PosDef.commute_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] {A B : Matrix n n 𝕜} (hA : A.PosDef) (hB : B.PosDef) : Commute A B ↔ (A * B).PosDef

theorem Matrix.PosDef.posDef_sqrt {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : (CFC.sqrt M).PosDef

theorem Matrix.posDef_iff_eq_conjTranspose_mul_self {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} : A.PosDef ↔ ∃ (B : Matrix n n 𝕜), IsUnit B ∧ A = B.conjTranspose * B

A matrix is positive definite if and only if it has the form Bᴴ * B for some invertible B.

@[deprecated Matrix.posDef_iff_eq_conjTranspose_mul_self (since := "07-08-2025")]

theorem Matrix.PosDef.posDef_iff_eq_conjTranspose_mul_self {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} : A.PosDef ↔ ∃ (B : Matrix n n 𝕜), IsUnit B ∧ A = B.conjTranspose * B

Alias of Matrix.posDef_iff_eq_conjTranspose_mul_self.

---

A matrix is positive definite if and only if it has the form Bᴴ * B for some invertible B.

noncomputable def Matrix.PosDef.matrixNormedAddCommGroup {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] {M : Matrix n n 𝕜} (hM : M.PosDef) : NormedAddCommGroup (Matrix n n 𝕜)

A positive definite matrix M induces a norm on Matrix n n 𝕜: ‖x‖ = sqrt (x * M * xᴴ).trace.

Equations

• hM.matrixNormedAddCommGroup = InnerProductSpace.Core.toNormedAddCommGroup

def Matrix.PosDef.matrixInnerProductSpace {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] {M : Matrix n n 𝕜} (hM : M.PosDef) : InnerProductSpace 𝕜 (Matrix n n 𝕜)

A positive definite matrix M induces an inner product on Matrix n n 𝕜: ⟪x, y⟫ = (y * M * xᴴ).trace.

Equations

• One or more equations did not get rendered due to their size.