Exploring a percolation cluster: deferred decisions (EPI-2)

The crux of the proof of Theorem E.1 of Becchetti, Clementi, Denni, Pasquale, Trevisan, Ziccardi, Percolation and epidemic processes in one-dimensional small-world networks (arXiv:2103.16398): the cluster of a vertex in bond percolation on a graph of maximum degree d is explored one edge at a time, each coin being looked at only when its edge is examined, so the cluster size is dominated by a binomial tail.

Instead of running an explicit BFS, we prove a statement about every state of an exploration: a set D of discovered vertices and a set X of examined pairs, whose coins are forced closed (closeOff X ω; an examined open edge has both endpoints in D, so closing it is harmless). The frontier counts the unexamined edges of G leaving D. Theorem prob_reachSet_le_binTail: if frontier G D X + (k - 1)(d - 1) ≤ m, then D reaches at least k new vertices with probability at most binTail p m k. The induction on m conditions on the coin of one frontier edge {w, x} (coins_prob_split):

• closed: the state becomes (D, X ∪ {wx}) and the frontier loses one edge;
• open: the state becomes (D ∪ {x}, X ∪ {wx}), one vertex is found, and the frontier gains at most d - 1 edges at x while losing wx; which matches the recursion binTail_succ_succ. Starting from ({s}, ∅), whose frontier is at most d, gives the bound binTail p (t (d - 1) + 1) t for t < |C(s)|.

Closing examined coins

def Epidemics.closeOff {V : Type u_1} [DecidableEq V] (X : Finset (Sym2 V)) (ω : Sym2 V → Bool) : Sym2 V → Bool

The coins with every pair of X forced closed.

Equations

• Epidemics.closeOff X ω e = (ω e && decide (e ∉ X))

theorem Epidemics.closeOff_empty {V : Type u_1} [DecidableEq V] (ω : Sym2 V → Bool) : closeOff ∅ ω = ω

