One-Step Scale Lower Bound

Proved

FunctionalInequalities.KLS.LogConcave.PoissonIterate.inv_le_scale_sq_step_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the one-step inequality corresponding to BKL (32).

Let $V$ be finite-dimensional, let $\nu$ be a log-concave probability measure represented as $m\mathbin{.}\mathrm{tilted}(-U)$ with $U\in C^2$ , and suppose $C_P(\nu)\le C$ for $C\in[0,\infty)$ . Assume also $C>0$ . For any natural number $k$ and any Poisson-iterate field $h$ at level $k$ , if its scale is strictly positive, then

C^{-1}\le \operatorname{scale}(\bar T,h)^2.

Here $\bar T$ is the closed unit-weight gradient operator, and the scale is the definition used for the Poisson step.

This estimate supplies the lower bound on a positive iteration scale required in the recursive symmetry and Taylor estimates.

Formalization Note: The theorem uses $C$ as the real coercion of an NNReal; the Poincaré constant is compared in ENNReal. The conclusion is an ordinary real inequality.

Original Lean declaration header

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

theorem inv_le_scale_sq_step (hCpos : 0 < C) {k : ℕ} (h : Field ν k) (hs : 0 < scale T̄ h) :
    (C : ℝ)⁻¹ ≤ scale T̄ h ^ 2

Module navigation

Module: KLS/BKL/PoissonIterate/Domain.

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

Supporting theorems: centered_adjointComp_bounds, existsUnique_centered_adjointComp_eq, sum_norm_sq_compLp_innerSL.

Source excerpt, lines 385–386 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Domain

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.inv_le_scale_sq_step_readable (hCpos : 0 < C) {k : ℕ} (h : Field ν k) (hs : 0 < scale T̄ h) :
    (C : ℝ)⁻¹ ≤ scale T̄ h ^ 2 := by sorry

Source

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

View graph