orthonormal — Mathlib

English

The representation map has a representation of sums as ⟪x, b_i⟫·b_i converging to x.

Русский

Представление имеет вид сумму скалярных произведений, сходящихся к x.

LaTeX

$$$ HasSum (\\lambda i, ⟪x, b_i⟫ · b_i) x $$$

Lean4

@[simp]
protected theorem orthonormal (b : HilbertBasis ι 𝕜 E) : Orthonormal 𝕜 b := by
  classical
  rw [orthonormal_iff_ite]
  intro i j
  rw [← b.repr.inner_map_map (b i) (b j), b.repr_self, b.repr_self, lp.inner_single_left, lp.single_apply,
    Pi.single_apply]
  simp

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