posSemidef_toMatrix_iff — Mathlib

English

A matrix A is positive semidefinite if and only if the corresponding linear map is positive.

Русский

Матрица A положительно полна тогда, когда соответствующее линейное отображение положительно.

LaTeX

$$$$A^{\text{PosSemidef}} \iff A^{-\text{toEuclideanLin}} \text{IsPositive}$$$$

Lean4

/-- `A.toMatrix` is positive semi-definite if and only if `A` is positive. -/
@[simp]
theorem posSemidef_toMatrix_iff {ι : Type*} [Fintype ι] [DecidableEq ι] {A : E →ₗ[𝕜] E} (b : OrthonormalBasis ι 𝕜 E) :
    (A.toMatrix b.toBasis b.toBasis).PosSemidef ↔ A.IsPositive := by
  rw [← Matrix.isPositive_toEuclideanLin_iff,
    (by exact Matrix.toLin'_toMatrix' _ :
      (A.toMatrix b.toBasis b.toBasis).toEuclideanLin = b.repr.toLinearMap ∘ₗ A ∘ₗ b.repr.symm.toLinearMap),
    isPositive_linearIsometryEquiv_conj_iff]

Похожие утверждения