Orthogonality of the Affine Residual to Linear Functions

This statement gives orthogonality of the designated affine residual to every linear function.

Let $n\in\mathbb N$, $E=$ EuclideanSpace ℝ (Fin n), and $(e_j)_{j\in\operatorname{Fin}(n)}$ 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. $g:E\to\mathbb R$ belongs to $L^2(\mu)$.

Set $h=$ L2.affineOrthPart μ g, explicitly

For every $u\in E$,

This is the linear orthogonality property of the affine decomposition under centered identity-covariance moment assumptions. The $L^2$ assumptions are MemLp conditions, and no restriction $n>0$ is imposed.

Original Lean declaration header

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

theorem integral_inner_mul_affineOrthPart (μ : 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⟫)
    {g : EuclideanSpace ℝ (Fin n) → ℝ} (hg : MemLp g 2 μ) (u : EuclideanSpace ℝ (Fin n)) :
    ∫ x, ⟪u, x⟫ * affineOrthPart μ g x ∂μ = 0

Module navigation

Module: L2/AffineDecomposition.

Previous: memLp_affineOrthPart · Next: sub_affineOrthPart_eq.

Source excerpt, lines 274–278 · Frozen source 408915f.