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.

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.
• 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.

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

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 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.