English
Let E be a finite-dimensional inner product space and f an indexed family of vectors spanning E. If we form the Gram-Schmidt orthonormal basis from f, the matrix that encodes the coefficients of f in this basis is upper triangular.
Русский
Пусть E — конечномерное вложенное векторное пространство с скалярным произведением, и f — заданная относительно индекса семейство векторов, порождающее E. При построении ортонормированной базы по Граму–Шмидту из f матрица коэффициентов в этой базе является верхне-треугольной.
LaTeX
$$$M = ((\mathrm{gramSchmidtOrthonormalBasis}(h,f)).toBasis)^{\}26812 M @ M$ is upper triangular, i.e. $M_{ij}=0$ for all $i>j$.$$
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`, the matrix of coefficients of `f` with respect to the
orthonormal basis `gramSchmidtOrthonormalBasis` constructed from `f` is upper-triangular. -/
theorem gramSchmidtOrthonormalBasis_inv_blockTriangular :
((gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f).BlockTriangular id := fun _ _ =>
gramSchmidtOrthonormalBasis_inv_triangular' h f
