Composing tail bounds (EPI-8, shrinking regime and total time)

Generic finite-time tools for the tails notYet, used for Theorem 31 and for the total spreading time:

• notYet_add_le: the Markov property at a fixed time. If from every state with at least m' informed nodes the tail after t more rounds is at most B, then the tail after s + t rounds is at most the tail of reaching m' after s rounds, plus B.
• tail_compose: two exponential tails in sequence give an exponential tail, by splitting the extra rounds r into r / 2 and r - r / 2.
• sum_notYet_le_of_tail: an exponential tail after T₀ rounds bounds every partial sum of the tail series ∑_t P[T > t] by T₀ + A / (1 - e^{-α}).

theorem Epidemics.Revisited.notYet_nonneg {n : ℕ} (P : RumorProcess n) (m : ℝ) (t : ℕ) (S : Finset (Fin n)) : 0 ≤ P.notYet m t S

theorem Epidemics.Revisited.notYet_le_one {n : ℕ} (P : RumorProcess n) (m : ℝ) (t : ℕ) (S : Finset (Fin n)) : P.notYet m t S ≤ 1

theorem Epidemics.Revisited.notYet_succ {n : ℕ} (P : RumorProcess n) (m : ℝ) (t : ℕ) (S : Finset (Fin n)) : P.notYet m (t + 1) S = (P.K S).expect fun (T : Finset (Fin n)) => P.notYet m t T

One more round: P_S[T > t + 1] = E_{S' ∼ K S}[P_{S'}[T > t]].

theorem Epidemics.Revisited.notYet_zero {n : ℕ} (P : RumorProcess n) (m : ℝ) (S : Finset (Fin n)) : P.notYet m 0 S = below m S

theorem Epidemics.Revisited.notYet_add_le {n : ℕ} (P : RumorProcess n) {m m' B : ℝ} (hB : 0 ≤ B) (s t : ℕ) (hT : ∀ (T : Finset (Fin n)), m' ≤ ↑T.card → P.notYet m t T ≤ B) (S : Finset (Fin n)) : P.notYet m (s + t) S ≤ P.notYet m' s S + B

Markov property at a fixed time: the tail after s + t rounds is at most the tail of reaching m' within s rounds plus a bound B on the tail after t rounds from any state with at least m' informed nodes.

theorem Epidemics.Revisited.one_sub_pow_le_exp {p : ℝ} (hp1 : p ≤ 1) (r : ℕ) : (1 - p) ^ r ≤ Real.exp (-p * ↑r)

(1 - p)^r ≤ e^{-p r}.

theorem Epidemics.Revisited.exp_split_le {A₁ α₁ A₂ α₂ : ℝ} (hA₁ : 0 ≤ A₁) (hA₂ : 0 ≤ A₂) (hα₁ : 0 < α₁) (hα₂ : 0 < α₂) (r : ℕ) : A₁ * Real.exp (-α₁ * ↑(r / 2)) + A₂ * Real.exp (-α₂ * ↑(r - r / 2)) ≤ (A₁ * Real.exp (min α₁ α₂ / 2) + A₂) * Real.exp (-(min α₁ α₂ / 2) * ↑r)

Splitting r extra rounds into r / 2 and r - r / 2: two exponential rates α₁, α₂ give the rate min α₁ α₂ / 2.

theorem Epidemics.Revisited.tail_compose {n : ℕ} (P : RumorProcess n) {m m' A₁ α₁ A₂ α₂ : ℝ} (hA₁ : 0 ≤ A₁) (hA₂ : 0 ≤ A₂) (hα₁ : 0 < α₁) (hα₂ : 0 < α₂) {T₁ T₂ : ℕ} (S : Finset (Fin n)) (h₁ : ∀ (r : ℕ), P.notYet m' (T₁ + r) S ≤ A₁ * Real.exp (-α₁ * ↑r)) (h₂ : ∀ (T : Finset (Fin n)), m' ≤ ↑T.card → ∀ (r : ℕ), P.notYet m (T₂ + r) T ≤ A₂ * Real.exp (-α₂ * ↑r)) (r : ℕ) : P.notYet m (T₁ + T₂ + r) S ≤ (A₁ * Real.exp (min α₁ α₂ / 2) + A₂) * Real.exp (-(min α₁ α₂ / 2) * ↑r)

Two exponential tails in sequence: if from S the process reaches m' informed nodes within T₁ + r rounds except with probability A₁ e^{-α₁ r}, and from every state with at least m' informed nodes it reaches m within T₂ + r rounds except with probability A₂ e^{-α₂ r}, then from S it reaches m within T₁ + T₂ + r rounds except with probability (A₁ e^{α} + A₂) e^{-α r}, where α = min α₁ α₂ / 2.

theorem Epidemics.Revisited.sum_notYet_le_of_tail {n : ℕ} (P : RumorProcess n) {m A α : ℝ} (hA : 0 ≤ A) (hα : 0 < α) (T₀ : ℕ) (S : Finset (Fin n)) (h : ∀ (r : ℕ), P.notYet m (T₀ + r) S ≤ A * Real.exp (-α * ↑r)) (R : ℕ) : ∑ t ∈ Finset.range R, P.notYet m t S ≤ ↑T₀ + A / (1 - Real.exp (-α))

An exponential tail after T₀ rounds bounds every partial sum of the tail series: ∑_{t < R} P[T > t] ≤ T₀ + A / (1 - e^{-α}).