Approximate Symmetry of Poisson Iterates

Proved

FunctionalInequalities.KLS.LogConcave.PoissonIterate.normSq_grad0_iter_sub_symField_le_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes BKL Lemma 3.3, p. 12.

Let $V$ be finite-dimensional, let $\nu=m\mathbin{.}\mathrm{tilted}(-U)$ with $U$ of temperate growth and all exponential moments, and assume $C_P(\nu)\le C$ with $C>0$ . Let $f\in D(A)$ , where $A=\bar T^\dagger\bar T$ . For natural numbers $k,q$ and a real $\beta$ , assume:

$2\le q\le k+1$ .
For every $j$ with $k+1-q\le j<k$ , the iterate scale satisfies

0<\alpha_j,\qquad \alpha_j^2\le\frac\beta C.

Then the centered gradient field of the $k$ th iterate obeys

\|\nabla_0h_{k+1}-S_q\nabla_0h_{k+1}\|^2 \le4q^4\max(1,\beta)^qC \sum_{j=k+1-q}^{k-1}\chi_j,

where $S_q$ symmetrizes the first $q$ positions and $\chi_j$ is the defect of the corresponding iterate.

This is the main approximate-symmetry estimate used in the Taylor recursion.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave.PoissonIterate. Shown in its original module context. Proof omitted.

theorem normSq_grad0_iter_sub_symField_le (hCpos : 0 < C)
    {f : Lp ℝ 2 (ν : Measure V)} (hf : f ∈ (adjointComp T̄).domain) {β : ℝ} (k q : ℕ)
    (hq : 2 ≤ q) (hqk : q ≤ k + 1)
    (hα : ∀ j, k + 1 - q ≤ j → j < k →
      0 < scale T̄ (iter T̄ f j) ∧ scale T̄ (iter T̄ f j) ^ 2 ≤ β / C) :
    normSq (grad0 T̄ (iter T̄ f k) - symField q (grad0 T̄ (iter T̄ f k))) ≤
      4 * (q : ℝ) ^ 4 * max 1 β ^ q * C *
        ∑ j ∈ Finset.Ico (k + 1 - q) k, defect T̄ (iter T̄ f j)

Module navigation

Module: KLS/BKL/PoissonIterate/Symmetry.

Definition modules: KLS/BKL/PoissonIterate/Basic, KLS/LogConcave/WeightedGradient/Closure, Analysis/Semigroup/AdjointComp, Probability/LogConcave, Poincare/LocalSlope/Basic.

Selected supporting theorems: exists_symm_normSq_grad0_step_sub_le, grad0_step_sub_permField_succ, normSq_sub_symField_le, centered_adjointComp_bounds, existsUnique_centered_adjointComp_eq.

Previous: grad0_step_sub_permField_succ.

Source excerpt, lines 349–356 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Symmetry

open MeasureTheory Finset
open FunctionalInequalities.Analysis.Semigroup
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {ν : MeasureTheory.ProbabilityMeasure V} (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] (hν : FunctionalInequalities.KLS.LogConcave ν)
  (hi : (interior (ν : MeasureTheory.Measure V).support).Nonempty) {U : V → ℝ}
  (hνU : (ν : MeasureTheory.Measure V) = m.tilted (-U)) (hUt : U.HasTemperateGrowth)
  (hexp : ∀ r : ℝ, MeasureTheory.Integrable (fun x => Real.exp (r * ‖x‖)) (ν : MeasureTheory.Measure V))
  {C : NNReal} (hC : FunctionalInequalities.Poincare.LocalSlope.Intrinsic.constant ν ≤ (C : ENNReal))
local notation "T̄" => hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
include hνU hUt hexp hC

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.PoissonIterate.normSq_grad0_iter_sub_symField_le_readable (hCpos : 0 < C)
    {f : Lp ℝ 2 (ν : Measure V)} (hf : f ∈ (adjointComp T̄).domain) {β : ℝ} (k q : ℕ)
    (hq : 2 ≤ q) (hqk : q ≤ k + 1)
    (hα : ∀ j, k + 1 - q ≤ j → j < k →
      0 < scale T̄ (iter T̄ f j) ∧ scale T̄ (iter T̄ f j) ^ 2 ≤ β / C) :
    normSq (grad0 T̄ (iter T̄ f k) - symField q (grad0 T̄ (iter T̄ f k))) ≤
      4 * (q : ℝ) ^ 4 * max 1 β ^ q * C *
        ∑ j ∈ Finset.Ico (k + 1 - q) k, defect T̄ (iter T̄ f j) := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Lemma 3.3, p. 12. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/PoissonIterate/Symmetry.lean#L345-L373 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.PoissonIterate.Symmetry`, declaration `FunctionalInequalities.KLS.LogConcave.PoissonIterate.normSq_grad0_iter_sub_symField_le`; the repository is private at upload time).

View graph