Lemma 20: one round and the path bound

• overshoot_round_proof: by Lemma 9 and Chebyshev's inequality, a round started with k < f n informed nodes ends with at least f' n informed nodes with probability at most (p + c) / ((f' - f - p (1 - f))² n). The expected number of newly informed nodes is at most p (n - k), and k + p (n - k) ≤ n (f + p (1 - f)) because p ≤ 1.
• jumpProb_le_sum: if every round started below lo from a nonempty set reaches hi with probability at most ε, the path jumps over [lo, hi[ within t rounds with probability at most ε times the expected number of those rounds that start below lo. The proof is an induction on t along Kernel.trajectory: the jump happens in the first round or in the path that follows it.

theorem Epidemics.Revisited.traj_mono {α : Type u_1} [Fintype α] (K : Dynamics.Kernel α) (t : ℕ) (a : α) {F G : List α → α → ℝ} (h : ∀ (l : List α) (b : α), F l b ≤ G l b) : K.trajectory t a F ≤ K.trajectory t a G

theorem Epidemics.Revisited.traj_add {α : Type u_1} [Fintype α] (K : Dynamics.Kernel α) (t : ℕ) (a : α) (F G : List α → α → ℝ) : (K.trajectory t a fun (l : List α) (b : α) => F l b + G l b) = K.trajectory t a F + K.trajectory t a G

theorem Epidemics.Revisited.traj_const {α : Type u_1} [Fintype α] (K : Dynamics.Kernel α) (t : ℕ) (a : α) (c : ℝ) : (K.trajectory t a fun (x : List α) (x_1 : α) => c) = c

theorem Epidemics.Revisited.traj_head {α : Type u_1} [Fintype α] (K : Dynamics.Kernel α) (t : ℕ) (a : α) (G : α → ℝ) : (K.trajectory t a fun (l : List α) (b : α) => G ((l ++ [b]).headD b)) = G a

A functional of the first state of the path a, S₁, … is evaluated at a.

theorem Epidemics.Revisited.jumpsOver_cons {n : ℕ} {lo hi : ℝ} {S : Finset (Fin n)} {l : List (Finset (Fin n))} {c : Finset (Fin n)} (h : JumpsOver lo hi (S :: (l ++ [c]))) : ↑S.card < lo ∧ hi ≤ ↑((l ++ [c]).headD c).card ∨ JumpsOver lo hi (l ++ [c])

A jump along S :: path happens in the first round or along path.

theorem Epidemics.Revisited.jumpInd_cons_le {n : ℕ} (lo hi : ℝ) (S : Finset (Fin n)) (l : List (Finset (Fin n))) (c : Finset (Fin n)) : (if JumpsOver lo hi (S :: (l ++ [c])) then 1 else 0) ≤ (if ↑S.card < lo ∧ hi ≤ ↑((l ++ [c]).headD c).card then 1 else 0) + if JumpsOver lo hi (l ++ [c]) then 1 else 0

theorem Epidemics.Revisited.jumpProb_succ_le {n : ℕ} (P : RumorProcess n) (lo hi : ℝ) (t : ℕ) (S : Finset (Fin n)) : P.jumpProb lo hi (t + 1) S ≤ (P.K S).expect fun (S₁ : Finset (Fin n)) => (if ↑S.card < lo ∧ hi ≤ ↑S₁.card then 1 else 0) + P.jumpProb lo hi t S₁

One step of the path: P[jump within t + 1 rounds] ≤ E_{S₁}[1[|S| < lo ≤ hi ≤ |S₁|] + P_{S₁}[jump within t rounds]].

theorem Epidemics.Revisited.jumpProb_zero {n : ℕ} (P : RumorProcess n) (lo hi : ℝ) (S : Finset (Fin n)) : P.jumpProb lo hi 0 S = 0

theorem Epidemics.Revisited.jumpProb_le_sum {n : ℕ} (P : RumorProcess n) {lo hi ε : ℝ} (hround : ∀ (S : Finset (Fin n)), S.Nonempty → ↑S.card < lo → ((P.K S).prob fun (S' : Finset (Fin n)) => hi ≤ ↑S'.card) ≤ ε) (t : ℕ) (S : Finset (Fin n)) (hS : S.Nonempty) : P.jumpProb lo hi t S ≤ ε * ∑ i ∈ Finset.range t, P.notYet lo i S

Lemma 20, path form with a per-round bound ε: the probability of jumping over [lo, hi[ within t rounds is at most ε times the expected number of those rounds started below lo.

theorem Epidemics.Revisited.overshoot_round_proof {f p c f' : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hc : 0 ≤ c) (hff' : f + p * (1 - f) < f') : ∃ (C : ℝ), ∀ (n : ℕ) (P : RumorProcess n) (S : Finset (Fin n)), ↑S.card < f * ↑n → (∀ x ∉ S, P.informProb S x ≤ p) → (∀ x ∉ S, ∀ y ∉ S, x ≠ y → P.cov S x y ≤ c / ↑n) → ((P.K S).prob fun (S' : Finset (Fin n)) => f' * ↑n ≤ ↑S'.card) ≤ C / ↑n

Lemma 20, one round (proof of overshoot_round).

theorem Epidemics.Revisited.jumpProb_le_proof {f p c : ℝ} (hf1 : f < 1) (hp0 : 0 < p) (hp1 : p < 1) (hc : 0 < c) : ∃ (f' : ℝ), f < f' ∧ f' < 1 ∧ ∃ (C : ℝ), ∀ (n : ℕ) (P : RumorProcess n), (∀ (S : Finset (Fin n)), S.Nonempty → ↑S.card < f * ↑n → (∀ x ∉ S, P.informProb S x ≤ p) ∧ ∀ x ∉ S, ∀ y ∉ S, x ≠ y → P.cov S x y ≤ c / ↑n) → ∀ (S : Finset (Fin n)), S.Nonempty → ∀ (t : ℕ), P.jumpProb (f * ↑n) (f' * ↑n) t S ≤ C / ↑n * ∑ i ∈ Finset.range t, P.notYet (f * ↑n) i S

Lemma 20, path form (proof of jumpProb_le).