Binomial tails and the Chernoff bound of Theorem E.1 (EPI-2)

The tail binTail p m k of the number of successes in m independent Bernoulli(p) trials (the coin Distribution.bernoulli of the Chernoff bounds of dynamics/), its one-step recursion (condition on the first trial), and the Chernoff bound used in the proof of Theorem E.1 of Becchetti, Clementi, Denni, Pasquale, Trevisan, Ziccardi, Percolation and epidemic processes in one-dimensional small-world networks (arXiv:2103.16398).

The paper tilts by ε rather than by the optimal log (1 + δ), which gives its closed form exp (ε - ε² t / 2). Markov's inequality on exp (ε X) and the bound on the moment-generating function are the core's Distribution.prob_ge_le_exp (Dynamics.ChernoffAux, FND-3); only the scalar inequality (1 - ε) e^ε ≤ 1 - ε² / 2 and the arithmetic of the paper's constants are local.

noncomputable def Epidemics.binTail (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) (m k : ℕ) : ℝ

The tail of a binomial distribution: the probability of at least k successes in m independent Bernoulli(p) trials.

Equations

• Epidemics.binTail p h0 h1 m k = (Dynamics.Distribution.independent fun (x : Fin m) => Dynamics.Distribution.bernoulli p h0 h1).prob fun (ξ : Fin m → Bool) => k ≤ {i : Fin m | ξ i = true}.card

theorem Epidemics.binTail_zero_right {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) (m : ℕ) : binTail p h0 h1 m 0 = 1

theorem Epidemics.binTail_nonneg {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) (m k : ℕ) : 0 ≤ binTail p h0 h1 m k

theorem Epidemics.card_filter_cons {m : ℕ} (b : Bool) (r : Fin m → Bool) : {i : Fin (m + 1) | Fin.cons b r i = true}.card = (if b = true then 1 else 0) + {i : Fin m | r i = true}.card

Successes among b followed by r.

theorem Epidemics.independent_prob_fin_succ {β : Type u_1} [Fintype β] {m : ℕ} (q : Dynamics.Distribution β) (s : (Fin (m + 1) → β) → Prop) : (Dynamics.Distribution.independent fun (x : Fin (m + 1)) => q).prob s = ∑ b : β, q.weight b * (Dynamics.Distribution.independent fun (x : Fin m) => q).prob fun (r : Fin m → β) => s (Fin.cons b r)

Probabilities under an i.i.d. product over Fin (m + 1), conditioned on the first trial.

theorem Epidemics.binTail_succ_succ {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) (m k : ℕ) : binTail p h0 h1 (m + 1) (k + 1) = p * binTail p h0 h1 m k + (1 - p) * binTail p h0 h1 m (k + 1)

One-step recursion of the binomial tail: condition on the first trial.

theorem Epidemics.one_sub_mul_exp_le {ε : ℝ} (hε : 0 ≤ ε) (hε1 : ε < 1) : (1 - ε) * Real.exp ε ≤ 1 - ε ^ 2 / 2

The key scalar inequality (1 - ε) e^ε ≤ 1 - ε² / 2 for 0 ≤ ε < 1.

theorem Epidemics.binomial_tail_le {d : ℕ} {p ε : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) (hε : 0 < ε) (hε1 : ε < 1) (hp : p * (↑d - 1) ≤ 1 - ε) (t : ℕ) : ((Dynamics.Distribution.independent fun (x : Fin (t * (d - 1) + 1)) => Dynamics.Distribution.bernoulli p h0 h1).prob fun (ξ : Fin (t * (d - 1) + 1) → Bool) => t ≤ {i : Fin (t * (d - 1) + 1) | ξ i = true}.card) ≤ Real.exp (ε - ε ^ 2 * ↑t / 2)

Chernoff bound for the proof of Theorem E.1: if p (d - 1) ≤ 1 - ε with 0 < ε < 1, then at least t successes among t (d - 1) + 1 independent Bernoulli(p) trials occur with probability at most exp (ε - ε² t / 2).