Parseval's identity in norm-square form

Mathlib states Parseval's identity in polarized, 𝕜-valued form: HilbertBasis.hasSum_inner_mul_inner gives ∑' i, ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪x, y⟫. This file states the diagonal, real-valued form ‖x‖² = ∑' i, ‖⟪b i, x⟫‖². The two differ in the type of their summands, so the real-valued form is not a substitution instance of the polarized one.

The real-valued form is the shape consumers state coefficient decay in, and it is the OrthogonalL2Bases roadmap's Part A3 acceptance criterion ‖f‖² = ∑' n, ‖⟪ψₙ, f⟫‖²; its instance for the Hermite basis is TauCeti.tsum_norm_sq_inner_hermiteFunctionLp.

Main declarations

• HilbertBasis.hasSum_norm_sq_inner — Parseval in norm-square form, as a HasSum statement.
• HilbertBasis.tsum_norm_sq_inner — the same identity as an equation between a tsum and ‖x‖².

theorem HilbertBasis.hasSum_norm_sq_inner {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (x : E) : HasSum (fun (i : ι) => ‖inner 𝕜 (b i) x‖ ^ 2) (‖x‖ ^ 2)

Parseval's identity, norm-square form. The squared coordinates of x in a Hilbert basis sum to ‖x‖², as a convergent series of real numbers.

theorem HilbertBasis.tsum_norm_sq_inner {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (x : E) : ∑' (i : ι), ‖inner 𝕜 (b i) x‖ ^ 2 = ‖x‖ ^ 2

Parseval's identity, norm-square form (tsum version of HilbertBasis.hasSum_norm_sq_inner).

theorem HilbertBasis.summable_norm_sq_inner {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (x : E) : Summable fun (i : ι) => ‖inner 𝕜 (b i) x‖ ^ 2

The squared coordinate family of a vector is summable.