The COBRA walk and the BIPS epidemic (EPI-4, model)

Cooper, Radzik, Rivera, The coalescing-branching random walk on expanders and the dual epidemic process, PODC 2016 (arXiv:1602.05768), Section 1.

Both processes run on a finite simple graph G with a branching factor k, and are driven by the same rounds of randomness: in every round each vertex x samples k neighbours, independently and uniformly at random with replacement. A round is an element of the finite type Choices G k, and t i.i.d. uniform rounds are averaged with Dynamics.expList (Choices G k) t.

• COBRA (coalescing-branching random walk): every vertex of the current set C_t pushes to its k sampled neighbours, and C_{t+1} is the set of all vertices pushed to. A vertex is active only when it has just been chosen ("not necessarily for the first time").
• BIPS (biased infection with persistent source v): the source v is always infected, and every other vertex is infected at time t + 1 iff at least one of its k sampled neighbours was infected at time t (an SIS-type epidemic).

def Epidemics.Choices {V : Type u_1} (G : SimpleGraph V) (k : ℕ) : Type u_1

One round of neighbour choices: every vertex x samples k neighbours r x 0, …, r x (k-1). A uniformly random element of this finite product type is exactly the paper's sampling: for every vertex, k neighbours chosen uniformly at random with replacement, independently across vertices (and, through Dynamics.expList, across rounds).

Equations

• Epidemics.Choices G k = ((x : V) → Fin k → ↑(G.neighborSet x))

@[implicit_reducible]

instance Epidemics.instFintypeChoices {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : Fintype (Choices G k)

Rounds of neighbour choices form a finite type, so Dynamics.expList can average over them.

Equations

• Epidemics.instFintypeChoices G k = { elems := Epidemics.instFintypeChoices._aux_1 G k, complete := ⋯ }

theorem Epidemics.choices_nonempty {V : Type u_1} (G : SimpleGraph V) [Nontrivial V] (hG : G.Connected) (k : ℕ) : Nonempty (Choices G k)

On a connected graph with at least two vertices every vertex has a neighbour, so rounds of neighbour choices exist: the processes are well defined on the graphs of the paper, and Dynamics.expList (Choices G k) t is a genuine probability average (its total mass is 1).

def Epidemics.cobraStep {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {k : ℕ} (D : Finset V) (r : Choices G k) : Finset V

One COBRA round (Section 1, "Coalescing Branching Random Walk"): each vertex of D pushes to its k sampled neighbours; the next set consists of all chosen vertices.

Equations

• Epidemics.cobraStep D r = D.biUnion fun (x : V) => Finset.image (fun (i : Fin k) => ↑(r x i)) Finset.univ

def Epidemics.cobraRun {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {k : ℕ} (C : Finset V) (l : List (Choices G k)) : Finset V

COBRA after the rounds l (first round first), started from C₀ = C: the set C_s when l lists the first s rounds.

Equations

• Epidemics.cobraRun C l = List.foldl Epidemics.cobraStep C l

def Epidemics.bipsStep {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {k : ℕ} (v : V) (A : Finset V) (r : Choices G k) : Finset V

One BIPS round with persistent source v (Section 1, "Biased Infection with Persistent Source"): a vertex is infected next iff it is v or one of its k sampled neighbours is in the current infected set A.

Equations

• Epidemics.bipsStep v A r = insert v {u : V | ∃ (i : Fin k), ↑(r u i) ∈ A}

def Epidemics.bipsRun {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {k : ℕ} (v : V) (A₀ : Finset V) (l : List (Choices G k)) : Finset V

BIPS with source v after the rounds l (first round first), started from the infected set A₀; the paper's process starts from A₀ = {v}.

Equations

• Epidemics.bipsRun v A₀ l = List.foldl (Epidemics.bipsStep v) A₀ l