Pythagorean Identity for the Concrete Affine Decomposition

This statement gives the Pythagorean identity for the concrete affine decomposition in $L^2$.

Let $n\in\mathbb N$, $E=$ EuclideanSpace ℝ (Fin n), and $(e_j)$ its standard orthonormal basis. Assume:

1. $\mu$ is a probability measure and $\operatorname{id}\in L^2(\mu)$.
2. $\int x\,d\mu(x)=0$.
3. For all $u,v\in E$, $\int\langle u,x\rangle\langle v,x\rangle\,d\mu(x)=\langle u,v\rangle$.
4. $f:E\to\mathbb R$ belongs to $L^2(\mu)$.

Write $c=\int f\,d\mu$, $a_j=\int\langle e_j,x\rangle f(x)\,d\mu(x)$, and $h(x)=f(x)-c-\sum_j a_j\langle e_j,x\rangle$, the residual L2.affineOrthPart μ f. Then

This separates the squared $L^2$ size into constant, linear, and residual contributions. All $L^2$ hypotheses are MemLp conditions, and all natural dimensions are included.

Original Lean declaration header

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

theorem integral_sq_eq_affine_decomposition (μ : Measure (EuclideanSpace ℝ (Fin n)))
    [IsProbabilityMeasure μ] (hμ2 : MemLp id 2 μ) (hμ0 : ∫ x, x ∂μ = 0)
    (hμcov : ∀ u v : EuclideanSpace ℝ (Fin n), ∫ x, ⟪u, x⟫ * ⟪v, x⟫ ∂μ = ⟪u, v⟫)
    {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : MemLp f 2 μ) :
    ∫ x, f x ^ 2 ∂μ =
      (∫ x, f x ∂μ) ^ 2 + ∑ j, (∫ x, ⟪EuclideanSpace.basisFun (Fin n) ℝ j, x⟫ * f x ∂μ) ^ 2 +
        ∫ x, affineOrthPart μ f x ^ 2 ∂μ

Module navigation

Module: L2/AffineDecomposition.

Supporting theorems: integral_affineOrthPart_mul_sub, integral_affine_sq, memLp_affineOrthPart.

Previous: integral_affine_sq.

Source excerpt, lines 938–944 · Frozen source 408915f.