gramSchmidt_def'' — Mathlib

English

A formula for f(n) using inner products and normalization terms; expresses f(n) as a combination of Gram-Schmidt vectors with normalized projections.

Русский

Формула для f(n) через скалярные проекции и нормализации; выражает f(n) как линейную комбинацию ортогональных векторов с нормализованными проекциями.

LaTeX

$$$ f(n) = \mathrm{gramSchmidt}_{\mathbb{K}}(f)(n) + \sum_{i \in Iio(n)} \frac{\langle \mathrm{gramSchmidt}_{\mathbb{K}}(f,i), f(n) \rangle}{\|\mathrm{gramSchmidt}_{\mathbb{K}}(f,i)\|^{2}} \; \mathrm{gramSchmidt}_{\mathbb{K}}(f,i) $$$

Lean4

theorem gramSchmidt_def'' (f : ι → E) (n : ι) :
    f n =
      gramSchmidt 𝕜 f n + ∑ i ∈ Iio n, (⟪gramSchmidt 𝕜 f i, f n⟫ / (‖gramSchmidt 𝕜 f i‖ : 𝕜) ^ 2) • gramSchmidt 𝕜 f i :=
  by simp only [← map_pow, ← starProjection_singleton, ← gramSchmidt_def' 𝕜 f n]

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