Crossing a flat middle range (Lemma 19)

If every uninformed node is informed with probability at least p while the number of informed nodes lies in [ℓ, m), the tail P[T(ℓ, m) > r] is at most the Markov bound on the expected number of uninformed nodes. The potential is gap m, equal to n - |S| below m and to 0 at and above m. Monotonicity keeps the chain inside {|S| ≥ ℓ}, so there is no dummy process.

theorem Epidemics.Revisited.event_of_indicator {α : Type u_1} [Fintype α] (K : Dynamics.Kernel α) (s : α → Prop) (ind : α → ℝ) (h0 : ∀ (a : α), ¬s a → ind a = 0) (h1 : ∀ (a : α), s a → ind a = 1) (t : ℕ) (a : α) : K.event s t a = K.iterate t ind a

Kernel.event agrees with iteration of any indicator of the event.

noncomputable def Epidemics.Revisited.gap {n : ℕ} (m : ℝ) (T : Finset (Fin n)) : ℝ

Uninformed mass while fewer than m nodes are informed, and 0 afterwards.

Equations

• Epidemics.Revisited.gap m T = if ↑T.card < m then ↑n - ↑T.card else 0

theorem Epidemics.Revisited.gap_of_lt {n : ℕ} {m : ℝ} {T : Finset (Fin n)} (h : ↑T.card < m) : gap m T = ↑n - ↑T.card

theorem Epidemics.Revisited.gap_of_not_lt {n : ℕ} {m : ℝ} {T : Finset (Fin n)} (h : ¬↑T.card < m) : gap m T = 0

theorem Epidemics.Revisited.gap_nonneg {n : ℕ} (m : ℝ) (T : Finset (Fin n)) : 0 ≤ gap m T

theorem Epidemics.Revisited.gap_le_deficit {n : ℕ} (m : ℝ) (T : Finset (Fin n)) : gap m T ≤ ↑n - ↑T.card

theorem Epidemics.Revisited.gap_le_slack {n : ℕ} {m : ℝ} {ℓ : ℕ} {T : Finset (Fin n)} (hℓ : ℓ ≤ T.card) : gap m T ≤ ↑n - ↑ℓ

theorem Epidemics.Revisited.notYet_indicator_le {n : ℕ} {m : ℝ} (hmn : m < ↑n) (T : Finset (Fin n)) : (if ↑T.card < m then 1 else 0) ≤ gap m T / (↑n - m)

theorem Epidemics.Revisited.expect_card_eq {n : ℕ} (P : RumorProcess n) (S : Finset (Fin n)) : ((P.K S).expect fun (T : Finset (Fin n)) => ↑T.card) = ↑S.card + ∑ x ∈ Finset.univ \ S, P.informProb S x

theorem Epidemics.Revisited.expect_deficit {n : ℕ} (P : RumorProcess n) (S : Finset (Fin n)) : ((P.K S).expect fun (T : Finset (Fin n)) => ↑n - ↑T.card) = ∑ x ∈ Finset.univ \ S, (1 - P.informProb S x)

theorem Epidemics.Revisited.apply_gap_le {n : ℕ} (P : RumorProcess n) {ℓ : ℕ} {m p : ℝ} (hp1 : p ≤ 1) (hp : ∀ (S : Finset (Fin n)), ℓ ≤ S.card → ↑S.card < m → ∀ x ∉ S, p ≤ P.informProb S x) (S : Finset (Fin n)) (hS : ℓ ≤ S.card) : P.K.apply (gap m) S ≤ (1 - p) * gap m S

theorem Epidemics.Revisited.iterate_gap_le {n : ℕ} (P : RumorProcess n) {ℓ : ℕ} {m p : ℝ} (hp1 : p ≤ 1) (hp : ∀ (S : Finset (Fin n)), ℓ ≤ S.card → ↑S.card < m → ∀ x ∉ S, p ≤ P.informProb S x) (r : ℕ) (S : Finset (Fin n)) (hS : ℓ ≤ S.card) : P.K.iterate r (gap m) S ≤ (1 - p) ^ r * gap m S

theorem Epidemics.Revisited.iterate_notYet_le {n : ℕ} (P : RumorProcess n) {ℓ : ℕ} {m p : ℝ} (hmn : m < ↑n) (hp1 : p ≤ 1) (hp : ∀ (S : Finset (Fin n)), ℓ ≤ S.card → ↑S.card < m → ∀ x ∉ S, p ≤ P.informProb S x) (S : Finset (Fin n)) (hS : ℓ ≤ S.card) (r : ℕ) : P.K.iterate r (fun (T : Finset (Fin n)) => if ↑T.card < m then 1 else 0) S ≤ (↑n - ↑ℓ) / (↑n - m) * (1 - p) ^ r

theorem Epidemics.Revisited.notYet_eq_zero_of_ge {n : ℕ} (P : RumorProcess n) {m : ℝ} {S : Finset (Fin n)} (hS : m ≤ ↑S.card) (t : ℕ) : P.notYet m t S = 0

States that already have at least m informed nodes stay there, so the tail is zero.

theorem Epidemics.Revisited.connect_tail_proof {n : ℕ} (P : RumorProcess n) {ℓ : ℕ} {m p : ℝ} (hℓm : ↑ℓ < m) (hmn : m < ↑n) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hp : ∀ (S : Finset (Fin n)), ℓ ≤ S.card → ↑S.card < m → ∀ x ∉ S, p ≤ P.informProb S x) (S : Finset (Fin n)) (hS : ℓ ≤ S.card) (r : ℕ) : P.notYet m r S ≤ (↑n - ↑ℓ) / (↑n - m) * (1 - p) ^ r

theorem Epidemics.Revisited.connect_expect_proof {n : ℕ} (P : RumorProcess n) {ℓ : ℕ} {m p : ℝ} (hℓm : ↑ℓ < m) (hmn : m < ↑n) (hp0 : 0 < p) (hp1 : p ≤ 1) (hp : ∀ (S : Finset (Fin n)), ℓ ≤ S.card → ↑S.card < m → ∀ x ∉ S, p ≤ P.informProb S x) (S : Finset (Fin n)) (hS : ℓ ≤ S.card) (R : ℕ) : ∑ t ∈ Finset.range R, P.notYet m t S ≤ (↑n - ↑ℓ) / (↑n - m) * (1 / p)