All-Order Cutoff Energy Claim

This formalizes the strong-induction form of the cutoff-energy claim associated with Equation (95) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Assume the compact Letwin bound and let $K\ge153$. Also assume:

1. For every $m\ge3$, if the cutoff claims hold at all orders $r-1$ with $2\le r<m$, and the corresponding compact cumulant bounds hold, then CutoffEnergyClaim K (m - 1) holds.
2. Every CutoffEnergyClaim K d implies CumulantBoundCompact d (envelope K (d+1)).

Then every integer $d\ge1$ satisfies

This declaration is an induction interface: it reduces all positive orders to the supplied step and bound hypotheses together with the base case.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

theorem cutoffEnergyClaim_all (hL : LogConcave.Suspension.LetwinCompactBound) {K : ℝ} (hK : 153 ≤ K)
    (hstep : ∀ m : ℕ, 3 ≤ m →
      (∀ r : ℕ, 2 ≤ r → r < m → CutoffEnergyClaim K (r - 1)) →
      (∀ r : ℕ, 2 ≤ r → r < m → LogConcave.Suspension.CumulantBoundCompact (r - 1) (envelope K r)) →
      CutoffEnergyClaim K (m - 1))
    (hbound : ∀ d : ℕ, CutoffEnergyClaim K d → LogConcave.Suspension.CumulantBoundCompact d (envelope K (d + 1))) :
    ∀ d : ℕ, 1 ≤ d → CutoffEnergyClaim K d

Module navigation

Module: KLS/BKL/Localization/CutoffEnergy/Induction.

Definition modules: KLS/BKL/CompactReduction, KLS/BKL/Localization/CutoffEnergy/Basic, KLS/BKL/CumulantEnvelope.

Supporting theorems: cutoffEnergyClaim_one.

Source excerpt, lines 19–25 · Frozen source 408915f.