BKL cumulant envelope

Definition

KLSModular_FunctionalInequalities_KLS_BKL_CumulantEnvelope

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

bkl2026functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

envelope K m is the real-valued sequence $b_m=K^{m-1}((m-1)!)^2$ for $K,m\in\mathbb{R}\times\mathbb{N}$ . It is a deterministic arithmetic expression used as an induction envelope; the definition alone asserts no cumulant estimate or KLS bound.

Original module imports

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Algebra.Order.BigOperators.Group.Finset

Original declaration excerpt

Shown in the original module context.

def envelope (K : ℝ) (m : ℕ) : ℝ := K ^ (m - 1) * ((m - 1).factorial : ℝ) ^ 2

Module navigation

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.CumulantEnvelope · Frozen source 408915f.

Definition code

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Algebra.Order.BigOperators.Group.Finset

noncomputable section
namespace FunctionalInequalities
namespace KLS
namespace BKL
/-- The cumulant envelope `b_m = K^{m-1} ((m-1)!)²` of BKL (94). -/
def envelope (K : ℝ) (m : ℕ) : ℝ := K ^ (m - 1) * ((m - 1).factorial : ℝ) ^ 2
end BKL
end KLS
end FunctionalInequalities

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), item T41. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/CumulantEnvelope.lean#L19-L20 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.CumulantEnvelope`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_CumulantEnvelope`; the repository is private at upload time).

View graph