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.

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.

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

theorem Matrix.posSemidef_is_closed {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] : IsClosed {A : Matrix n n 𝕜 | A.PosSemidef}

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

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

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}

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

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.PosSemidef.posDef_iff_det_ne_zero {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) : A.PosDef ↔ A.det ≠ 0

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.

theorem Matrix.PosSemidef.hadamard {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_3} {A B : Matrix ι ι 𝕜} (hA : A.PosSemidef) (hB : B.PosSemidef) : (A.hadamard B).PosSemidef

[Schur product theorem][schur1911] (positive semidefinite version): the Hadamard (entrywise) product of positive semidefinite matrices is positive semidefinite.

theorem Matrix.PosDef.hadamard {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_3} {A B : Matrix ι ι 𝕜} (hA : A.PosDef) (hB : B.PosDef) : (A.hadamard B).PosDef

Schur product theorem: the Hadamard (entrywise) product of positive definite matrices is positive definite.

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.

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

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

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

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

instance Matrix.instIsometricContinuousFunctionalCalculus {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] : IsometricContinuousFunctionalCalculus ℝ (Matrix n n 𝕜) IsSelfAdjoint

The isometric continuous functional calculus on Matrix n n 𝕜 arising from the operator norm given by the identification with (continuous) linear endomorphisms of EuclideanSpace 𝕜 n.