Square Integrability of the Affine Residual

Proved

FunctionalInequalities.L2.memLp_affineOrthPart_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement asserts square integrability of the designated affine residual.

Let $n\in\mathbb N$ , $E=$ EuclideanSpace ℝ (Fin n), and $(e_j)$ its standard orthonormal basis. Let $\mu$ be a probability measure on $E$ with $\operatorname{id}\in L^2(\mu)$ , and let $g:E\to\mathbb R$ belong to $L^2(\mu)$ . Define $h=$ L2.affineOrthPart μ g 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

h\in L^2(\mu).

This makes the residual available as an $L^2$ function in subsequent decomposition identities. No centering or identity-covariance assumption is required.

Formalization Note Membership is expressed by MemLp, including almost-everywhere strong measurability. All natural dimensions, including zero, are allowed.

Original Lean declaration header

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

theorem memLp_affineOrthPart (μ : Measure (EuclideanSpace ℝ (Fin n))) [IsProbabilityMeasure μ]
    (hμ2 : MemLp id 2 μ) {g : EuclideanSpace ℝ (Fin n) → ℝ} (hg : MemLp g 2 μ) :
    MemLp (affineOrthPart μ g) 2 μ

Module navigation

Module: L2/AffineDecomposition.

Previous: integral_affineOrthPart · Next: integral_inner_mul_affineOrthPart.

Source excerpt, lines 245–247 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_L2_AffineDecomposition

open MeasureTheory
variable {n : ℕ}

Formal statement


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

Source

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

View graph