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 = inferInstanceAs (PartialOrder ↥(selfAdjoint (Matrix n n 𝕜)))

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

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

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

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.