More results about positive definite and positive semidefinite matrices (see Mathlib.LinearAlgebra.Matrix.PosDef).

theorem Matrix.PosSemidef.det_nonneg {n : Type u_1} [Fintype n] {M : Matrix n n ℝ} (hM : M.PosSemidef) [DecidableEq n] : 0 ≤ M.det

theorem Matrix.PosDef.det_ne_zero {n : Type u_1} [Fintype n] {𝕜 : Type u_2} [NormedField 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] [RCLike 𝕜] [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : M.det ≠ 0

theorem Matrix.PosDef.isUnit_det {n : Type u_1} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : M.PosDef) : IsUnit M.det

noncomputable instance Matrix.PosDef.Invertible {n : Type u_1} [Fintype n] {𝕜 : Type u_2} [NormedField 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] [RCLike 𝕜] [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : Invertible M

Equations

• hM.Invertible = M.invertibleOfIsUnitDet ⋯

theorem Matrix.PosSemidef_diagonal {n : Type u_1} [Fintype n] [DecidableEq n] {f : n → ℝ} (hf : ∀ (i : n), 0 ≤ f i) : (Matrix.diagonal f).PosSemidef

theorem Matrix.PosDef_diagonal {n : Type u_1} [Fintype n] [DecidableEq n] {f : n → ℝ} (hf : ∀ (i : n), 0 < f i) : (Matrix.diagonal f).PosDef

theorem Matrix.PosSemidef.conjTranspose_mul_mul {n : Type u_1} [Fintype n] {𝕜 : Type u_2} [NormedField 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] (M : Matrix n n 𝕜) (N : Matrix n n 𝕜) (hM : M.PosSemidef) : (N.conjTranspose * M * N).PosSemidef

theorem Matrix.PosDef.conjTranspose_mul_mul {n : Type u_1} [Fintype n] {𝕜 : Type u_2} [NormedField 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] [DecidableEq n] (M : Matrix n n 𝕜) (N : Matrix n n 𝕜) (hM : M.PosDef) (hN : N.det ≠ 0) : (N.conjTranspose * M * N).PosDef

theorem Matrix.IsHermitian.nonsingular_inv {n : Type u_1} [Fintype n] {𝕜 : Type u_2} [NormedField 𝕜] [StarRing 𝕜] [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.IsHermitian) (hMdet : IsUnit M.det) : M⁻¹.IsHermitian

theorem Matrix.conj_symm {n : Type u_1} [Fintype n] {𝕜 : Type u_2} [NormedField 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] {x : n → 𝕜} {M : Matrix n n 𝕜} (hM : M.IsHermitian) : star (Matrix.dotProduct (star x) (M.mulVec x)) = Matrix.dotProduct (star x) (M.mulVec x)

theorem Matrix.PosDef.nonsingular_inv {n : Type u_1} [Fintype n] {𝕜 : Type u_2} [NormedField 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] [RCLike 𝕜] [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : M⁻¹.PosDef

theorem Matrix.PosSemidef.mul_mul_of_IsHermitian {n : Type u_1} [Fintype n] {𝕜 : Type u_2} [NormedField 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] {M : Matrix n n 𝕜} {N : Matrix n n 𝕜} (hM : M.PosSemidef) (hN : N.IsHermitian) : (N * M * N).PosSemidef

theorem Matrix.PosSemidef.add {n : Type u_1} [Fintype n] {𝕜 : Type u_2} [NormedField 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] {M : Matrix n n 𝕜} {N : Matrix n n 𝕜} (hM : M.PosSemidef) (hN : N.PosSemidef) : (M + N).PosSemidef

theorem Matrix.isUnit_det_of_PosDef_inv {n : Type u_1} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (h : M⁻¹.PosDef) : IsUnit M.det

theorem Matrix.PosDef_inv_iff_PosDef {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℝ) : M⁻¹.PosDef ↔ M.PosDef

theorem Matrix.PosSemiDef.IsSymm {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.PosSemidef) : A.IsSymm