posSemidef_gram — Mathlib

English

The Gram matrix of any finite family is positive semidefinite.

Русский

Граммова матрица конечного набора векторов всегда положительно полуположна.

LaTeX

$$$ \text{PosSemidef }( \text{gram } 𝕜 v )$$$

Lean4

/-- A Gram matrix is positive semidefinite. -/
theorem posSemidef_gram (v : n → E) : PosSemidef (gram 𝕜 v) :=
  by
  refine ⟨isHermitian_gram _ _, fun x ↦ ?_⟩
  rw [star_dotProduct_gram_mulVec, le_iff_re_im]
  simp [inner_self_nonneg]

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