The binomial tail, and its derivative in the success probability

Infrastructure for MiscMath.Probability.PoissonTrialsFixedMean, which is where the results are stated and where the reader should start. Nothing here is a result on its own: this file supplies the elementary object binTail and the one calculus fact about it that the argument for Hoeffding's Theorem 4 needs. PoissonTrialsFixedMean.Bridge identifies binTail with Mathlib's ProbabilityTheory.binomial.

The binomial tail

Mathlib has the binomial distribution but no partial sum, tail or cumulative distribution function for it, and no derivative or monotonicity in either parameter. This section supplies the elementary object and the one calculus fact about it that the argument for Theorem 4 needs:

binTail n P k = ∑_{j ≤ k} C(n,j) · P^j · (1-P)^(n-j)   ( = P[Bin(n,P) ≤ k] )

and

d/dP binTail n P k = - n · C(n-1,k) · P^k · (1-P)^(n-1-k).

The derivative is proved by telescoping rather than by passing through Polynomial: differentiating term by term and applying j·C(n,j) = n·C(n-1,j-1) and (n-j)·C(n,j) = n·C(n-1,j) turns each summand into a difference of consecutive terms, and Finset.sum_range_sub' collapses the sum.

Every exponent below is the ℕ-truncated one. That is deliberate, and it is where the care is: at j = 0 and at j > n the truncated powers are wrong, and in each case the accompanying coefficient (j, or n - j, or C(n,j)) vanishes and kills the term. Stating the derivative with binShapeD, which has no negative powers anywhere, is what makes the statement true as written rather than true-up-to-edge-cases.

def MiscMath.Probability.binTail {𝕜 : Type u_1} [CommRing 𝕜] (n : ℕ) (P : 𝕜) (k : ℕ) : 𝕜

The binomial tail P[Bin(n,P) ≤ k] = ∑_{j ≤ k} C(n,j) P^j (1-P)^(n-j). Terms with j > n vanish because C(n,j) = 0, so no truncation guard on k is needed. See binTail_eq_binomial_real_Iic for the identification with Mathlib's ProbabilityTheory.binomial.

Equations

• MiscMath.Probability.binTail n P k = ∑ j ∈ Finset.range (k + 1), ↑(n.choose j) * P ^ j * (1 - P) ^ (n - j)

def MiscMath.Probability.binShape {𝕜 : Type u_1} [CommRing 𝕜] (k m : ℕ) (t : 𝕜) : 𝕜

The shape t^k (1-t)^(m-k); its C(m,k)-multiple is minus 1/(m+1) times the derivative of binTail (m+1) · k.

Equations

• MiscMath.Probability.binShape k m t = t ^ k * (1 - t) ^ (m - k)

def MiscMath.Probability.binShapeD {𝕜 : Type u_1} [CommRing 𝕜] (k m : ℕ) (t : 𝕜) : 𝕜

The derivative of binShape, written with no negative powers: the two coefficients k and m - k kill the truncated exponents exactly where they would otherwise be wrong.

Equations

• MiscMath.Probability.binShapeD k m t = ↑k * t ^ (k - 1) * (1 - t) ^ (m - k) - ↑(m - k) * t ^ k * (1 - t) ^ (m - k - 1)

theorem MiscMath.Probability.binTail_eq_sum_shape {𝕜 : Type u_1} [CommRing 𝕜] (n k : ℕ) (P : 𝕜) : binTail n P k = ∑ j ∈ Finset.range (k + 1), ↑(n.choose j) * binShape j n P

theorem MiscMath.Probability.binTail_succ_term {𝕜 : Type u_1} [CommRing 𝕜] (n k : ℕ) (P : 𝕜) : binTail n P (k + 1) = binTail n P k + ↑(n.choose (k + 1)) * binShape (k + 1) n P

Peeling the top term off a tail.

theorem MiscMath.Probability.binTail_eq_one {𝕜 : Type u_1} [CommRing 𝕜] {n k : ℕ} (P : 𝕜) (hk : n ≤ k) : binTail n P k = 1

Above the number of trials the tail is 1: it is the whole binomial expansion of (P + (1 - P))^n. This is the edge case the ℕ-truncated exponent n - j has to get right.

theorem MiscMath.Probability.binTail_zero_prob {𝕜 : Type u_1} [CommRing 𝕜] (n k : ℕ) : binTail n 0 k = 1

At P = 0 the tail is 1 for every k, including k = 0 — the other edge the truncation touches.

theorem MiscMath.Probability.binTail_nonneg {𝕜 : Type u_1} [CommRing 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {n k : ℕ} {P : 𝕜} (h0 : 0 ≤ P) (h1 : P ≤ 1) : 0 ≤ binTail n P k

The tail is nonnegative in the probability range — it is a probability.

theorem MiscMath.Probability.hasDerivAt_binShape (k m : ℕ) (t : ℝ) : HasDerivAt (binShape k m) (binShapeD k m t) t

theorem MiscMath.Probability.binTail_deriv_telescope (m k : ℕ) (t : ℝ) : ∑ j ∈ Finset.range (k + 1), ↑((m + 1).choose j) * binShapeD j (m + 1) t = -((↑m + 1) * (↑(m.choose k) * binShape k m t))

The telescoping identity. Summing the term-by-term derivatives of the binomial tail collapses to a single term. The two Nat.choose identities j·C(n,j) = n·C(n-1,j-1) and (n-j)·C(n,j) = n·C(n-1,j) turn each summand into a difference of consecutive C(m,·)·binShape values.

theorem MiscMath.Probability.hasDerivAt_binTail (m k : ℕ) (t : ℝ) : HasDerivAt (fun (p : ℝ) => binTail (m + 1) p k) (-((↑m + 1) * (↑(m.choose k) * binShape k m t))) t

The derivative of a binomial tail in the success probability. d/dP ∑_{j ≤ k} C(n,j) P^j (1-P)^(n-j) = - n · C(n-1,k) · P^k (1-P)^(n-1-k), stated at n = m + 1 so that no ℕ-subtraction appears in the coefficient.

theorem MiscMath.Probability.binTail_deriv_nonpos {m k : ℕ} {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : -((↑m + 1) * (↑(m.choose k) * binShape k m t)) ≤ 0

The tail is nonincreasing in P on [0,1]: the derivative is ≤ 0 there.