Parseval Identity for Vector-Valued $L^2$ Components

This statement gives Parseval's identity in vector-valued $L^2$.

Let $(\alpha,\mu)$ be a measurable space with measure $\mu$, let $G$ be a real inner-product normed space, let $\iota$ be a finite index type, and let $b=(b_k)_{k\in\iota}$ be an orthonormal basis of $G$. For any $g\in L^2(\mu;G)$, take the scalar component $(x\mapsto\langle b_k,g(x)\rangle)$ for each basis vector. Then

This is the componentwise identity used to transfer scalar estimates to finite-dimensional vector-valued data.

Formalization Note: The components are represented by (innerSL ℝ (b k)).compLp g; the equality is in real $L^2$ and requires only a measurable space for the underlying measure.

Original Lean declaration header

Within namespace FunctionalInequalities.L2. Shown in its original module context. Proof omitted.

theorem sum_norm_sq_compLp_innerSL {μ : Measure α} {ι : Type*} [Fintype ι]
    (b : OrthonormalBasis ι ℝ G) (g : Lp G 2 μ) :
    ∑ k, ‖(innerSL ℝ (b k)).compLp g‖ ^ 2 = ‖g‖ ^ 2

Module navigation

Module: L2/Components.

Source excerpt, lines 60–62 · Frozen source 408915f.