Scalar Absorption by the Cumulant Envelope

Proved

FunctionalInequalities.KLS.BKL.absorption_le_envelope_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the scalar absorption estimate after BKL (106), p. 27.

Let $C,K\in\mathbb{R}$ satisfy $C\ge0$ , $K\ge9C$ , and $K\ge64$ . For an integer $m\ge3$ , let

b_j=\operatorname{envelope}(K,j)=K^{j-1}((j-1)!)^2.

Then

2Cm^2b_{m-1}+4(m-3)\sqrt{b_{m-1}b_m}\le b_m.

This is an arithmetic estimate only; it does not assert a cumulant bound or complete the induction by itself.

Original Lean declaration header

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

theorem absorption_le_envelope {K C : ℝ} (hC : 0 ≤ C) (hK9 : 9 * C ≤ K) (hK64 : 64 ≤ K)
    {m : ℕ} (hm : 3 ≤ m) :
    2 * C * (m : ℝ) ^ 2 * envelope K (m - 1) +
        4 * ((m - 3 : ℕ) : ℝ) * Real.sqrt (envelope K (m - 1) * envelope K m) ≤
      envelope K m

Module navigation

Module: KLS/BKL/CumulantEnvelope.

Previous: sum_choose_mul_sqrt_envelope.

Source excerpt, lines 133–137 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_CumulantEnvelope

Formal statement


theorem FunctionalInequalities.KLS.BKL.absorption_le_envelope_readable {K C : ℝ} (hC : 0 ≤ C) (hK9 : 9 * C ≤ K) (hK64 : 64 ≤ K)
    {m : ℕ} (hm : 3 ≤ m) :
    2 * C * (m : ℝ) ^ 2 * envelope K (m - 1) +
        4 * ((m - 3 : ℕ) : ℝ) * Real.sqrt (envelope K (m - 1) * envelope K m) ≤
      envelope K m := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Theorem 4.1, p. 18. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/CumulantEnvelope.lean#L129-L242 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.CumulantEnvelope`, declaration `FunctionalInequalities.KLS.BKL.absorption_le_envelope`; the repository is private at upload time).

View graph