The binomial tail in closed form

For m ≤ n the mass a binomial law Bin(n, p) puts on {k | m ≤ k} is a single value of the regularized incomplete beta function,

Bin(n, p).real {k | m ≤ k} = I_p(m, n - m + 1).

This is the binomial entry of the "Closed-form cdfs and tails" target of TauCetiRoadmap/StandardDistributions/README.md, Layer 2, and it is what supplies the cumulative mass function that Layer 1 defers to Layer 2 for the binomial and Bernoulli laws.

The identity is proved by induction on m with n fixed. Removing the least point of the tail subtracts the binomial weight (n.choose m) * p ^ m * (1 - p) ^ (n - m), so the right-hand side must satisfy the same recurrence, and it does: I_p(m, n - m + 1) and I_p(m + 1, n - m) are neighbours along the antidiagonal a + b = n + 1, whose step TauCeti.regularizedIncompleteBeta_add_one_right_sub_add_one_left has increment Γ(a + b + 1) / (Γ(a + 1) * Γ(b + 1)) times p ^ a * (1 - p) ^ b. At a = m and b = n - m that generalized binomial coefficient is n.choose m, by Nat.choose_mul_factorial_mul_factorial.

The induction starts at m = 0, where the tail is everything and the left-hand side is 1. This is the one place the boundary convention I_x(0, b) = 1 of TauCeti.regularizedIncompleteBeta is used, and it is the completion check the roadmap states for this target: at m = 0 the identity reads 1 = 1 for every admissible p, including p = 0 and p = 1.

Main results

• TauCeti.Probability.binomial_tail_eq_regularizedIncompleteBeta — the tail I_p(m, n - m + 1);
• TauCeti.Probability.sum_Icc_choose_mul_pow_eq_regularizedIncompleteBeta — the same identity written as a partial sum of binomial weights, which is the classical form;
• TauCeti.Probability.binomial_cumulative_eq_regularizedIncompleteBeta — the complementary cumulative mass I_{1-p}(n - m, m + 1).

References

• Roadmap: TauCetiRoadmap/StandardDistributions/README.md, Layer 2, the "Closed-form cdfs and tails" target.
• NIST Digital Library of Mathematical Functions, §8.17(v).
• N. L. Johnson, A. W. Kemp, S. Kotz, Univariate Discrete Distributions, 3rd ed., Wiley, 2005, §3.4.

@[simp]

theorem TauCeti.Probability.binomial_tail_eq_regularizedIncompleteBeta {m n : ℕ} (hmn : m ≤ n) (p : ↑unitInterval) : (ProbabilityTheory.binomial n p).real {k : ℕ | m ≤ k} = regularizedIncompleteBeta (↑m) (↑n - ↑m + 1) ↑p

The binomial tail is a regularized incomplete beta value. For m ≤ n the mass that Bin(n, p) puts on {k | m ≤ k} is I_p(m, n - m + 1).

At m = 0 both sides are 1: the left-hand side because Bin(n, p) is a probability measure, the right-hand side by the boundary convention I_x(0, b) = 1 built into TauCeti.regularizedIncompleteBeta.

theorem TauCeti.Probability.sum_Icc_choose_mul_pow_eq_regularizedIncompleteBeta {m n : ℕ} (hmn : m ≤ n) (p : ↑unitInterval) : ∑ k ∈ Finset.Icc m n, ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k) = regularizedIncompleteBeta (↑m) (↑n - ↑m + 1) ↑p

The classical form of the tail identity: a partial sum of binomial weights is a value of the regularized incomplete beta function.

@[simp]

theorem TauCeti.Probability.binomial_cumulative_eq_regularizedIncompleteBeta {m n : ℕ} (hmn : m ≤ n) (p : ↑unitInterval) : (ProbabilityTheory.binomial n p).real {k : ℕ | k ≤ m} = regularizedIncompleteBeta (↑n - ↑m) (↑m + 1) (1 - ↑p)

The cumulative mass of a binomial law, the complement of the tail identity: for m ≤ n, Bin(n, p).real {k | k ≤ m} = I_{1-p}(n - m, m + 1).

This is the cumulative mass function that TauCetiRoadmap/StandardDistributions/README.md, Layer 1 defers to this layer.