Symmetric Approximation of a Centered Gradient Step

Proved

FunctionalInequalities.KLS.LogConcave.PoissonIterate.exists_symm_normSq_grad0_step_sub_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes BKL Lemma 3.2 for one step.

Let $V$ be finite-dimensional, let $\nu=m\mathbin{.}\mathrm{tilted}(-U)$ with $U$ of temperate growth and all exponential moments, and suppose $C_P(\nu)\le C$ with $C>0$ . Let $h$ be a level- $k$ field whose components lie in $D(A)$ , where $A=\bar T^\dagger\bar T$ . Then there exists a level- $(k+2)$ field $S$ such that:

$S$ is symmetric in its first two indices:

S(J\circ(0\;1))=S(J).

The centered gradient of the Poisson step is within the defect bound:

\|\nabla_0(\operatorname{step}(h))-S\|^2\le C\,\operatorname{defect}(h).

The field $S$ is allowed to depend on $h$ and is not asserted to be unique.

This estimate is the starting point for the approximate symmetry bounds of later iterates.

Original Lean declaration header

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

theorem exists_symm_normSq_grad0_step_sub_le (hCpos : 0 < C) {k : ℕ} (h : Field ν k)
    (hh : ∀ I, h I ∈ (adjointComp T̄).domain) :
    ∃ S : Field ν (k + 2), (∀ J, S (J ∘ Equiv.swap 0 1) = S J) ∧
      normSq (grad0 T̄ (step T̄ h) - S) ≤ (C : ℝ) * defect T̄ h

Module navigation

Module: KLS/BKL/PoissonIterate/Defect.

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

Supporting theorems: gradField_gradField_comp_swap, inv_le_scale_sq_step, inner_center_center, sum_norm_sq_compLp_innerSL.

Previous: gradField_gradField_comp_swap.

Source excerpt, lines 285–288 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Defect

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.exists_symm_normSq_grad0_step_sub_le_readable (hCpos : 0 < C) {k : ℕ} (h : Field ν k)
    (hh : ∀ I, h I ∈ (adjointComp T̄).domain) :
    ∃ S : Field ν (k + 2), (∀ J, S (J ∘ Equiv.swap 0 1) = S J) ∧
      normSq (grad0 T̄ (step T̄ h) - S) ≤ (C : ℝ) * defect T̄ h := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/PoissonIterate/Defect.lean#L281-L309 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.PoissonIterate.Defect`, declaration `FunctionalInequalities.KLS.LogConcave.PoissonIterate.exists_symm_normSq_grad0_step_sub_le`; the repository is private at upload time).

View graph