gramSchmidtNormed_linearIndependent

English

If the family is pairwise orthogonal, the orthonormal basis vector equals a normalized original vector for that index.

Русский

Если система попарно ортогональна, то ортонормированный вектор базиса на индексе i равен нормализованной копии f_i.

LaTeX

$$$$ \text{If } \langle f_i, f_j \rangle = 0 \ (i\neq j) \text{ and } f_i \neq 0, \\ \mathrm{gramSchmidtOrthonormalBasis}(h,f)_i = \frac{1}{\|f_i\|} f_i. $$$$

Lean4

/-- `gramSchmidtNormed` produces linearly independent vectors when given linearly independent
vectors. -/
theorem gramSchmidtNormed_linearIndependent {f : ι → E} (h₀ : LinearIndependent 𝕜 f) :
    LinearIndependent 𝕜 (gramSchmidtNormed 𝕜 f) :=
  by
  unfold gramSchmidtNormed
  have (i : ι) : IsUnit (‖gramSchmidt 𝕜 f i‖⁻¹ : 𝕜) := isUnit_iff_ne_zero.mpr (by simp [gramSchmidt_ne_zero i h₀])
  let w : ι → 𝕜ˣ := fun i ↦ (this i).unit
  apply (gramSchmidt_linearIndependent h₀).units_smul (w := fun i ↦ (this i).unit)

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