Centered Gradient Difference Under Adjacent Permutation

Proved

FunctionalInequalities.KLS.LogConcave.PoissonIterate.grad0_step_sub_permField_succ_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes BKL (42).

Let $V$ be finite-dimensional, let $\nu=m\mathbin{.}\mathrm{tilted}(-U)$ with $U\in C^2$ , assume $C_P(\nu)\le C$ , and let $h$ be a level- $k$ field. For an index position $\ell\in\mathrm{Fin}(k+1)$ satisfying $\ell+1<k+1$ , let $\tau_\ell$ swap positions $\ell$ and $\ell+1$ , and let $\tau_{\ell+1}$ be the corresponding swap after the new index is added. Then

\nabla_0(\operatorname{step}(h))-\tau_{\ell+1}\nabla_0(\operatorname{step}(h)) =\operatorname{scale}(h)\,\nabla_0(-L)^{-1}\bigl(\nabla_0h-\tau_\ell\nabla_0h\bigr).

The permutations are represented by permField using Equiv.swap and finRotate.

This identity propagates approximate symmetry from one iterate to the next.

Original Lean declaration header

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

theorem grad0_step_sub_permField_succ {k : ℕ} (h : Field ν k) (ℓ : Fin (k + 1))
    (hℓ : ℓ.val + 1 < k + 1) :
    grad0 T̄ (step T̄ h) -
        permField (Equiv.swap ℓ.succ (finRotate (k + 2) ℓ.succ)) (grad0 T̄ (step T̄ h)) =
      scale T̄ h • grad0 T̄ (invField T̄
        (grad0 T̄ h - permField (Equiv.swap ℓ (finRotate (k + 1) ℓ)) (grad0 T̄ h)))

Module navigation

Module: KLS/BKL/PoissonIterate/Symmetry.

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

Supporting theorems: grad0_sub, existsUnique_centered_adjointComp_eq.

Previous: grad0_sub · Next: normSq_grad0_iter_sub_symField_le.

Source excerpt, lines 191–196 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Symmetry

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)) (hU : ContDiff ℝ 2 U)
  {C : NNReal} (hC : FunctionalInequalities.Poincare.LocalSlope.Intrinsic.constant ν ≤ (C : ENNReal))
local notation "T̄" => hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
include hνU hU hC

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.PoissonIterate.grad0_step_sub_permField_succ_readable {k : ℕ} (h : Field ν k) (ℓ : Fin (k + 1))
    (hℓ : ℓ.val + 1 < k + 1) :
    grad0 T̄ (step T̄ h) -
        permField (Equiv.swap ℓ.succ (finRotate (k + 2) ℓ.succ)) (grad0 T̄ (step T̄ h)) =
      scale T̄ h • grad0 T̄ (invField T̄
        (grad0 T̄ h - permField (Equiv.swap ℓ (finRotate (k + 1) ℓ)) (grad0 T̄ h))) := by sorry

Source

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

View graph