sum_inner_mul_inner — Mathlib

English

For an orthonormal basis b = (b_i) of E and any x, y ∈ E, the inner product is given by the Parseval sum: ∑_i ⟪x, b_i⟫ ⟪b_i, y⟫ = ⟪x, y⟫.

Русский

Для ортонормированного базиса b = (b_i) и любых x, y ∈ E выполняется тождество Парсеваля: ∑_i ⟪x, b_i⟫ ⟪b_i, y⟫ = ⟪x, y⟫.

LaTeX

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

Lean4

protected theorem sum_inner_mul_inner (b : OrthonormalBasis ι 𝕜 E) (x y : E) : ∑ i, ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪x, y⟫ :=
  by
  have := congr_arg (innerSL 𝕜 x) (b.sum_repr y)
  rw [map_sum] at this
  convert this
  rw [map_smul, b.repr_apply_apply, mul_comm]
  simp

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