Counting positive answers among i.i.d. trials (EPI-3)

The probabilistic half of the proofs of Krivelevich–Sudakov (The phase transition in random graphs: a simple proof, Random Structures & Algorithms 43 (2013), arXiv:1201.6529): Lemma 1, part 2, with the Chernoff bounds of FND-3 (Dynamics.Chernoff) in place of Chebyshev's inequality, as suggested in the paper's Discussion, item 1.

The trials are x : Fin m → Bool under independent (fun _ => bernoulli p), listed as List.ofFn x, so that ((List.ofFn x).take t).count true is the number of successes among the first t trials (count_take_ofFn).

• prob_count_take_le, prob_count_take_ge: lower and upper tails for the first t trials.
• prob_count_take_far: Lemma 1, part 2.
• Good, prob_not_good_le: the typical properties used in the proof of Theorem 2 (the counts at times t₁ and N₀, and at every time between them, are close to their means).
• pow_three_mul_exp_neg_le: x³ e^{-κx} ≤ 6 / κ³, to turn exponential bounds into C / n.

theorem Epidemics.count_take_ofFn {m : ℕ} (x : Fin m → Bool) (t : ℕ) : List.count true (List.take t (List.ofFn x)) = {j ∈ {j : Fin m | ↑j < t} | x j = true}.card

The number of successes among the first t trials.

theorem Epidemics.sum_filter_lt {m t : ℕ} (ht : t ≤ m) (p : ℝ) : ∑ _i : Fin m with ↑_i < t, p = ↑t * p

theorem Epidemics.prob_count_take_le (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) {m t : ℕ} (ht : t ≤ m) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 1) : ((Dynamics.Distribution.independent fun (x : Fin m) => Dynamics.Distribution.bernoulli p h0 h1).prob fun (x : Fin m → Bool) => ↑(List.count true (List.take t (List.ofFn x))) ≤ (1 - δ) * (↑t * p)) ≤ Real.exp (-(δ ^ 2 * (↑t * p) / 2))

Lower tail for the first t ≤ m trials (Chernoff, FND-3): P(∑_{i<t} Xᵢ ≤ (1 - δ) t p) ≤ exp (-δ² t p / 2).

theorem Epidemics.prob_count_take_ge (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) {m t : ℕ} (ht : t ≤ m) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 1) : ((Dynamics.Distribution.independent fun (x : Fin m) => Dynamics.Distribution.bernoulli p h0 h1).prob fun (x : Fin m → Bool) => (1 + δ) * (↑t * p) ≤ ↑(List.count true (List.take t (List.ofFn x)))) ≤ Real.exp (-(δ ^ 2 * (↑t * p) / 3))

Upper tail for the first t ≤ m trials (Chernoff, FND-3): P(∑_{i<t} Xᵢ ≥ (1 + δ) t p) ≤ exp (-δ² t p / 3) for δ < 1.

theorem Epidemics.prob_count_take_far (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) {m N₀ : ℕ} (hN₀ : N₀ ≤ m) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 1) : ((Dynamics.Distribution.independent fun (x : Fin m) => Dynamics.Distribution.bernoulli p h0 h1).prob fun (x : Fin m → Bool) => δ * (↑N₀ * p) ≤ |↑(List.count true (List.take N₀ (List.ofFn x))) - ↑N₀ * p|) ≤ 2 * Real.exp (-(δ ^ 2 * (↑N₀ * p) / 3))

Krivelevich–Sudakov, Lemma 1, part 2, with the Chernoff bounds (FND-3) instead of Chebyshev's inequality, as in their Discussion, item 1: among the first N₀ of m i.i.d. Bernoulli(p) trials, the number of successes deviates from its mean N₀ p by at least δ N₀ p with probability at most 2 exp (-δ² N₀ p / 3).

def Epidemics.Good (p : ℝ) (N₀ t₁ : ℕ) (δ : ℝ) (L : List Bool) : Prop

The typical behaviour of the answers used in the proof of Theorem 2: the numbers of positive answers among the first N₀ and the first t₁ are at most (1 + δ) times their means, and among the first t at least (1 - δ) times the mean for every t₁ ≤ t ≤ N₀.

Equations

• One or more equations did not get rendered due to their size.

theorem Epidemics.prob_not_good_le (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) {N₀ t₁ : ℕ} (ht₁ : t₁ ≤ N₀) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 1) : ((Dynamics.Distribution.independent fun (x : Fin N₀) => Dynamics.Distribution.bernoulli p h0 h1).prob fun (x : Fin N₀ → Bool) => ¬Good p N₀ t₁ δ (List.ofFn x)) ≤ (↑N₀ + 3) * Real.exp (-(δ ^ 2 * (↑t₁ * p) / 3))

The answers are typical except with probability (N₀ + 3) exp (-δ² t₁ p / 3).

theorem Epidemics.pow_three_mul_exp_neg_le {κ : ℝ} (hκ : 0 < κ) {x : ℝ} (hx : 0 ≤ x) : x ^ 3 * Real.exp (-(κ * x)) ≤ 6 / κ ^ 3

x³ e^{-κx} ≤ 6 / κ³ for κ > 0, x ≥ 0.