Bounds on partial sums of binomial coefficients

TheoremWeighted partial binomial sum bounded by the full expansion#✓fully proved

A weighted partial binomial sum is bounded by the full binomial expansion.

theorem pow_mul_sum_choose_le {D r : ℕ} (hr : r ≤ D) {x : ℝ}
    (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :
    x ^ r * ∑ j ∈ range (r + 1), (D.choose j : ℝ) ≤ (x + 1) ^ D

Used by 2

Used byExponential bound on a weighted partial binomial sum · Number of subsets of size at most \(r\) is at most \((3D/r)^r\)

TheoremExponential bound on a weighted partial binomial sum#✓fully proved

Exponential bound on the weighted partial binomial sum, including the zero-weight boundary.

theorem pow_mul_sum_choose_le_exp {D r : ℕ} (hr : r ≤ D) {x : ℝ}
    (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :
    x ^ r * ∑ j ∈ range (r + 1), (D.choose j : ℝ) ≤ exp ((D : ℝ) * x)

Uses 1

Proof usesWeighted partial binomial sum bounded by the full expansion

TheoremNumber of subsets of size at most \(r\) is at most \((3D/r)^r\)#✓fully proved

For 1 ≤ r ≤ D, the number of subsets of size at most r is at most (3 * D / r) ^ r.

theorem sum_choose_le_pow {D r : ℕ} (hr0 : 1 ≤ r) (hrD : r ≤ D) :
    (∑ j ∈ range (r + 1), (D.choose j : ℝ)) ≤ (3 * D / r) ^ r

Uses 1

Proof usesWeighted partial binomial sum bounded by the full expansion

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.