sum_sq_inner_right — Mathlib

English

Specialization of Parseval to the real inner product: ∑_i ‖⟪b_i, x⟫‖^2 = ‖x‖^2 for a real inner product space.

Русский

Специализация Парсеваля для вещественного скалярного произведения: ∑_i ‖⟪b_i, x⟫‖^2 = ‖x‖^2.

LaTeX

$$$\sum_i \|\langle b_i, x \rangle\|^2 = \|x\|^2$$$

Lean4

theorem sum_sq_inner_right {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : OrthonormalBasis ι ℝ E)
    (x : E) : ∑ i : ι, ⟪b i, x⟫ ^ 2 = ‖x‖ ^ 2 :=
  by
  rw [← b.sum_sq_norm_inner_right]
  simp

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