Reed–Frost epidemics and bond percolation, pathwise (EPI-1)

The Reed–Frost (Independent Cascade) epidemic on a finite graph G: in every round, each infected node infects each susceptible neighbour across the edge between them if that edge is open, and then recovers for good. Every edge carries a single coin ω e : Bool, flipped once and for all (true = open). The open edges form the percolated graph perc G ω.

Pathwise, for every coin assignment, the nodes infected in round t are exactly those at distance t from the initial set I₀ in perc G ω, and the recovered ones those at distance < t; the epidemic is over after card V rounds, and its final recovered set is the set of nodes connected to I₀ by open edges. With i.i.d. Bernoulli(p) coins, the probability that a node is eventually infected is the probability that bond percolation connects it to I₀.

def Epidemics.perc {V : Type u_1} (G : SimpleGraph V) (ω : Sym2 V → Bool) : SimpleGraph V

The percolated graph: the edges of G whose coin is true.

Equations

• Epidemics.perc G ω = { Adj := fun (u v : V) => G.Adj u v ∧ ω s(u, v) = true, symm := ⋯, loopless := ⋯ }

structure Epidemics.SIR (V : Type u_2) : Type u_2

Infected and recovered nodes; the others are susceptible.

• infected : Finset V
• recovered : Finset V

def Epidemics.step {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ω : Sym2 V → Bool) (s : SIR V) : SIR V

One round: a susceptible node becomes infected if it has an infected neighbour across an open edge; every infected node recovers.

Equations

• Epidemics.step G ω s = { infected := {v : V | v ∉ s.infected ∧ v ∉ s.recovered ∧ ∃ u ∈ s.infected, G.Adj u v ∧ ω s(u, v) = true}, recovered := s.recovered ∪ s.infected }

def Epidemics.run {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ω : Sym2 V → Bool) (I₀ : Finset V) : ℕ → SIR V

The epidemic started from the infected set I₀, with nobody recovered.

Equations

• Epidemics.run G ω I₀ 0 = { infected := I₀, recovered := ∅ }
• Epidemics.run G ω I₀ t.succ = Epidemics.step G ω (Epidemics.run G ω I₀ t)

noncomputable def Epidemics.setDist {V : Type u_1} (H : SimpleGraph V) (I₀ : Finset V) (v : V) : ℕ∞

Distance from the set I₀ in a graph H (⊤ if v is not connected to I₀).

Equations

• Epidemics.setDist H I₀ v = ⨅ u ∈ I₀, H.edist u v

theorem Epidemics.setDist_eq_subtype {V : Type u_1} (H : SimpleGraph V) (I₀ : Finset V) (v : V) : setDist H I₀ v = ⨅ (u : ↑↑I₀), H.edist (↑u) v

theorem Epidemics.setDist_eq_zero_iff {V : Type u_1} (H : SimpleGraph V) (I₀ : Finset V) {v : V} : setDist H I₀ v = 0 ↔ v ∈ I₀

theorem Epidemics.setDist_le_add_one {V : Type u_1} (H : SimpleGraph V) (I₀ : Finset V) {u v : V} (huv : H.Adj u v) : setDist H I₀ v ≤ setDist H I₀ u + 1

theorem Epidemics.exists_edist_eq_setDist {V : Type u_1} (H : SimpleGraph V) (I₀ : Finset V) {v : V} (h : setDist H I₀ v ≠ ⊤) : ∃ u ∈ I₀, H.edist u v = setDist H I₀ v

theorem Epidemics.exists_adj_of_setDist_succ {V : Type u_1} (H : SimpleGraph V) (I₀ : Finset V) {v : V} {t : ℕ} (h : setDist H I₀ v = ↑t + 1) : ∃ (u : V), H.Adj u v ∧ setDist H I₀ u = ↑t

theorem Epidemics.setDist_ne_top_iff {V : Type u_1} (H : SimpleGraph V) (I₀ : Finset V) {v : V} : setDist H I₀ v ≠ ⊤ ↔ ∃ u ∈ I₀, H.Reachable u v

