gramSchmidt — Mathlib

English

The Gram-Schmidt process takes a family of vectors and outputs an orthogonal family spanning the same subspace.

Русский

Процесс Грамма-Шмидта принимает множество векторов и выдаёт ортогональное множество, порождающее ту же самую подобласть.

LaTeX

$$$ \text{GramSchmidt}_{\mathbb{K}}(f) \text{ is an orthogonal system with } \mathrm{span}(f) = \mathrm{span}(\mathrm{GramSchmidt}_{\mathbb{K}}(f)) $$$

Lean4

/-- The Gram-Schmidt process takes a set of vectors as input
and outputs a set of orthogonal vectors which have the same span. -/
noncomputable def gramSchmidt [WellFoundedLT ι] (f : ι → E) (n : ι) : E :=
  f n - ∑ i : Iio n, (𝕜 ∙ gramSchmidt f i).starProjection (f n)
termination_by n
decreasing_by exact mem_Iio.1 i.2

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