posDef_gram_of_linearIndependent — Mathlib

English

If the vectors v_i are linearly independent, then the Gram matrix Gram 𝕜 v is positive definite.

Русский

Если векторы v_i линейно независимы, то граммова матрица 𝕜 v положительно определена.

LaTeX

$$$ \text{LinearIndependent } 𝕜 v \Rightarrow \text{PosDef }( \text{gram } 𝕜 v ) $$$

Lean4

/-- In a normed space, linear independence of `v` implies positive definiteness of `gram 𝕜 v`. -/
theorem posDef_gram_of_linearIndependent {v : n → E} (h_li : LinearIndependent 𝕜 v) : PosDef (gram 𝕜 v) :=
  by
  rw [Fintype.linearIndependent_iff] at h_li
  obtain ⟨h0, h1⟩ := posSemidef_gram 𝕜 v
  refine ⟨h0, fun x hx ↦ (h1 x).lt_of_ne' ?_⟩
  rw [star_dotProduct_gram_mulVec, inner_self_eq_zero.ne]
  exact mt (h_li x) (mt funext hx)

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