Real bounds for partial binomial sums

The binomial generating function gives ∑ j ≤ e, q.choose j ≤ exp (q / T) * T ^ e for any real T ≥ 1. For 0 < e ≤ q, choosing T = q / e gives (exp 1 * q / e) ^ e. This bound remains valid above half the dimension. At radius zero the sum and bound are both one.

The generating-function proof is shared with the sparsification lemma. The logarithmic consequences turn an exponential lower bound on the square of a partial binomial sum into size-activity bounds; they include the zero-radius case using the usual total real operations.

An exact integer logarithm test also bounds the tail of dimension C * N and radius Γ * N / M by 2 ^ (N / B) for every N. This is an original specialization of the generating-function bound, motivated by the geometric thresholds in Appendix A.3 of [OAI26c]; it does not construct the parameters or bound the cost of selecting them.

Main results

• Cslib.sum_choose_le_exp_mul_pow: a real-parameter generating-function bound.
• Cslib.sum_choose_le_exp_one_mul_div_pow: the bound with parameter q / e.
• Nat.choose_le_exp_mul_div_pow: its single-binomial-coefficient consequence, for all n, k.
• Cslib.sum_choose_le_two_rpow_div: the geometric tail under an exact integer budget test.
• Cslib.sum_choose_le_two_pow_div_add_one: its natural-number rounded form.
• Cslib.le_mul_logb_of_two_pow_le_sum_choose_sq: the logarithmic consequence.
• Cslib.mul_rpow_le_of_two_pow_le_sum_choose_sq: the rearranged size lower bound.
• Real.exists_one_le_and_mul_pow_le_pow: a polynomial is eventually below an exponential with base r > 1.

References

• [Threshold Circuits as Decision Trees and Finite-State Programs, Theorem 3.2] [26]
• C. Calabro, R. Impagliazzo, R. Paturi, A duality between clause width and clause density for SAT
• OpenAI, The Exponential Time Hypothesis is False, Appendix A.3, pp. 46–47

theorem Cslib.sum_choose_le_exp_mul_pow (q e : ℕ) (T : ℝ) (hT : 1 ≤ T) : ∑ j ∈ Finset.range (e + 1), ↑(q.choose j) ≤ Real.exp (↑q / T) * T ^ e

A partial binomial sum is at most exp (q / T) * T ^ e for every real T ≥ 1. The radius e may exceed q.

theorem Cslib.sum_choose_le_exp_one_mul_div_pow {q e : ℕ} (heq : e ≤ q) : ∑ j ∈ Finset.range (e + 1), ↑(q.choose j) ≤ (Real.exp 1 * ↑q / ↑e) ^ e

The standard bound (exp 1 * q / e) ^ e holds throughout e ≤ q, not just for e ≤ q / 2. At e = 0 both sides are one.

theorem Nat.choose_le_exp_mul_div_pow (n k : ℕ) : ↑(n.choose k) ≤ (Real.exp 1 * ↑n / ↑k) ^ k

A single binomial coefficient is at most (exp 1 * n / k)^k, including k = 0. This follows from Cslib.sum_choose_le_exp_one_mul_div_pow when k ≤ n; otherwise the coefficient vanishes. The statement is also present in Anthropic's formal source; this proof reuses the partial-sum bound.

theorem Cslib.sum_choose_le_two_rpow_div {C Γ M B : ℕ} (hC : 4 ≤ C) (hΓ : 4 ≤ Γ) (hM : Γ ≤ M) (hB : 1 ≤ B) (hbudget : B * Γ * Nat.clog 2 (4 * C * M) ≤ M) (N : ℕ) : ∑ j ∈ Finset.range (Γ * N / M + 1), ↑((C * N).choose j) ≤ 2 ^ (↑N / ↑B)

For any input size N, the tail with dimension C * N and radius Γ * N / M is at most 2 ^ (N / B) when the exact integer test B * Γ * ⌈log₂ (4 * C * M)⌉ ≤ M holds. This is an original corollary of sum_choose_le_exp_mul_pow, motivated by Appendix A.3 of [OAI26c], rather than a verbatim result from that source. Zero input and zero radius are included. The parameters are supplied; no parameter-selection or complexity bound is asserted.

theorem Cslib.sum_choose_le_two_pow_div_add_one {C Γ M B : ℕ} (hC : 4 ≤ C) (hΓ : 4 ≤ Γ) (hM : Γ ≤ M) (hB : 1 ≤ B) (hbudget : B * Γ * Nat.clog 2 (4 * C * M) ≤ M) (N : ℕ) : ∑ j ∈ Finset.range (Γ * N / M + 1), (C * N).choose j ≤ 2 ^ (N / B + 1)

The natural-number rounding of sum_choose_le_two_rpow_div, suitable for a discrete leaf-count or round budget. The division in the conclusion is natural-number division.

theorem Cslib.le_mul_logb_of_two_pow_le_sum_choose_sq {m q e : ℕ} (heq : e ≤ q) (h : 2 ^ m ≤ (∑ j ∈ Finset.range (e + 1), q.choose j) ^ 2) : ↑m / 2 ≤ ↑e * Real.logb 2 (Real.exp 1 * ↑q / ↑e)

If the square of the radius-e binomial sum is at least 2 ^ m, then m / 2 ≤ e * log₂ (exp 1 * q / e). The statement includes e = 0, which forces m = 0.

theorem Cslib.mul_rpow_le_of_two_pow_le_sum_choose_sq {m q e : ℕ} (heq : e ≤ q) (h : 2 ^ m ≤ (∑ j ∈ Finset.range (e + 1), q.choose j) ^ 2) : ↑e / Real.exp 1 * 2 ^ (↑m / (2 * ↑e)) ≤ ↑q

The logarithmic partial-binomial-sum bound rearranged as a lower bound on q. At radius zero the lower bound is zero.

theorem Real.exists_one_le_and_mul_pow_le_pow (C : ℝ) (d : ℕ) {r : ℝ} (hr : 1 < r) : ∃ (α : ℕ), 1 ≤ α ∧ C * ↑α ^ d ≤ r ^ α

A polynomial is eventually below an exponential with base r > 1.