From one cluster to all components: the union bound (EPI-2)

The "furthermore" part of Theorem E.1 of Becchetti, Clementi, Denni, Pasquale, Trevisan, Ziccardi, Percolation and epidemic processes in one-dimensional small-world networks (arXiv:2103.16398): a tail bound β for the cluster of every vertex gives, by a union bound over the vertices (every component is the component of one of its vertices), probability at least 1 - n β that all components are small. The scalar lemma card_mul_exp_le checks that the choice (10 / ε²) log n makes n β ≤ 1 / n for the tail β = exp (ε - ε² t / 2).

theorem Epidemics.prob_components_le_of_tail {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) {L β : ℝ} (hL : 0 ≤ L) (htail : ∀ (s : V), ((coins p h0 h1).prob fun (ω : Sym2 V → Bool) => ⌊L⌋₊ < ((perc G ω).connectedComponentMk s).supp.ncard) ≤ β) : 1 - ↑(Fintype.card V) * β ≤ (coins p h0 h1).prob fun (ω : Sym2 V → Bool) => ∀ (K : (perc G ω).ConnectedComponent), ↑K.supp.ncard ≤ L

Union bound over the components: if the cluster of every vertex has more than ⌊L⌋₊ vertices with probability at most β, then all components have at most L vertices with probability at least 1 - n β.

theorem Epidemics.card_mul_exp_le {n : ℕ} (hn : 2 ≤ n) {ε : ℝ} (hε : 0 < ε) (hε1 : ε < 1) : ↑n * Real.exp (ε - ε ^ 2 * ↑⌊10 / ε ^ 2 * Real.log ↑n⌋₊ / 2) ≤ 1 / ↑n

The union-bound arithmetic: for n ≥ 2 and 0 < ε < 1, the tail exp (ε - ε² t / 2) at t = ⌊(10 / ε²) log n⌋ is at most 1 / n².