Clusters of a set of vertices (EPI-2)

The reachable set reachSet H D of a finite set D of vertices: the vertices joined to D by a path in H. For a single vertex it is the vertex set of its connected component, measured in Mathlib by (H.connectedComponentMk s).supp.ncard; for the initial set I₀ of a Reed–Frost epidemic in the percolated graph it is the final outbreak (EPI-1).

This file collects the pathwise facts used by the subcritical percolation proofs:

• how the reachable set behaves when D is closed under H, when a neighbour is added to D, and when H loses edges whose endpoints lie in D;
• the distance between two vertices of a component is smaller than its size;
• small components force a small final outbreak and an early end of the Reed–Frost epidemic.

noncomputable def Epidemics.reachSet {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) (D : Finset V) : Finset V

The vertices joined to some vertex of D by a path in H.

Equations

• Epidemics.reachSet H D = {v : V | ∃ u ∈ D, H.Reachable u v}

theorem Epidemics.mem_reachSet {V : Type u_1} [Fintype V] [DecidableEq V] {H : SimpleGraph V} {D : Finset V} {v : V} : v ∈ reachSet H D ↔ ∃ u ∈ D, H.Reachable u v

theorem Epidemics.subset_reachSet {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) (D : Finset V) : D ⊆ reachSet H D

theorem Epidemics.mem_of_walk {V : Type u_1} {H : SimpleGraph V} {D : Finset V} (h : ∀ u ∈ D, ∀ (v : V), H.Adj u v → v ∈ D) {u v : V} : ∀ (a : H.Walk u v), u ∈ D → v ∈ D

A walk starting in a set closed under the edges of H stays in it.

theorem Epidemics.reachSet_eq_self {V : Type u_1} [Fintype V] [DecidableEq V] {H : SimpleGraph V} {D : Finset V} (h : ∀ u ∈ D, ∀ (v : V), H.Adj u v → v ∈ D) : reachSet H D = D

A set closed under the edges of H is its own reachable set.

theorem Epidemics.reachSet_insert {V : Type u_1} [Fintype V] [DecidableEq V] {H : SimpleGraph V} {D : Finset V} {w x : V} (hw : w ∈ D) (hwx : H.Adj w x) : reachSet H (insert x D) = reachSet H D

Adding a neighbour of D to D does not change the reachable set.

theorem Epidemics.reachable_or_of_walk {V : Type u_1} {H H' : SimpleGraph V} {S : Finset V} (hle : H' ≤ H) (hS : ∀ (u v : V), H.Adj u v → ¬H'.Adj u v → v ∈ S) {u v : V} : ∀ (a : H.Walk u v), H'.Reachable u v ∨ ∃ u' ∈ S, H'.Reachable u' v

A walk of H either survives in a subgraph H' that only misses edges ending in S, or its end is reached in H' from a vertex of S.

theorem Epidemics.reachSet_eq_of_le {V : Type u_1} [Fintype V] [DecidableEq V] {H H' : SimpleGraph V} {S : Finset V} (hle : H' ≤ H) (hS : ∀ (u v : V), H.Adj u v → ¬H'.Adj u v → v ∈ S) : reachSet H' S = reachSet H S

Deleting edges of H whose endpoints lie in S does not change the reachable set of S.

theorem Epidemics.ncard_supp_eq_card_reachSet {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) (s : V) : (H.connectedComponentMk s).supp.ncard = (reachSet H {s}).card

The component of s has as many vertices as the reachable set of {s}.

theorem Epidemics.dist_lt_ncard_supp {V : Type u_1} [Fintype V] [DecidableEq V] {H : SimpleGraph V} {u v : V} (h : H.Reachable u v) : H.dist u v < (H.connectedComponentMk u).supp.ncard

Two vertices of a component are at distance smaller than its number of vertices.

theorem Epidemics.card_reachSet_le {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) (I₀ : Finset V) {L : ℝ} (h : ∀ (u : V), ↑(H.connectedComponentMk u).supp.ncard ≤ L) : ↑(reachSet H I₀).card ≤ ↑I₀.card * L

The reachable set of I₀ has at most |I₀| times the largest component size.

theorem Epidemics.card_recovered_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ω : Sym2 V → Bool) (I₀ : Finset V) {L : ℝ} (h : ∀ (u : V), ↑((perc G ω).connectedComponentMk u).supp.ncard ≤ L) : ↑(run G ω I₀ (Fintype.card V)).recovered.card ≤ ↑I₀.card * L

Final size from component sizes: if every component of the percolated graph has at most L vertices, the Reed–Frost epidemic from I₀ infects at most |I₀| L nodes.

theorem Epidemics.infected_eq_empty_of_ncard_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ω : Sym2 V → Bool) (I₀ : Finset V) {k : ℕ} (h : ∀ (u : V), ((perc G ω).connectedComponentMk u).supp.ncard ≤ k) : (run G ω I₀ k).infected = ∅

Duration from component sizes: if every component of the percolated graph has at most k vertices, nobody is infected in round k of the Reed–Frost epidemic.