tsum_inner_mul_inner — Mathlib

English

The squared-norm pairing with basis vectors sums to the norm pairing with the vector.

Русский

Сумма пар в скалярном произведении по базе восстанавливает норму вектора.

LaTeX

$$$ \\sum_i ⟪x, b_i⟫ · ⟪b_i, y⟫ = ⟪x, y⟫ $$$

Lean4

protected theorem tsum_inner_mul_inner (b : HilbertBasis ι 𝕜 E) (x y : E) : ∑' i, ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪x, y⟫ :=
  (b.hasSum_inner_mul_inner x y).tsum_eq

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