A quadratic potential for the exponential shrinking regime (Theorem 31)

With u = n - |S| uninformed nodes, the potential is Φ_β(S) = u + (β / n) u². Under the upper exponential shrinking conditions, once u ≤ g₀ n for a small g₀, one round multiplies its expectation by at most e^{-ρ} (1 + K / n) (apply_shrinkPot_le):

• E[u'] ≤ u (e^{-ρ} + a u / n) by condition (i);
• E[u'²] = Var[u'] + E[u']² ≤ (1 + c) u + E[u']² by Lemma 9 with the covariance bound c / u;
• the excess a u² / n of the first line is paid by the drop of the quadratic term, provided a + β q₀² ≤ β e^{-ρ} with q₀ = e^{-ρ} + a g₀, and the variance term β (1 + c) u / n by the factor 1 + K / n, provided β (1 + c) ≤ e^{-ρ} K.

Since Φ_β ≥ 1 while some node is uninformed, Markov's inequality after T = ⌈ln n / ρ⌉ + r rounds gives P[T(·, n) > T] ≤ e^{-ρ T} (1 + K / n)^T Φ_β(S), and (1 + K / n)^T stays bounded because ln n ≤ n (notYet_shrink_stage2). This replaces the paper's phase calculus (Lemmas 32-37) for this regime.

theorem Epidemics.Revisited.card_cast_le {n : ℕ} (T : Finset (Fin n)) : ↑T.card ≤ ↑n

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

The potential u + (β / n) u² in the number u = n - |T| of uninformed nodes.

Equations

• Epidemics.Revisited.shrinkPot β T = ↑n - ↑T.card + β / ↑n * (↑n - ↑T.card) ^ 2

theorem Epidemics.Revisited.shrinkPot_nonneg {n : ℕ} {β : ℝ} (hβ : 0 ≤ β) (T : Finset (Fin n)) : 0 ≤ shrinkPot β T

theorem Epidemics.Revisited.below_le_shrinkPot {n : ℕ} {β : ℝ} (hβ : 0 ≤ β) (T : Finset (Fin n)) : below (↑n) T ≤ shrinkPot β T

While some node is uninformed, the potential is at least one.

theorem Epidemics.Revisited.expect_deficit_le {n : ℕ} (P : RumorProcess n) {ρ a c g : ℝ} (hUS : P.UpperShrinking ρ a c g) (S : Finset (Fin n)) (hS : ↑n - ↑S.card ≤ g * ↑n) : ((P.K S).expect fun (T : Finset (Fin n)) => ↑n - ↑T.card) ≤ (↑n - ↑S.card) * (Real.exp (-ρ) + a * ((↑n - ↑S.card) / ↑n))

Expected number of uninformed nodes after one round under condition (i).

theorem Epidemics.Revisited.expect_deficit_sq_le {n : ℕ} (P : RumorProcess n) {ρ a c g : ℝ} (hc : 0 ≤ c) (hUS : P.UpperShrinking ρ a c g) (S : Finset (Fin n)) (hS : ↑n - ↑S.card ≤ g * ↑n) : ((P.K S).expect fun (T : Finset (Fin n)) => (↑n - ↑T.card) ^ 2) ≤ (1 + c) * (↑n - ↑S.card) + ((P.K S).expect fun (T : Finset (Fin n)) => ↑n - ↑T.card) ^ 2

Second moment of the number of uninformed nodes after one round: E[u'²] ≤ (1 + c) u + E[u']² (Lemma 9 with the covariance bound c / u).

theorem Epidemics.Revisited.apply_shrinkPot_le {n : ℕ} (P : RumorProcess n) {ρ a c g g₀ β K : ℝ} (ha : 0 ≤ a) (hc : 0 ≤ c) (hg₀ : g₀ ≤ g) (hβ : 0 ≤ β) (hK : 0 ≤ K) (hβq : a + β * (Real.exp (-ρ) + a * g₀) ^ 2 ≤ β * Real.exp (-ρ)) (hβK : β * (1 + c) ≤ Real.exp (-ρ) * K) (hUS : P.UpperShrinking ρ a c g) (hn : 0 < ↑n) (S : Finset (Fin n)) (hS : ↑n - ↑S.card ≤ g₀ * ↑n) : P.K.apply (shrinkPot β) S ≤ Real.exp (-ρ) * (1 + K / ↑n) * shrinkPot β S

One round contracts the potential Φ_β by e^{-ρ} (1 + K / n) once at most g₀ n nodes are uninformed.

theorem Epidemics.Revisited.iterate_shrinkPot_le {n : ℕ} (P : RumorProcess n) {ρ a c g g₀ β K : ℝ} (ha : 0 ≤ a) (hc : 0 ≤ c) (hg₀ : g₀ ≤ g) (hβ : 0 ≤ β) (hK : 0 ≤ K) (hβq : a + β * (Real.exp (-ρ) + a * g₀) ^ 2 ≤ β * Real.exp (-ρ)) (hβK : β * (1 + c) ≤ Real.exp (-ρ) * K) (hUS : P.UpperShrinking ρ a c g) (hn : 0 < ↑n) (t : ℕ) (S : Finset (Fin n)) (hS : ↑n - ↑S.card ≤ g₀ * ↑n) : P.K.iterate t (shrinkPot β) S ≤ (Real.exp (-ρ) * (1 + K / ↑n)) ^ t * shrinkPot β S

Iterating the contraction: E[Φ_β(S_t)] ≤ (e^{-ρ} (1 + K / n))^t Φ_β(S).

theorem Epidemics.Revisited.shrink_exponent_le {n : ℕ} {ρlo ρ K : ℝ} (hρlo : 0 < ρlo) (hρ : ρlo ≤ ρ) (hK : 0 ≤ K) (hn1 : 1 ≤ ↑n) (hnK : 2 * K ≤ ρlo * ↑n) (r : ℕ) : -ρ * ↑(⌈Real.log ↑n / ρ⌉₊ + r) + ↑(⌈Real.log ↑n / ρ⌉₊ + r) * (K / ↑n) + Real.log ↑n ≤ K / ρlo + K - ρlo / 2 * ↑r

The exponent after T = ⌈ln n / ρ⌉ + r rounds: -ρ T + T K / n + ln n is at most K / ρlo + K - (ρlo / 2) r, when n ≥ 1 and 2 K ≤ ρlo n.

theorem Epidemics.Revisited.notYet_shrink_stage2 {n : ℕ} (P : RumorProcess n) {ρlo ρ a c g g₀ β K : ℝ} (hρlo : 0 < ρlo) (hρ : ρlo ≤ ρ) (ha : 0 ≤ a) (hc : 0 ≤ c) (hg₀0 : 0 ≤ g₀) (hg₀ : g₀ ≤ g) (hβ : 0 ≤ β) (hK : 0 ≤ K) (hβq : a + β * (Real.exp (-ρ) + a * g₀) ^ 2 ≤ β * Real.exp (-ρ)) (hβK : β * (1 + c) ≤ Real.exp (-ρ) * K) (hUS : P.UpperShrinking ρ a c g) (hn1 : 1 ≤ ↑n) (hnK : 2 * K ≤ ρlo * ↑n) (S : Finset (Fin n)) (hS : ↑n - ↑S.card ≤ g₀ * ↑n) (r : ℕ) : P.notYet (↑n) (⌈Real.log ↑n / ρ⌉₊ + r) S ≤ (1 + β * g₀) * Real.exp (K / ρlo + K) * Real.exp (-(ρlo / 2) * ↑r)

Stage two of Theorem 31: from at most g₀ n uninformed nodes, some node is still uninformed after ⌈ln n / ρ⌉ + r rounds with probability at most (1 + β g₀) e^{K / ρlo + K} e^{-(ρlo / 2) r}.