Binomial prefix tail bound with a strict rate in (0,1)

Proved

binomial_prefix_tail_of_linear_gap

by mysticflounder · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

binomialchernoff-ratefinite-sumnumber-theoryreal-inequality

For every real c > 0, natural q,t with q > 0, and linear-gap hypothesis (2+c)t ≤ q, the finite prefix sum ∑_{k<t} binom(q-1,k), normalized by 2^q, is at most the q-th power of the explicit rate ((2+c)/(2(1+c))) * (1+c)^(1/(2+c)). The same conjunction records that this rate is strictly between 0 and 1.

Preamble

import Mathlib
set_option autoImplicit false
open Real
open scoped BigOperators
noncomputable section

Formal statement

theorem binomial_prefix_tail_of_linear_gap (c : ℝ) (hc : 0 < c) (q t : ℕ) (hq : 0 < q) (hqt : (2 + c) * (t : ℝ) ≤ (q : ℝ)) :
    0 < ((2 + c) / (2 * (1 + c))) * Real.rpow (1 + c) (1 / (2 + c)) ∧
      ((2 + c) / (2 * (1 + c))) * Real.rpow (1 + c) (1 / (2 + c)) < 1 ∧
      (∑ k : Fin t, (Nat.choose (q - 1) k : ℝ)) / (2 : ℝ) ^ q ≤
        (((2 + c) / (2 * (1 + c))) * Real.rpow (1 + c) (1 / (2 + c))) ^ q := by sorry

View graph