theorem Epidemics.perc_closeOff_adj {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {X : Finset (Sym2 V)} {ω : Sym2 V → Bool} {u v : V} : (perc G (closeOff X ω)).Adj u v ↔ G.Adj u v ∧ ω s(u, v) = true ∧ s(u, v) ∉ X

theorem Epidemics.closeOff_update_false {V : Type u_1} [DecidableEq V] (X : Finset (Sym2 V)) (ω : Sym2 V → Bool) (e : Sym2 V) : closeOff X (Function.update ω e false) = closeOff (insert e X) ω

A closed examined coin is the same as a forced-closed one.

The frontier of an exploration state

def Epidemics.frontier {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (D : Finset V) (X : Finset (Sym2 V)) : ℕ

The unexamined edges of G leaving D, counted from their endpoint in D.

Equations

• Epidemics.frontier G D X = ∑ u ∈ D, {v : V | v ∉ D ∧ G.Adj u v ∧ s(u, v) ∉ X}.card

theorem Epidemics.mem_of_frontier_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {D : Finset V} {X : Finset (Sym2 V)} (h : frontier G D X = 0) {u v : V} (hu : u ∈ D) (hv : v ∉ D) (hadj : G.Adj u v) : s(u, v) ∈ X

theorem Epidemics.exists_of_frontier_ne_zero {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {D : Finset V} {X : Finset (Sym2 V)} (h : frontier G D X ≠ 0) : ∃ w ∈ D, ∃ x ∉ D, G.Adj w x ∧ s(w, x) ∉ X

theorem Epidemics.sum_card_lt_frontier {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {D D' : Finset V} {X : Finset (Sym2 V)} (hD : D ⊆ D') {w x : V} (hw : w ∈ D) (hx : x ∉ D) (hadj : G.Adj w x) (hX : s(w, x) ∉ X) : ∑ u ∈ D, {v : V | v ∉ D' ∧ G.Adj u v ∧ s(u, v) ∉ insert s(w, x) X}.card < frontier G D X

Examining the frontier edge {w, x} removes it from the count of w, whether or not x is added to the discovered set.

theorem Epidemics.frontier_insert_edge_lt {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {D : Finset V} {X : Finset (Sym2 V)} {w x : V} (hw : w ∈ D) (hx : x ∉ D) (hadj : G.Adj w x) (hX : s(w, x) ∉ X) : frontier G D (insert s(w, x) X) < frontier G D X

Closed branch: the frontier loses the examined edge.

theorem Epidemics.frontier_insert_vertex_le {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} (hdeg : ∀ (v : V), G.degree v ≤ d) {D : Finset V} {X : Finset (Sym2 V)} {w x : V} (hw : w ∈ D) (hx : x ∉ D) (hadj : G.Adj w x) (hX : s(w, x) ∉ X) : frontier G (insert x D) (insert s(w, x) X) + 1 ≤ frontier G D X + (d - 1)

Open branch: the new vertex x brings at most d - 1 new frontier edges, and the examined edge leaves the frontier.

theorem Epidemics.frontier_singleton_le {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} (hdeg : ∀ (v : V), G.degree v ≤ d) (s : V) : frontier G {s} ∅ ≤ d

The initial frontier ({s}, ∅) has at most d edges.

theorem Epidemics.reachSet_closeOff_eq_self {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {D : Finset V} {X : Finset (Sym2 V)} (h : frontier G D X = 0) (ω : Sym2 V → Bool) : reachSet (perc G (closeOff X ω)) D = D

With an empty frontier, the discovered set is the whole cluster.

theorem Epidemics.reachSet_update_true {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {D : Finset V} {X : Finset (Sym2 V)} {w x : V} (hw : w ∈ D) (hadj : G.Adj w x) (hX : s(w, x) ∉ X) (ω : Sym2 V → Bool) : reachSet (perc G (closeOff X (Function.update ω s(w, x) true))) D = reachSet (perc G (closeOff (insert s(w, x) X) ω)) (insert x D)

Open branch, pathwise: if the frontier edge {w, x} is open, the cluster of D is the cluster of D ∪ {x} with that edge examined.

Deferred decisions

theorem Epidemics.coins_prob_update {V : Type u_1} [Fintype V] [DecidableEq V] {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) (e : Sym2 V) (s : (Sym2 V → Bool) → Prop) : (coins p h0 h1).prob s = (p * (coins p h0 h1).prob fun (ω : Sym2 V → Bool) => s (Function.update ω e true)) + (1 - p) * (coins p h0 h1).prob fun (ω : Sym2 V → Bool) => s (Function.update ω e false)

Conditioning the percolation coins on the coin of one pair.

theorem Epidemics.prob_reachSet_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) {D : Finset V} {X : Finset (Sym2 V)} (hF : frontier G D X = 0) (k : ℕ) : ((coins p h0 h1).prob fun (ω : Sym2 V → Bool) => D.card + (k + 1) ≤ (reachSet (perc G (closeOff X ω)) D).card) = 0

With an empty frontier, no new vertex is ever found.

theorem Epidemics.prob_reachSet_le_binTail {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) (hdeg : ∀ (v : V), G.degree v ≤ d) (m : ℕ) (D : Finset V) (X : Finset (Sym2 V)) (k : ℕ) : frontier G D X + (k - 1) * (d - 1) ≤ m → ((coins p h0 h1).prob fun (ω : Sym2 V → Bool) => D.card + k ≤ (reachSet (perc G (closeOff X ω)) D).card) ≤ binTail p h0 h1 m k

Deferred decisions, for every exploration state: if frontier G D X + (k - 1)(d - 1) ≤ m, then the cluster of D with the pairs of X closed has at least |D| + k vertices with probability at most binTail p m k.

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

Deferred decisions (the proof of [BCDPTZ22, Theorem E.1]): the cluster of s has more than t vertices with probability at most binTail p (t (d - 1) + 1) t.