Iterated Taylor Symmetrization Bound

Proved

FunctionalInequalities.KLS.LogConcave.PoissonIterate.norm_symmetrize_taylorField_grad0_iter_sq_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes BKL (56)–(57).

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$ . For $f\in L^2(\nu)$ , let $e,d,k\in\mathbb N$ satisfy $d\ge1$ and $e\le k$ . Suppose that for every $j<k$ ,

\alpha_j^2\le\frac\beta C,

where $\alpha_j$ is the scale of the $j$ th Poisson iterate. Then

\left\|S_{d+e}T_d(\nabla_0h_{k+1})\right\|^2 \le\left(\frac\beta C\right)^e \left\|T_{d+e}(\nabla_0h_{k+1-e})\right\|^2.

Here $S_{d+e}$ symmetrizes the indicated initial positions and the Taylor fields are represented by the formalization's taylorField.

This estimate iterates the one-step Taylor-field identity and supplies the main recursive contraction factor.

Original Lean declaration header

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

theorem norm_symmetrize_taylorField_grad0_iter_sq_le (f : Lp ℝ 2 (ν : Measure V)) {β : ℝ}
    (e : ℕ) : ∀ (d k : ℕ), 1 ≤ d → e ≤ k → (∀ j < k, scale T̄ (iter T̄ f j) ^ 2 ≤ β / C) →
      ‖symmetrize (Module.finrank ℝ V) (d + (k + 1)) (d + e)
          (taylorField d (grad0 T̄ (iter T̄ f k)))‖ ^ 2 ≤
        (β / C) ^ e * ‖taylorField (d + e) (grad0 T̄ (iter T̄ f (k - e)))‖ ^ 2

Module navigation

Module: KLS/BKL/PoissonIterate/TaylorRecursion.

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

Supporting theorems: symmetrize_taylorField_grad0_step.

Next: norm_taylorField_grad0_iter_sq_le.

Source excerpt, lines 435–439 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_TaylorRecursion

open MeasureTheory Finset
open FunctionalInequalities.Analysis.Tensor
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.norm_symmetrize_taylorField_grad0_iter_sq_le_readable (f : Lp ℝ 2 (ν : Measure V)) {β : ℝ}
    (e : ℕ) : ∀ (d k : ℕ), 1 ≤ d → e ≤ k → (∀ j < k, scale T̄ (iter T̄ f j) ^ 2 ≤ β / C) →
      ‖symmetrize (Module.finrank ℝ V) (d + (k + 1)) (d + e)
          (taylorField d (grad0 T̄ (iter T̄ f k)))‖ ^ 2 ≤
        (β / C) ^ e * ‖taylorField (d + e) (grad0 T̄ (iter T̄ f (k - e)))‖ ^ 2 := by sorry

Source

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

View graph