gramSchmidt_def' — Mathlib

English

A refinement of the Gram-Schmidt definition; expresses f(n) equals gramSchmidt plus a sum of star-projections applied to f(n).

Русский

Уточнение определения Грамм-Schmidt: f(n) равно gramSchmidt(f)(n) плюс сумма, включающая starProjection(f(n)).

LaTeX

$$$ f(n) = \mathrm{gramSchmidt}_{\mathbb{K}}(f)(n) + \sum_{i \in Iio(n)} (\mathbb{K} \cdot \mathrm{gramSchmidt}_{\mathbb{K}}(f,i)).starProjection (f(n)) $$$

Lean4

theorem gramSchmidt_def' (f : ι → E) (n : ι) :
    f n = gramSchmidt 𝕜 f n + ∑ i ∈ Iio n, (𝕜 ∙ gramSchmidt 𝕜 f i).starProjection (f n) := by
  rw [gramSchmidt_def, sub_add_cancel]

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