Total spreading time, upper bound (Theorems 21 and 31 composed through Lemma 19)

Three stages, composed by tail_compose:

1. growth from a nonempty set to f n informed nodes within ⌈log_{1+γ} n⌉ + r rounds (Theorem 21, growth_upper_tail);
2. from f n informed nodes to at most g n uninformed ones within r rounds, when every uninformed node is informed with probability at least p in between (Lemma 19, notYet_middle_le, prefactor (1 - f) / g);
3. from at most g n uninformed nodes to none within ⌈ln n / ρ⌉ + r rounds (Theorem 31, notYet_shrink_le).

The expectation follows from the tail by sum_notYet_le_of_tail.

theorem Epidemics.Revisited.notYet_middle_le {n : ℕ} (P : RumorProcess n) {f g p : ℝ} (hf1 : f < 1) (hg0 : 0 < g) (hp0 : 0 < p) (hp1 : p ≤ 1) (hn : 0 < ↑n) (hmid : ∀ (S : Finset (Fin n)), f * ↑n ≤ ↑S.card → g * ↑n < ↑n - ↑S.card → ∀ x ∉ S, p ≤ P.informProb S x) (S : Finset (Fin n)) (hS : f * ↑n ≤ ↑S.card) (r : ℕ) : P.notYet (↑n - g * ↑n) r S ≤ (1 - f) / g * Real.exp (-p * ↑r)

The middle stage (Lemma 19): from at least f n informed nodes, more than g n nodes are still uninformed after r rounds with probability at most ((1 - f) / g) e^{-p r}.

theorem Epidemics.Revisited.spreading_upper_tail_proof {γlo γhi a b c f ρlo ρhi a' c' g p : ℝ} (hγlo : 0 < γlo) (hγ : γlo ≤ γhi) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hf0 : 0 < f) (hf1 : f < 1) (haf : a * f < 1) (hρlo : 0 < ρlo) (hρ : ρlo ≤ ρhi) (ha' : 0 ≤ a') (hc' : 0 ≤ c') (hg0 : 0 < g) (hag : Real.exp (-ρlo) + a' * g < 1) (hp0 : 0 < p) (hp1 : p ≤ 1) : ∃ (A : ℝ) (α : ℝ), 0 ≤ A ∧ 0 < α ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (γ : ℝ), γlo ≤ γ → γ ≤ γhi → ∀ (ρ : ℝ), ρlo ≤ ρ → ρ ≤ ρhi → ∀ (P : RumorProcess n), P.UpperGrowth γ a b c f → P.UpperShrinking ρ a' c' g → (∀ (S : Finset (Fin n)), f * ↑n ≤ ↑S.card → g * ↑n < ↑n - ↑S.card → ∀ x ∉ S, p ≤ P.informProb S x) → ∀ (S : Finset (Fin n)), S.Nonempty → ∀ (r : ℕ), P.notYet (↑n) (⌈Real.logb (1 + γ) ↑n⌉₊ + ⌈Real.log ↑n / ρ⌉₊ + r) S ≤ A * Real.exp (-α * ↑r)

Total spreading time, tail bound, with a nonnegative prefactor (proof of spreading_upper_tail).

theorem Epidemics.Revisited.spreading_upper_expect_proof {γlo γhi a b c f ρlo ρhi a' c' g p : ℝ} (hγlo : 0 < γlo) (hγ : γlo ≤ γhi) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hf0 : 0 < f) (hf1 : f < 1) (haf : a * f < 1) (hρlo : 0 < ρlo) (hρ : ρlo ≤ ρhi) (ha' : 0 ≤ a') (hc' : 0 ≤ c') (hg0 : 0 < g) (hag : Real.exp (-ρlo) + a' * g < 1) (hp0 : 0 < p) (hp1 : p ≤ 1) : ∃ (B : ℝ) (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (γ : ℝ), γlo ≤ γ → γ ≤ γhi → ∀ (ρ : ℝ), ρlo ≤ ρ → ρ ≤ ρhi → ∀ (P : RumorProcess n), P.UpperGrowth γ a b c f → P.UpperShrinking ρ a' c' g → (∀ (S : Finset (Fin n)), f * ↑n ≤ ↑S.card → g * ↑n < ↑n - ↑S.card → ∀ x ∉ S, p ≤ P.informProb S x) → ∀ (S : Finset (Fin n)), S.Nonempty → ∀ (R : ℕ), ∑ t ∈ Finset.range R, P.notYet (↑n) t S ≤ Real.logb (1 + γ) ↑n + Real.log ↑n / ρ + B

Total spreading time, expectation (proof of spreading_upper_expect).