Supercritical Reed–Frost epidemics on the complete graph (EPI-3, epidemic reading)

By the pathwise coupling of EPI-1 (final_recovered_iff), the nodes eventually infected by the Reed–Frost epidemic started from a single node v form the connected component of v in the percolated graph perc G ω. On the complete graph K_n with transmission probability p and R₀ = p n > 1, the supercritical giant component (Krivelevich–Sudakov, Theorem 2, and its extension to every ε > 0) thus gives an outbreak of Ω(n) nodes with probability Ω(1): by symmetry, v lies in a component of size ≥ k with probability at least k / n times the probability that such a component exists (prob_component_ge).

R₀ = p n follows the roadmap; the mean number of secondary infections caused by the first infected node is p (n - 1).

theorem Epidemics.card_final_recovered {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ω : Sym2 V → Bool) (v : V) : (run G ω {v} (Fintype.card V)).recovered.card = ((perc G ω).connectedComponentMk v).supp.ncard

Final size (EPI-1): the number of nodes eventually infected from {v} is the size of the connected component of v in the percolated graph.

def Epidemics.percPermIso {V : Type u_1} (ω : Sym2 V → Bool) (σ : Equiv.Perm V) : (perc ⊤ fun (e : Sym2 V) => ω (Sym2.map (⇑σ) e)) ≃g perc ⊤ ω

Relabelling the vertices by σ is an isomorphism perc ⊤ (ω ∘ σ) ≃g perc ⊤ ω.

Equations

• Epidemics.percPermIso ω σ = { toEquiv := σ, map_rel_iff' := ⋯ }

theorem Epidemics.ncard_supp_perm {V : Type u_1} (ω : Sym2 V → Bool) (σ : Equiv.Perm V) (w : V) : ((perc ⊤ fun (e : Sym2 V) => ω (Sym2.map (⇑σ) e)).connectedComponentMk w).supp.ncard = ((perc ⊤ ω).connectedComponentMk (σ w)).supp.ncard

The components of w after relabelling and of σ w before have the same size.

theorem Epidemics.prob_component_ge_eq {V : Type u_1} [Fintype V] [DecidableEq V] (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) (v w : V) (k : ℝ) : ((coins p h0 h1).prob fun (ω : Sym2 V → Bool) => k ≤ ↑((perc ⊤ ω).connectedComponentMk w).supp.ncard) = (coins p h0 h1).prob fun (ω : Sym2 V → Bool) => k ≤ ↑((perc ⊤ ω).connectedComponentMk v).supp.ncard

Symmetry of K_n: the size of the component of a vertex has the same law for all vertices.

theorem Epidemics.prob_component_ge {V : Type u_1} [Fintype V] [DecidableEq V] (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) (v : V) (k : ℝ) : (k / ↑(Fintype.card V) * (coins p h0 h1).prob fun (ω : Sym2 V → Bool) => ∃ (K : (perc ⊤ ω).ConnectedComponent), k ≤ ↑K.supp.ncard) ≤ (coins p h0 h1).prob fun (ω : Sym2 V → Bool) => k ≤ ↑((perc ⊤ ω).connectedComponentMk v).supp.ncard

Symmetry of K_n: the vertex v lies in a component with at least k vertices with probability at least k / n times the probability that such a component exists (the expected number of vertices in such components is n times the former, and at least k times the latter).

theorem Epidemics.reedFrost_large_outbreak_explicit : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε ≤ ε₀ → ∃ (C : ℝ), ∀ (V : Type u_2) [inst : Fintype V] [inst_1 : DecidableEq V] (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1), p * ↑(Fintype.card V) = 1 + ε → ∀ (v : V), ε / 2 - C / ↑(Fintype.card V) ≤ (coins p h0 h1).prob fun (ω : Sym2 V → Bool) => ε * ↑(Fintype.card V) / 2 ≤ ↑(run ⊤ ω {v} (Fintype.card V)).recovered.card

Large outbreak near the threshold, explicit constants (EPI-3, Krivelevich–Sudakov, Theorem 2, via EPI-1): for every small enough ε > 0 there is C such that the Reed–Frost epidemic on the complete graph on n nodes with transmission probability p = (1 + ε) / n (R₀ = p n = 1 + ε), started from any single infected node v, eventually infects at least ε n / 2 nodes with probability at least ε / 2 - C / n.

theorem Epidemics.reedFrost_large_outbreak (R₀ : ℝ) (hR₀ : 1 < R₀) : ∃ (c : ℝ), 0 < c ∧ ∃ (q : ℝ), 0 < q ∧ ∃ (n₀ : ℕ), ∀ (V : Type u_2) [inst : Fintype V] [inst_1 : DecidableEq V], n₀ ≤ Fintype.card V → ∀ (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1), p * ↑(Fintype.card V) = R₀ → ∀ (v : V), q ≤ (coins p h0 h1).prob fun (ω : Sym2 V → Bool) => c * ↑(Fintype.card V) ≤ ↑(run ⊤ ω {v} (Fintype.card V)).recovered.card

Large outbreak (EPI-3, epidemic reading of the supercritical giant component, via EPI-1): for every R₀ > 1 there are c > 0, q > 0 and n₀ such that the Reed–Frost epidemic on the complete graph on n ≥ n₀ nodes with transmission probability p = R₀ / n, started from any single infected node v, eventually infects at least c n nodes with probability at least q: Ω(n) nodes with probability Ω(1).