Squared-Integral Contraction of the Affine-Orthogonal Part

Proved

FunctionalInequalities.L2.integral_affineOrthPart_sq_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This lemma states Bessel's inequality for the concrete affine-orthogonal part.

Let $n\in\mathbb N$ and let $\mu$ be a probability measure on $E=\mathbb R^n$ (EuclideanSpace ℝ (Fin n)). Assume:

$\operatorname{id}\in L^2(\mu)$ and $\int x\,d\mu=0$ .
$\int\langle u,x\rangle\langle v,x\rangle\,d\mu=\langle u,v\rangle$ for all $u,v\in E$ .
$g:E\to\mathbb R$ belongs to $L^2(\mu)$ .

Using the standard orthonormal basis $(e_j)$ , let $\widetilde g=$ affineOrthPart $\mu\ g$ , namely

\widetilde g(x)=g(x)-\int g\,d\mu-\sum_j\left(\int\langle e_j,y\rangle g(y)\,d\mu(y)\right)\langle e_j,x\rangle.

Then

\int\widetilde g^2\,d\mu\le\int g^2\,d\mu.

This controls the squared $L^2$ size of the affine-orthogonal remainder under centered identity-covariance moment assumptions.

Original Lean declaration header

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

theorem integral_affineOrthPart_sq_le (μ : 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 μ) :
    ∫ x, affineOrthPart μ g x ^ 2 ∂μ ≤ ∫ x, g x ^ 2 ∂μ

Module navigation

Module: L2/AffineDecomposition.

Supporting theorems: integral_affineOrthPart, integral_inner_mul_affineOrthPart, memLp_affineOrthPart.

Previous: integral_affineOrthPart_mul_sub · Next: integral_affine_sq.

Source excerpt, lines 698–702 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_L2_AffineDecomposition

open MeasureTheory
open scoped RealInnerProductSpace
variable {n : ℕ}

Formal statement


theorem FunctionalInequalities.L2.integral_affineOrthPart_sq_le_readable (μ : 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 μ) :
    ∫ x, affineOrthPart μ g x ^ 2 ∂μ ≤ ∫ x, g x ^ 2 ∂μ := by sorry

Source

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

View graph