theorem Epidemics.setDist_lt_card {V : Type u_1} [Fintype V] (H : SimpleGraph V) (I₀ : Finset V) {v : V} (h : setDist H I₀ v ≠ ⊤) : setDist H I₀ v < ↑(Fintype.card V)

theorem Epidemics.infected_recovered_iff {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ω : Sym2 V → Bool) (I₀ : Finset V) (t : ℕ) (v : V) : (v ∈ (run G ω I₀ t).infected ↔ setDist (perc G ω) I₀ v = ↑t) ∧ (v ∈ (run G ω I₀ t).recovered ↔ setDist (perc G ω) I₀ v < ↑t)

theorem Epidemics.infected_iff {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ω : Sym2 V → Bool) (I₀ : Finset V) (t : ℕ) (v : V) : v ∈ (run G ω I₀ t).infected ↔ setDist (perc G ω) I₀ v = ↑t

Pathwise layers: the nodes infected in round t are those at percolation distance t.

theorem Epidemics.recovered_iff {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ω : Sym2 V → Bool) (I₀ : Finset V) (t : ℕ) (v : V) : v ∈ (run G ω I₀ t).recovered ↔ setDist (perc G ω) I₀ v < ↑t

The nodes recovered by round t are those at percolation distance < t.

theorem Epidemics.no_infected_of_dist_lt {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ω : Sym2 V → Bool) (I₀ : Finset V) (t : ℕ) (h : ∀ (v : V), setDist (perc G ω) I₀ v ≠ ⊤ → setDist (perc G ω) I₀ v < ↑t) : (run G ω I₀ t).infected = ∅

theorem Epidemics.extinct {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ω : Sym2 V → Bool) (I₀ : Finset V) (t : ℕ) (ht : Fintype.card V ≤ t) : (run G ω I₀ t).infected = ∅

The epidemic is over after card V rounds.

theorem Epidemics.final_recovered_iff {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ω : Sym2 V → Bool) (I₀ : Finset V) (v : V) : v ∈ (run G ω I₀ (Fintype.card V)).recovered ↔ ∃ u ∈ I₀, (perc G ω).Reachable u v

Final size: the eventually recovered nodes are those connected to I₀ by open edges.

noncomputable def Epidemics.bernoulli (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) : Dynamics.Distribution Bool

A biased coin: true with probability p.

Equations

• Epidemics.bernoulli p h0 h1 = { weight := fun (b : Bool) => if b = true then p else 1 - p, nonneg := ⋯, sum_one := ⋯ }

noncomputable def Epidemics.coins {V : Type u_1} [Fintype V] [DecidableEq V] (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) : Dynamics.Distribution (Sym2 V → Bool)

Independent Bernoulli(p) coins, one per unordered pair of nodes.

Equations

• Epidemics.coins p h0 h1 = Dynamics.Distribution.independent fun (x : Sym2 V) => Epidemics.bernoulli p h0 h1

theorem Epidemics.coins_prob_open {V : Type u_1} [Fintype V] [DecidableEq V] (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) (e : Sym2 V) : ((coins p h0 h1).prob fun (ω : Sym2 V → Bool) => ω e = true) = p

The coin of a single pair is open with probability p.

theorem Epidemics.prob_infected_eq_prob_connected {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) (I₀ : Finset V) (v : V) : ((coins p h0 h1).prob fun (ω : Sym2 V → Bool) => v ∈ (run G ω I₀ (Fintype.card V)).recovered) = (coins p h0 h1).prob fun (ω : Sym2 V → Bool) => ∃ u ∈ I₀, (perc G ω).Reachable u v

Reed–Frost ⇔ bond percolation: the probability that v is eventually infected equals the probability that v is connected to I₀ in the percolated graph.

theorem Epidemics.extinct_of_dist_lt {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ω : Sym2 V → Bool) (I₀ : Finset V) (t : ℕ) (h : ∀ (v : V), setDist (perc G ω) I₀ v ≠ ⊤ → setDist (perc G ω) I₀ v < ↑t) : (run G ω I₀ t).infected = ∅

The epidemic cannot outlast the percolation distances: if every node connected to I₀ is at distance < t, nobody is infected in round t.