Orthogonality Between the Affine Residual and Affine Part

Proved

FunctionalInequalities.L2.integral_affineOrthPart_mul_sub_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement gives the vanishing cross term between a function's designated affine residual and its affine part.

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

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

Let $h=$ L2.affineOrthPart μ g, where

h(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 h(x)\bigl(g(x)-h(x)\bigr)\,d\mu(x)=0.

This is the cross-term identity used in the affine Pythagorean decomposition. The $L^2$ hypotheses are MemLp conditions; dimension zero is included.

Original Lean declaration header

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

theorem integral_affineOrthPart_mul_sub (μ : 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 * (g x - affineOrthPart μ g x) ∂μ = 0

Module navigation

Module: L2/AffineDecomposition.

Supporting theorems: integral_affineOrthPart, integral_inner_mul_affineOrthPart, memLp_affineOrthPart.

Previous: contDiff_affineOrthPart · Next: integral_affineOrthPart_sq_le.

Source excerpt, lines 595–599 · 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_mul_sub_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 * (g 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#L594-L695 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.L2.AffineDecomposition`, declaration `FunctionalInequalities.L2.integral_affineOrthPart_mul_sub`; the repository is private at upload time).

View graph