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.

source

@[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 := ⋯ }

Instances For

source

theorem Matrix.le_iff {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] {A B : Matrix n n 𝕜} :

A ≤ B ↔ (B - A).PosSemidef

source

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

0 ≤ A ↔ A.PosSemidef

source

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.

source

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.

source

@[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 := ⋯ }

Instances For

source

theorem Matrix.instIsOrderedAddMonoid {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] :

IsOrderedAddMonoid (Matrix n n 𝕜)

source

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

NonnegSpectrumClass ℝ (Matrix n n 𝕜)

source

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

StarOrderedRing (Matrix n n 𝕜)

source

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⁻¹

source

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.

source

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

source

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

source

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‖

source

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}

source

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.

source

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

source

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.

source

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.

source

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

source

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

source

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.

source

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.

source

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

source

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

Instances For

source

@[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 α 𝕜

source

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

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

Documentation

Mathlib.Analysis.Matrix.Order

The partial order on matrices #

Main results #

Implementation notes #