gramSchmidtOrthonormalBasis — Mathlib

English

If gramSchmidtNormed i = 0, then the inner product with any f_j is zero for all j.

Русский

Если gramSchmidtNormed i = 0, то скалярное произведение с любым f_j равно нулю.

LaTeX

$$$$ \langle \mathrm{gramSchmidtOrthonormalBasis}(h,f)_i, f_j \rangle = 0 \quad \text{whenever } \mathrm{gramSchmidtNormed}_{\mathbb{K}} f(i) = 0.$$$$

Lean4

/-- Given an indexed family `f : ι → E` of vectors in an inner product space `E`, for which the
size of the index set is the dimension of `E`, produce an orthonormal basis for `E` which agrees
with the orthonormal set produced by the Gram-Schmidt orthonormalization process on the elements of
`ι` for which this process gives a nonzero number. -/
noncomputable def gramSchmidtOrthonormalBasis : OrthonormalBasis ι 𝕜 E :=
  ((gramSchmidtNormed_orthonormal' f).exists_orthonormalBasis_extension_of_card_eq (v := gramSchmidtNormed 𝕜 f)
      h).choose

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