Subcritical percolation and small outbreaks (EPI-2)

Becchetti, Clementi, Denni, Pasquale, Trevisan, Ziccardi, Percolation and epidemic processes in one-dimensional small-world networks ([BCDPTZ22], arXiv:2103.16398), Theorem 2.3 and its proof, Theorem E.1.

Let the degrees of a finite graph G be at most d, and percolate G with independent Bernoulli(p) coins (coins, from EPI-1), where p (d - 1) ≤ 1 - ε. Explore the cluster of a vertex s (its connected component in perc G ω) one vertex at a time. The first t steps examine at most t (d - 1) + 1 edges, each for the first time, and the cluster has more than t vertices only if at least t of them are open. By the principle of deferred decisions, the cluster size is dominated by a binomial tail, which a Chernoff bound turns into exp (ε - ε² t / 2); a union bound over s gives clusters of at most (10 / ε²) log n vertices with probability at least 1 - 1/n.

Corollaries:

• by the pathwise Reed–Frost ⇔ percolation coupling (EPI-1), a Reed–Frost epidemic with R₀ = p (d - 1) ≤ 1 - ε infects at most |I₀| (10 / ε²) log n nodes and is over within (10 / ε²) log n rounds, with probability at least 1 - 1/n;
• every component of the Erdős–Rényi graph G(n, c/n) with c ≤ 1 - ε (bond percolation on the complete graph) has at most (10 / ε²) log n vertices, with probability at least 1 - 1/n.

Component sizes are measured as in Mathlib, by K.supp.ncard.

theorem Epidemics.prob_cluster_gt_le_binomial {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {d : ℕ} (hdeg : ∀ (v : V), G.degree v ≤ d) {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) (s : V) (t : ℕ) : ((coins p h0 h1).prob fun (ω : Sym2 V → Bool) => t < ((perc G ω).connectedComponentMk s).supp.ncard) ≤ (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

Deferred decisions (the proof of [BCDPTZ22, Theorem E.1]): if the degrees of G are at most d, the cluster of s in the percolated graph has more than t vertices with probability at most that of at least t successes in t (d - 1) + 1 independent Bernoulli(p) trials.

theorem Epidemics.prob_cluster_gt_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {d : ℕ} (hdeg : ∀ (v : V), G.degree v ≤ d) {p ε : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) (hε : 0 < ε) (hε1 : ε < 1) (hp : p * (↑d - 1) ≤ 1 - ε) (s : V) (t : ℕ) : ((coins p h0 h1).prob fun (ω : Sym2 V → Bool) => t < ((perc G ω).connectedComponentMk s).supp.ncard) ≤ Real.exp (ε - ε ^ 2 * ↑t / 2)

Theorem E.1, first part ([BCDPTZ22]): if the degrees of G are at most d and p (d - 1) ≤ 1 - ε with 0 < ε < 1, the cluster of any vertex s in the percolated graph has more than t vertices with probability at most exp (ε - ε² t / 2).

theorem Epidemics.prob_components_small {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {d : ℕ} (hdeg : ∀ (v : V), G.degree v ≤ d) {p ε : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) (hε : 0 < ε) (hε1 : ε < 1) (hp : p * (↑d - 1) ≤ 1 - ε) : 1 - 1 / ↑(Fintype.card V) ≤ (coins p h0 h1).prob fun (ω : Sym2 V → Bool) => ∀ (K : (perc G ω).ConnectedComponent), ↑K.supp.ncard ≤ 10 / ε ^ 2 * Real.log ↑(Fintype.card V)

Theorem 2.3 ([BCDPTZ22]; Theorem E.1, second part): if the degrees of G are at most d and p (d - 1) ≤ 1 - ε with 0 < ε < 1, then with probability at least 1 - 1/n every connected component of the percolated graph has at most (10 / ε²) log n vertices, where n = |V|.

theorem Epidemics.reedFrost_subcritical {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {d : ℕ} (hdeg : ∀ (v : V), G.degree v ≤ d) {p ε : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) (hε : 0 < ε) (hε1 : ε < 1) (hR₀ : p * (↑d - 1) ≤ 1 - ε) (I₀ : Finset V) : 1 - 1 / ↑(Fintype.card V) ≤ (coins p h0 h1).prob fun (ω : Sym2 V → Bool) => ↑(run G ω I₀ (Fintype.card V)).recovered.card ≤ ↑I₀.card * (10 / ε ^ 2 * Real.log ↑(Fintype.card V)) ∧ (run G ω I₀ ⌊10 / ε ^ 2 * Real.log ↑(Fintype.card V)⌋₊).infected = ∅

Subcritical Reed–Frost (the bounded-degree statement whose formal version [BCDPTZ22] omits after Theorem 2.5; compare claim 2 of Theorems 2.4 and 2.5): if the degrees of G are at most d and the reproduction number R₀ = p (d - 1) is at most 1 - ε with 0 < ε < 1, then with probability at least 1 - 1/n the epidemic started from I₀ infects at most |I₀| (10 / ε²) log n nodes in total, and nobody is infected in round ⌊(10 / ε²) log n⌋: the epidemic is over by then.

theorem Epidemics.erdosRenyi_subcritical {V : Type u_1} [Fintype V] [DecidableEq V] {c ε : ℝ} (hε : 0 < ε) (hε1 : ε < 1) (hc : c ≤ 1 - ε) (h0 : 0 ≤ c / ↑(Fintype.card V)) (h1 : c / ↑(Fintype.card V) ≤ 1) : 1 - 1 / ↑(Fintype.card V) ≤ (coins (c / ↑(Fintype.card V)) h0 h1).prob fun (ω : Sym2 V → Bool) => ∀ (K : (perc ⊤ ω).ConnectedComponent), ↑K.supp.ncard ≤ 10 / ε ^ 2 * Real.log ↑(Fintype.card V)

Subcritical Erdős–Rényi graphs (Theorem 2.3 for the complete graph): if c ≤ 1 - ε with 0 < ε < 1, then with probability at least 1 - 1/n every connected component of G(n, c/n) has at most (10 / ε²) log n vertices.