Prove2Me

Binomial Envelope Product Identity

Proved
FunctionalInequalities.KLS.BKL.choose_mul_sqrt_envelope_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the binomial identity (105) from BKL.

Let K≥0K\ge0 and let integers m,am,a satisfy 1≤a≤m1\le a\le m. For bj=envelope⁡(K,j)=Kj−1((j−1)!)2b_j=\operatorname{envelope}(K,j)=K^{j-1}((j-1)!)^2, one has

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

The identity is purely arithmetic and is used to normalize the terms in the cumulant-envelope induction.

Original Lean declaration header

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

theorem choose_mul_sqrt_envelope {K : ℝ} (hK : 0 ≤ K) {m a : ℕ} (ha : 1 ≤ a) (ham : a ≤ m) :
    ((m - 1).choose (a - 1) : ℝ) * Real.sqrt (envelope K a * envelope K (m - a + 1)) =
      Real.sqrt (envelope K m)

Module navigation

Module: KLS/BKL/CumulantEnvelope.

Next: sum_choose_mul_sqrt_envelope.

Source excerpt, lines 28–30 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_CumulantEnvelope
Formal statement

theorem FunctionalInequalities.KLS.BKL.choose_mul_sqrt_envelope_readable {K : ℝ} (hK : 0 ≤ K) {m a : ℕ} (ha : 1 ≤ a) (ham : a ≤ m) :
    ((m - 1).choose (a - 1) : ℝ) * Real.sqrt (envelope K a * envelope K (m - a + 1)) =
      Real.sqrt (envelope K m) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/CumulantEnvelope.lean#L26-L86 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.CumulantEnvelope`, declaration `FunctionalInequalities.KLS.BKL.choose_mul_sqrt_envelope`; the repository is private at upload time).

View graph