@[implicit_reducible]

instance HermitianMat.instPartialOrder {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} : PartialOrder (HermitianMat n 𝕜)

The MatrixOrder instance for Matrix (the Loewner order) we keep open for HermitianMat, always.

Equations

• HermitianMat.instPartialOrder = { le := HermitianMat.instPartialOrder._aux_1, lt := HermitianMat.instPartialOrder._aux_3, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

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

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

theorem HermitianMat.zero_le_iff {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {A : HermitianMat n 𝕜} : 0 ≤ A ↔ (↑A).PosSemidef

theorem HermitianMat.le_iff_mulVec_le {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A B : HermitianMat n 𝕜} : A ≤ B ↔ ∀ (x : n → 𝕜), star x ⬝ᵥ (↑A).mulVec x ≤ star x ⬝ᵥ (↑B).mulVec x

instance HermitianMat.instZeroLEOneClass {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [DecidableEq n] : ZeroLEOneClass (HermitianMat n 𝕜)

theorem HermitianMat.lt_iff_posdef {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {A B : HermitianMat n 𝕜} : A < B ↔ (↑(B - A)).PosSemidef ∧ A ≠ B

instance HermitianMat.instIsStrictOrderedModuleReal {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} : IsStrictOrderedModule ℝ (HermitianMat n 𝕜)

theorem HermitianMat.posSemidef_iff_spectrum_Ici {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) : 0 ≤ A ↔ spectrum ℝ ↑A ⊆ Set.Ici 0

theorem HermitianMat.posSemidef_iff_spectrum_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A : HermitianMat n 𝕜) : 0 ≤ A ↔ ∀ x ∈ spectrum ℝ ↑A, 0 ≤ x

theorem HermitianMat.trace_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : HermitianMat n 𝕜} (hA : 0 ≤ A) : 0 ≤ A.trace

theorem HermitianMat.trace_pos {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : HermitianMat n 𝕜} (hA : 0 < A) : 0 < A.trace

def HermitianMat.evalHermitianMatTrace : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for HermitianMat.trace: nonneg when the matrix is nonneg, positive when the matrix is positive.

Equations

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

instance HermitianMat.instPosSMulMonoReal {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} : PosSMulMono ℝ (HermitianMat n 𝕜)

instance HermitianMat.instSMulPosMonoReal {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} : SMulPosMono ℝ (HermitianMat n 𝕜)

instance HermitianMat.instPosSMulReflectLEReal {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} : PosSMulReflectLE ℝ (HermitianMat n 𝕜)

theorem HermitianMat.le_trace_smul_one {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : HermitianMat n 𝕜} [DecidableEq n] (hA : 0 ≤ A) : A ≤ A.trace • 1

theorem HermitianMat.kronecker_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {m : Type u_3} [Fintype n] [Fintype m] {B : HermitianMat n 𝕜} {A : HermitianMat m 𝕜} (hA : 0 ≤ A) (hB : 0 ≤ B) : 0 ≤ A.kronecker B

The Kronecker product of two nonnegative Hermitian matrices is nonnegative.

theorem HermitianMat.kronecker_self_mono {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A B : HermitianMat n 𝕜} (hA : 0 ≤ A) (hB : 0 ≤ B) (hAB : A ≤ B) : A.kronecker A ≤ B.kronecker B

The self-Kronecker map A ↦ A ⊗ₖ A is monotone on nonnegative Hermitian matrices.

theorem HermitianMat.kronecker_pos {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {m : Type u_3} [Fintype n] [Fintype m] {B : HermitianMat n 𝕜} {A : HermitianMat m 𝕜} (hA : 0 < A) (hB : 0 < B) : 0 < A.kronecker B

The Kronecker product of two positive Hermitian matrices is positive.

theorem HermitianMat.posSemidef_to_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {A : Matrix n n 𝕜} (hA : A.PosSemidef) : 0 ≤ A

theorem HermitianMat.posDef_to_pos {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} (hA : A.PosDef) [Nonempty n] : 0 < A

partial def HermitianMat.findMatrixPSDInExpr (e p ty : Lean.Expr) : Lean.MetaM (Option (Bool × Lean.Expr))

Given an expression e (a matrix) and a proof expression p whose type may be Matrix.PosSemidef A, Matrix.PosDef A, or And P Q (syntactically), attempt to find a proof of nonnegativity or positivity for e. Only syntactic matching on the head constant is used; isDefEq is used only to compare the matrix argument.

def HermitianMat.evalMatrixPSD : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for Matrix: looks for A.PosSemidef or A.PosDef in the local context (including syntactic And conjunctions) to prove 0 ≤ A or 0 < A.

Equations

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

theorem HermitianMat.mat_posSemidef_to_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {A : HermitianMat n 𝕜} (hA : (↑A).PosSemidef) : 0 ≤ A

theorem HermitianMat.mat_posDef_to_pos {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : HermitianMat n 𝕜} [Nonempty n] (hA : (↑A).PosDef) : 0 < A

partial def HermitianMat.findHermitianMatPSDInExpr (e p ty : Lean.Expr) : Lean.MetaM (Option (Bool × Lean.Expr))

Given an expression e (a HermitianMat) and a proof expression p whose type may be Matrix.PosSemidef A.mat, Matrix.PosDef A.mat, or And P Q (syntactically), attempt to find a proof of nonnegativity or positivity for e. Only syntactic matching on the head constant is used; isDefEq is used only to compare the HermitianMat argument.

def HermitianMat.evalHermitianMatPSD : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for HermitianMat: looks for A.mat.PosSemidef or A.mat.PosDef in the local context (including syntactic And conjunctions) to prove 0 ≤ A or 0 < A.

Equations

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

def HermitianMat.evalHermitianMatKronecker : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for HermitianMat.kronecker: nonneg when both factors are.

Equations

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

theorem HermitianMat.conj_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {m : Type u_3} [Fintype n] [Fintype m] {A : HermitianMat n 𝕜} (M : Matrix m n 𝕜) (hA : 0 ≤ A) : 0 ≤ (conj M) A

Positivity extension for HermitianMat.conj: nonneg when the inner matrix is.

theorem HermitianMat.conj_pos {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {m : Type u_3} [Fintype n] [Fintype m] [DecidableEq n] {A : HermitianMat n 𝕜} {M : Matrix m n 𝕜} (hA : 0 < A) (h : (Matrix.toEuclideanLin M).ker ≤ A.ker) : 0 < (conj M) A

def HermitianMat.evalHermitianMatConj : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for HermitianMat.conj: nonneg when the inner matrix is.

Equations

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

theorem HermitianMat.convex_cone {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {A B : HermitianMat n 𝕜} (hA : 0 ≤ A) (hB : 0 ≤ B) {c₁ c₂ : ℝ} (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) : 0 ≤ c₁ • A + c₂ • B

theorem HermitianMat.sq_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : HermitianMat n 𝕜} [DecidableEq n] : 0 ≤ A ^ 2

theorem HermitianMat.ker_antitone {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A B : HermitianMat n 𝕜} [DecidableEq n] (hA : 0 ≤ A) : A ≤ B → B.ker ≤ A.ker

theorem HermitianMat.conj_mono {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {m : Type u_3} [Fintype n] [Fintype m] {A B : HermitianMat n 𝕜} {M : Matrix m n 𝕜} (h : A ≤ B) : (conj M) A ≤ (conj M) B

theorem HermitianMat.conj_posDef {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : HermitianMat n 𝕜} {N : Matrix n n 𝕜} [DecidableEq n] (hA : (↑A).PosDef) (hN : IsUnit N) : (↑((conj N) A)).PosDef

theorem HermitianMat.inv_conj {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : HermitianMat n 𝕜} [DecidableEq n] {M : Matrix n n 𝕜} (hM : IsUnit M) : ((conj M) A)⁻¹ = (conj M⁻¹.conjTranspose) A⁻¹

theorem HermitianMat.le_iff_mulVec_le_mulVec {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] (A B : HermitianMat n 𝕜) : A ≤ B ↔ ∀ (v : n → 𝕜), star v ⬝ᵥ (↑A).mulVec v ≤ star v ⬝ᵥ (↑B).mulVec v

theorem HermitianMat.inner_mulVec_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : HermitianMat n 𝕜} (hA : 0 ≤ A) (v : n → 𝕜) : 0 ≤ star v ⬝ᵥ (↑A).mulVec v

theorem HermitianMat.mem_ker_of_inner_mulVec_zero {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : HermitianMat n 𝕜} [DecidableEq n] (hA : 0 ≤ A) (v : EuclideanSpace 𝕜 n) (h : star v.ofLp ⬝ᵥ (↑A).mulVec v.ofLp = 0) : v ∈ A.ker

theorem HermitianMat.ker_add {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A B : HermitianMat n 𝕜} [DecidableEq n] (hA : 0 ≤ A) (hB : 0 ≤ B) : (A + B).ker = A.ker ⊓ B.ker

theorem HermitianMat.ker_sum {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {ι : Type u_4} [Fintype n] [Fintype ι] [DecidableEq n] (f : ι → HermitianMat n 𝕜) (hf : ∀ (i : ι), 0 ≤ f i) : (∑ i : ι, f i).ker = ⨅ (i : ι), (f i).ker

theorem HermitianMat.ker_conj {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : HermitianMat n 𝕜} [DecidableEq n] (hA : 0 ≤ A) (B : Matrix n n 𝕜) : ((conj B) A).ker = Submodule.comap (Matrix.toEuclideanLin B.conjTranspose) A.ker

theorem HermitianMat.ker_le_of_le_smul {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A B : HermitianMat n 𝕜} {α : ℝ} [DecidableEq n] (hα : α ≠ 0) (hA : 0 ≤ A) (hAB : A ≤ α • B) : B.ker ≤ A.ker

theorem HermitianMat.le_smul_one_imp_eigenvalues_le {n : Type u_2} [Fintype n] [DecidableEq n] (A : HermitianMat n ℂ) (M : ℝ) (h : A ≤ M • 1) (i : n) : ⋯.eigenvalues i ≤ M

If a Hermitian matrix is bounded by M * I, then all its eigenvalues are at most M.

theorem HermitianMat.eigenvalues_le_imp_le_smul_one {n : Type u_2} [Fintype n] [DecidableEq n] (A : HermitianMat n ℂ) (M : ℝ) (h : ∀ (i : n), ⋯.eigenvalues i ≤ M) : A ≤ M • 1

If all eigenvalues of a Hermitian matrix are at most M, then it is bounded by M * I.

Positivity extensions connecting HermitianMat and Matrix

theorem HermitianMat.eigenvalues_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : HermitianMat n 𝕜} [DecidableEq n] (hA : 0 ≤ A) (i : n) : 0 ≤ ⋯.eigenvalues i

If a HermitianMat is PSD, then its eigenvalues are nonneg.

theorem HermitianMat.mat_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {A : HermitianMat n 𝕜} (hA : 0 ≤ A) : 0 ≤ ↑A

If a HermitianMat is PSD, its underlying matrix is nonneg in the Loewner order.

theorem HermitianMat.mat_pos {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {A : HermitianMat n 𝕜} (hA : 0 < A) : 0 < ↑A

If a HermitianMat is positive, its underlying matrix is positive in the Loewner order.

theorem Matrix.nonneg_conjTranspose_mul_self {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {m : Type u_5} [Fintype m] (M : Matrix m n 𝕜) : 0 ≤ M.conjTranspose * M

Mᴴ * M is nonneg in the Loewner order, for any matrix M.

theorem Matrix.nonneg_self_mul_conjTranspose {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {m : Type u_5} [Fintype m] (M : Matrix n m 𝕜) : 0 ≤ M * M.conjTranspose

M * Mᴴ is nonneg in the Loewner order, for any matrix M.

theorem HermitianMat.subtype_mk_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_3} {M : Matrix m m 𝕜} (h : 0 ≤ M) : 0 ≤ ⟨M, ⋯⟩

theorem HermitianMat.subtype_mk_pos {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_3} {M : Matrix m m 𝕜} (h : 0 < M) : 0 < ⟨M, ⋯⟩

def HermitianMat.evalHermitianMatMat : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for A.mat where A : HermitianMat: nonneg when 0 ≤ A.

Equations

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

def HermitianMat.evalHermitianMatVal : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for A.mat where A : HermitianMat: nonneg when 0 ≤ A.

Equations

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

def HermitianMat.evalMatrixSelfMulConjTranspose : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for M * Mᴴ as a Matrix: always nonneg.

Equations

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

def HermitianMat.evalMatrixConjTransposeMulSelf : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for Mᴴ * M as a Matrix: always nonneg.

Equations

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

def HermitianMat.evalHermitianMatMk : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for ⟨M, (pf : M.IsHermitian)⟩ as a HermitianMat: equivalent to 0 ≤ M in MatrixOrder.

Equations

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

def HermitianMat.evalMatrixEigenvalues : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for eigenvalues of a Matrix: 0 ≤ (_ : M.IsHermitian).eigenvalues i. Will try to prove 0 ≤ M in the MatrixOrder. If the proof is A.H, i.e. M comes from a HermitianMat, this will give 0 ≤ A.mat which becomes 0 ≤ A later.

Equations

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