Square Integral of an Affine Function Under Isotropic Moment Conditions

This statement evaluates the square integral of an affine function under centered identity-covariance moment assumptions.

Let $n\in\mathbb N$, $E=$ EuclideanSpace ℝ (Fin n), and $e_j=$ EuclideanSpace.basisFun (Fin n) ℝ j. Assume:

1. $\mu$ is a probability measure and $\operatorname{id}\in L^2(\mu)$ (MemLp).
2. $\int x\,d\mu(x)=0$.
3. For every $u,v\in E$, $\int\langle u,x\rangle\langle v,x\rangle\,d\mu(x)=\langle u,v\rangle$.

For every $c\in\mathbb R$ and coefficient family $a:\operatorname{Fin}(n)\to\mathbb R$,

This identifies the $L^2$ square of the affine part with the Euclidean square of its coefficients. No log-concavity or positive-dimension assumption is needed.

Original Lean declaration header

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

theorem integral_affine_sq (μ : 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⟫)
    (c : ℝ) (a : Fin n → ℝ) :
    ∫ x, (c + ∑ j, a j * ⟪EuclideanSpace.basisFun (Fin n) ℝ j, x⟫) ^ 2 ∂μ =
      c ^ 2 + ∑ j, a j ^ 2

Module navigation

Module: L2/AffineDecomposition.

Previous: integral_affineOrthPart_sq_le · Next: integral_sq_eq_affine_decomposition.

Source excerpt, lines 881–886 · Frozen source 408915f.