orthogonalProjection_eq_sum — Mathlib

English

The orthonormal basis induces a coordinate-wise representation on vector spaces via Pi, and applying the basis to a point behaves as expected on coordinates.

Русский

Ортонормированный базис задаёт координатное представление через Π, и применение базиса к вектору совпадает с ожидаемым преобразованием координат.

LaTeX

$$$\text{Pi.orthonormalBasis_apply}$$$

Lean4

protected theorem orthogonalProjection_eq_sum {U : Submodule 𝕜 E} [CompleteSpace U] (b : OrthonormalBasis ι 𝕜 U)
    (x : E) : U.orthogonalProjection x = ∑ i, ⟪(b i : E), x⟫ • b i := by
  simpa only [b.repr_apply_apply, inner_orthogonalProjection_eq_of_mem_left] using
    (b.sum_repr (U.orthogonalProjection x)).symm

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