posDef_iff_eq_conjTranspose_mul_self

English

A matrix is positive definite iff it has the form B^H B with B invertible.

Русский

Матрица положительно определена тогда и только тогда, когда она имеет вид B^H B при некоторой обратимой B.

LaTeX

$$$\text{PosDef}(A) \iff \exists B:\ Matrix, IsUnit(B) \land A = B^H B$$$

Lean4

/-- A matrix is positive definite if and only if it has the form `Bᴴ * B` for some invertible `B`.
-/
theorem posDef_iff_eq_conjTranspose_mul_self [DecidableEq n] {A : Matrix n n 𝕜} :
    PosDef A ↔ ∃ B : Matrix n n 𝕜, IsUnit B ∧ A = Bᴴ * B :=
  by
  refine ⟨fun hA ↦ ⟨_, hA.posDef_sqrt.isUnit, ?_⟩, fun ⟨B, hB, hA⟩ ↦ (hA ▸ ?_)⟩
  · simp [hA.posDef_sqrt.isHermitian.eq, CFC.sqrt_mul_sqrt_self A hA.posSemidef.nonneg]
  · exact PosDef.conjTranspose_mul_self _ (mulVec_injective_of_isUnit hB)

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