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.toMatrixInnerProductSpace: the inner product on matrices induced by a positive semi-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 𝕜] : 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 𝕜] {A B : Matrix n n 𝕜} : A ≤ B ↔ (B - A).PosSemidef

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

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

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

theorem Matrix.IsHermitian.det_abs {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : (CFC.abs A).det = ↑‖A.det‖

@[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.

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.isStrictlyPositive_iff_posDef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : IsStrictlyPositive x ↔ x.PosDef

theorem Matrix.IsStrictlyPositive.posDef {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : IsStrictlyPositive x → x.PosDef

Alias of the forward direction of Matrix.isStrictlyPositive_iff_posDef.

theorem Matrix.PosDef.isStrictlyPositive {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosDef → IsStrictlyPositive x

Alias of the reverse direction of Matrix.isStrictlyPositive_iff_posDef.

@[deprecated IsStrictlyPositive.commute_iff (since := "2025-09-26")]

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

@[deprecated IsStrictlyPositive.sqrt (since := "2025-09-26")]

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.PosSemidef.kronecker {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Finite n] {m : Type u_3} [Finite m] {x : Matrix n n 𝕜} {y : Matrix m m 𝕜} (hx : x.PosSemidef) (hy : y.PosSemidef) : (kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) x y).PosSemidef

The kronecker product of two positive semi-definite matrices is positive semi-definite.

theorem Matrix.PosDef.kronecker {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Finite n] {m : Type u_3} [Finite m] {x : Matrix n n 𝕜} {y : Matrix m m 𝕜} (hx : x.PosDef) (hy : y.PosDef) : (kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) x y).PosDef

The kronecker of two positive definite matrices is positive definite.

@[deprecated CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self (since := "2025-09-28")]

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.

def Matrix.tracePositiveLinearMap (n : Type u_3) (α : Type u_4) (𝕜 : Type u_5) [Fintype n] [Semiring α] [RCLike 𝕜] [Module α 𝕜] : Matrix n n 𝕜 →ₚ[α] 𝕜

Matrix.trace as a positive linear map.

Equations

• Matrix.tracePositiveLinearMap n α 𝕜 = PositiveLinearMap.mk₀ (Matrix.traceLinearMap n α 𝕜) ⋯

@[simp]

theorem Matrix.toLinearMap_tracePositiveLinearMap (n : Type u_3) (α : Type u_4) (𝕜 : Type u_5) [Fintype n] [Semiring α] [RCLike 𝕜] [Module α 𝕜] : (tracePositiveLinearMap n α 𝕜).toLinearMap = traceLinearMap n α 𝕜

@[simp]

theorem Matrix.tracePositiveLinearMap_apply (n : Type u_3) (α : Type u_4) (𝕜 : Type u_5) [Fintype n] [Semiring α] [RCLike 𝕜] [Module α 𝕜] (x : Matrix n n 𝕜) : (tracePositiveLinearMap n α 𝕜) x = x.trace

@[implicit_reducible]

noncomputable def Matrix.toMatrixSeminormedAddCommGroup {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] (M : Matrix n n 𝕜) (hM : M.PosSemidef) : SeminormedAddCommGroup (Matrix n n 𝕜)

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

Equations

• M.toMatrixSeminormedAddCommGroup hM = InnerProductSpace.Core.toSeminormedAddCommGroup

@[implicit_reducible]

noncomputable def Matrix.toMatrixNormedAddCommGroup {𝕜 : 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

• M.toMatrixNormedAddCommGroup hM = InnerProductSpace.Core.toNormedAddCommGroup

@[implicit_reducible]

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

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

Equations

• M.toMatrixInnerProductSpace hM = InnerProductSpace.ofCore (Matrix.PosSemidef.matrixPreInnerProductSpace✝ hM)

@[deprecated Matrix.toMatrixNormedAddCommGroup (since := "2025-11-18")]

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 𝕜)

Alias of Matrix.toMatrixNormedAddCommGroup.

---

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

Equations

• @Matrix.PosDef.matrixNormedAddCommGroup = @Matrix.toMatrixNormedAddCommGroup

@[deprecated Matrix.toMatrixInnerProductSpace (since := "2025-11-12")]

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

Alias of Matrix.toMatrixInnerProductSpace.

---

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

Equations

• @Matrix.PosDef.matrixInnerProductSpace = @Matrix.toMatrixInnerProductSpace