Zero Mean of the Affine Residual Under a Centered Law

Proved

FunctionalInequalities.L2.integral_affineOrthPart_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement shows that the designated affine residual is centered under a centered probability measure.

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

$\mu$ is a probability measure on $E$ , with $\operatorname{id}\in L^2(\mu)$ .
$\int x\,d\mu(x)=0$ .
$g:E\to\mathbb R$ belongs to $L^2(\mu)$ .

Define the residual L2.affineOrthPart by

h(x)=g(x)-\int g\,d\mu-\sum_{j\in\operatorname{Fin}(n)}\left(\int\langle e_j,y\rangle g(y)\,d\mu(y)\right)\langle e_j,x\rangle.

Then

\int h\,d\mu=0.

This supplies the centering property of the concrete affine decomposition. Identity covariance is not required for this conclusion, and $n=0$ is included.

Formalization Note The $L^2$ hypotheses are MemLp hypotheses, including almost-everywhere strong measurability.

Original Lean declaration header

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

theorem integral_affineOrthPart (μ : Measure (EuclideanSpace ℝ (Fin n))) [IsProbabilityMeasure μ]
    (hμ2 : MemLp id 2 μ) (hμ0 : ∫ x, x ∂μ = 0) {g : EuclideanSpace ℝ (Fin n) → ℝ}
    (hg : MemLp g 2 μ) :
    ∫ x, affineOrthPart μ g x ∂μ = 0

Module navigation

Module: L2/AffineDecomposition.

Previous: eLpNorm_le_eLpNorm_of_integral_sq_le · Next: memLp_affineOrthPart.

Source excerpt, lines 185–188 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_L2_AffineDecomposition

open MeasureTheory
variable {n : ℕ}

Formal statement


theorem FunctionalInequalities.L2.integral_affineOrthPart_readable (μ : Measure (EuclideanSpace ℝ (Fin n))) [IsProbabilityMeasure μ]
    (hμ2 : MemLp id 2 μ) (hμ0 : ∫ x, x ∂μ = 0) {g : EuclideanSpace ℝ (Fin n) → ℝ}
    (hg : MemLp g 2 μ) :
    ∫ x, affineOrthPart μ g x ∂μ = 0 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/L2/AffineDecomposition.lean#L184-L242 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.L2.AffineDecomposition`, declaration `FunctionalInequalities.L2.integral_affineOrthPart`; the repository is private at upload time).

View graph