Affine-orthogonal part of an L² function

Definition

KLSModular_FunctionalInequalities_L2_AffineDecomposition

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

bkl2026functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a measure $\mu$ on $\mathbb{R}^n$ and a real function $g$ , affineOrthPart μ g x subtracts from $g(x)$ its integral $\int g\,d\mu$ and its standard-basis linear component $\sum_j(\int\langle e_j,y\rangle g(y)\,d\mu)\langle e_j,x\rangle$ . Under the centered probability and identity-covariance hypotheses used by the module, this is the component orthogonal to affine functions; the bundle also contains the abstract affine-decomposition norm estimate.

Original module imports

import Mathlib.Analysis.InnerProductSpace.Projection.Basic
import Mathlib.Analysis.InnerProductSpace.Orthogonal
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.Normed.Lp.MeasurableSpace
import Mathlib.MeasureTheory.Function.L2Space
import Mathlib.Analysis.Calculus.ContDiff.Basic

Original declaration excerpt

Shown in the original module context.

noncomputable def affineOrthPart (μ : Measure (EuclideanSpace ℝ (Fin n)))
    (g : EuclideanSpace ℝ (Fin n) → ℝ) (x : EuclideanSpace ℝ (Fin n)) : ℝ :=
  g x - ∫ y, g y ∂μ -
    ∑ j, (∫ y, ⟪EuclideanSpace.basisFun (Fin n) ℝ j, y⟫ * g y ∂μ) *
      ⟪EuclideanSpace.basisFun (Fin n) ℝ j, x⟫

Module navigation

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.L2.AffineDecomposition · Frozen source 408915f.

Definition code

import Mathlib.Analysis.InnerProductSpace.Projection.Basic
import Mathlib.Analysis.InnerProductSpace.Orthogonal
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.Normed.Lp.MeasurableSpace
import Mathlib.MeasureTheory.Function.L2Space
import Mathlib.Analysis.Calculus.ContDiff.Basic

open MeasureTheory
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace L2
section AffineOrthPart
variable {n : ℕ}
/-- The affine-orthogonal part of `g`: `g` minus its mean and its linear component. -/
noncomputable def affineOrthPart (μ : Measure (EuclideanSpace ℝ (Fin n)))
    (g : EuclideanSpace ℝ (Fin n) → ℝ) (x : EuclideanSpace ℝ (Fin n)) : ℝ :=
  g x - ∫ y, g y ∂μ -
    ∑ j, (∫ y, ⟪EuclideanSpace.basisFun (Fin n) ℝ j, y⟫ * g y ∂μ) *
      ⟪EuclideanSpace.basisFun (Fin n) ℝ j, x⟫
end AffineOrthPart
end L2
end FunctionalInequalities

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), item P71. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/L2/AffineDecomposition.lean#L177-L182 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.L2.AffineDecomposition`, definition bundle `KLSModular_FunctionalInequalities_L2_AffineDecomposition`; the repository is private at upload time).

View graph