gramSchmidtOrthonormalBasis_det — Mathlib

English

In the Gram-Schmidt construction, the determinant of the coefficient matrix of the vectors f with respect to the orthonormal basis equals the product of the inner products ⟪g_i, f_i⟫ over all indices i.

Русский

При построении по Грамму–Шмидту детерминант матрицы коэффициентов вектора f по ортонормированной базе равен произведению скалярных произведений ⟪g_i, f_i⟫ по всем индексам i.

LaTeX

$$$\det(\mathrm{toBasis}.det f) = \prod_i \langle g_i, f_i \rangle,$ where $g_i$ are the Gram-Schmidt basis vectors.$$

Lean4

theorem gramSchmidtOrthonormalBasis_det [DecidableEq ι] :
    (gramSchmidtOrthonormalBasis h f).toBasis.det f = ∏ i, ⟪gramSchmidtOrthonormalBasis h f i, f i⟫ :=
  by
  convert Matrix.det_of_upperTriangular (gramSchmidtOrthonormalBasis_inv_blockTriangular h f)
  exact ((gramSchmidtOrthonormalBasis h f).repr_apply_apply (f _) _).symm

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