Prove2Me

Summed Binomial Envelope Identity

Proved
FunctionalInequalities.KLS.BKL.sum_choose_mul_sqrt_envelope_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the summation identity (106) from BKL.

Let K≥0K\ge0 and let m≥3m\ge3. With bj=envelope⁡(K,j)b_j=\operatorname{envelope}(K,j),

∑a=2m−2(m−1a−1)babm−a+1=(m−3)bm.\sum_{a=2}^{m-2} \binom{m-1}{a-1}\sqrt{b_a b_{m-a+1}} =(m-3)\sqrt{b_m}.

The identity counts the m−3m-3 terms in the indicated integer interval and is used in the scalar envelope recurrence.

Original Lean declaration header

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

theorem sum_choose_mul_sqrt_envelope {K : ℝ} (hK : 0 ≤ K) {m : ℕ} (hm : 3 ≤ m) :
    ∑ a ∈ Finset.Icc 2 (m - 2),
        ((m - 1).choose (a - 1) : ℝ) * Real.sqrt (envelope K a * envelope K (m - a + 1)) =
      ((m - 3 : ℕ) : ℝ) * Real.sqrt (envelope K m)

Module navigation

Module: KLS/BKL/CumulantEnvelope.

Supporting theorems: choose_mul_sqrt_envelope.

Previous: choose_mul_sqrt_envelope · Next: absorption_le_envelope.

Source excerpt, lines 100–103 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_CumulantEnvelope
Formal statement

theorem FunctionalInequalities.KLS.BKL.sum_choose_mul_sqrt_envelope_readable {K : ℝ} (hK : 0 ≤ K) {m : ℕ} (hm : 3 ≤ m) :
    ∑ a ∈ Finset.Icc 2 (m - 2),
        ((m - 1).choose (a - 1) : ℝ) * Real.sqrt (envelope K a * envelope K (m - a + 1)) =
      ((m - 3 : ℕ) : ℝ) * Real.sqrt (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#L98-L127 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.CumulantEnvelope`, declaration `FunctionalInequalities.KLS.BKL.sum_choose_mul_sqrt_envelope`; the repository is private at upload time).

View graph