Exponential shrinking regime, upper bound: constants and proof (Theorem 31)

Two stages, composed by tail_compose:

1. From at most g n to at most g₀ n uninformed nodes: every uninformed node is informed with probability at least p₀ = 1 - e^{-ρlo} - a g > 0, so Lemma 19 (connect_tail) gives the tail (g / g₀) e^{-p₀ r} (notYet_shrink_stage1).
2. From at most g₀ n uninformed nodes to none: the potential of ShrinkingPotential, with δ = e^{-ρhi} (1 - e^{-ρlo}) / 2, g₀ = min g (δ / (3 (a + 1))), β = a / δ and K = β (1 + c) e^{ρhi}, gives the tail (1 + β g₀) e^{K / ρlo + K} e^{-(ρlo / 2) r} after ⌈ln n / ρ⌉ + r rounds (notYet_shrink_stage2).

All constants depend only on ρlo, ρhi, a, c, g; the threshold is n ≥ 2 K / ρlo + 1.

noncomputable def Epidemics.Revisited.shrinkDelta (ρlo ρhi : ℝ) : ℝ

δ = e^{-ρhi} (1 - e^{-ρlo}) / 2, so that x (1 - x) ≥ 2 δ for x = e^{-ρ}, ρ ∈ [ρlo, ρhi].

Equations

• Epidemics.Revisited.shrinkDelta ρlo ρhi = Real.exp (-ρhi) * (1 - Real.exp (-ρlo)) / 2

noncomputable def Epidemics.Revisited.shrinkG0 (ρlo ρhi a g : ℝ) : ℝ

The fraction g₀ of uninformed nodes below which the potential contracts.

Equations

• Epidemics.Revisited.shrinkG0 ρlo ρhi a g = min g (Epidemics.Revisited.shrinkDelta ρlo ρhi / (3 * (a + 1)))

noncomputable def Epidemics.Revisited.shrinkBeta (ρlo ρhi a : ℝ) : ℝ

Weight of the quadratic term of the potential.

Equations

• Epidemics.Revisited.shrinkBeta ρlo ρhi a = a / Epidemics.Revisited.shrinkDelta ρlo ρhi

noncomputable def Epidemics.Revisited.shrinkK (ρlo ρhi a c : ℝ) : ℝ

Variance slack: one round multiplies the potential by at most e^{-ρ} (1 + K / n).

Equations

• Epidemics.Revisited.shrinkK ρlo ρhi a c = Epidemics.Revisited.shrinkBeta ρlo ρhi a * (1 + c) * Real.exp ρhi

noncomputable def Epidemics.Revisited.shrinkP0 (ρlo a g : ℝ) : ℝ

Lower bound 1 - e^{-ρlo} - a g on the probability to be informed, for at most g n uninformed nodes.

Equations

• Epidemics.Revisited.shrinkP0 ρlo a g = 1 - Real.exp (-ρlo) - a * g

noncomputable def Epidemics.Revisited.shrinkA1 (ρlo ρhi a g : ℝ) : ℝ

Prefactor of the first stage.

Equations

• Epidemics.Revisited.shrinkA1 ρlo ρhi a g = g / Epidemics.Revisited.shrinkG0 ρlo ρhi a g

noncomputable def Epidemics.Revisited.shrinkA2 (ρlo ρhi a c g : ℝ) : ℝ

Prefactor of the second stage.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Epidemics.Revisited.shrinkAlpha (ρlo a g : ℝ) : ℝ

Rate of the tail bound of Theorem 31.

Equations

• Epidemics.Revisited.shrinkAlpha ρlo a g = min (Epidemics.Revisited.shrinkP0 ρlo a g) (ρlo / 2) / 2

noncomputable def Epidemics.Revisited.shrinkA (ρlo ρhi a c g : ℝ) : ℝ

Prefactor of the tail bound of Theorem 31.

Equations

• Epidemics.Revisited.shrinkA ρlo ρhi a c g = Epidemics.Revisited.shrinkA1 ρlo ρhi a g * Real.exp (Epidemics.Revisited.shrinkAlpha ρlo a g) + Epidemics.Revisited.shrinkA2 ρlo ρhi a c g

noncomputable def Epidemics.Revisited.shrinkN (ρlo ρhi a c : ℝ) : ℕ

Threshold on n in Theorem 31.

Equations

• Epidemics.Revisited.shrinkN ρlo ρhi a c = ⌈2 * Epidemics.Revisited.shrinkK ρlo ρhi a c / ρlo⌉₊ + 1

theorem Epidemics.Revisited.exp_neg_lt_one {x : ℝ} (hx : 0 < x) : Real.exp (-x) < 1

theorem Epidemics.Revisited.shrinkDelta_pos {ρlo ρhi : ℝ} (hρlo : 0 < ρlo) : 0 < shrinkDelta ρlo ρhi

theorem Epidemics.Revisited.shrinkDelta_le_half {ρlo ρhi : ℝ} (hρlo : 0 < ρlo) (hρ : ρlo ≤ ρhi) : shrinkDelta ρlo ρhi ≤ 1 / 2

theorem Epidemics.Revisited.two_shrinkDelta_le {ρlo ρhi ρ : ℝ} (hρlo : 0 < ρlo) (hρ1 : ρlo ≤ ρ) (hρ2 : ρ ≤ ρhi) : 2 * shrinkDelta ρlo ρhi ≤ Real.exp (-ρ) * (1 - Real.exp (-ρ))

x (1 - x) ≥ 2 δ for x = e^{-ρ} with ρlo ≤ ρ ≤ ρhi.

theorem Epidemics.Revisited.shrinkG0_pos {ρlo ρhi a g : ℝ} (hρlo : 0 < ρlo) (ha : 0 ≤ a) (hg0 : 0 < g) : 0 < shrinkG0 ρlo ρhi a g

theorem Epidemics.Revisited.shrinkG0_le {ρlo ρhi a g : ℝ} : shrinkG0 ρlo ρhi a g ≤ g

theorem Epidemics.Revisited.a_mul_shrinkG0_le {ρlo ρhi a g : ℝ} (hρlo : 0 < ρlo) (ha : 0 ≤ a) : a * shrinkG0 ρlo ρhi a g ≤ shrinkDelta ρlo ρhi / 3

theorem Epidemics.Revisited.shrinkBeta_nonneg {ρlo ρhi a : ℝ} (hρlo : 0 < ρlo) (ha : 0 ≤ a) : 0 ≤ shrinkBeta ρlo ρhi a

theorem Epidemics.Revisited.shrinkK_nonneg {ρlo ρhi a c : ℝ} (hρlo : 0 < ρlo) (ha : 0 ≤ a) (hc : 0 ≤ c) : 0 ≤ shrinkK ρlo ρhi a c

theorem Epidemics.Revisited.shrink_drift {ρlo ρhi a g ρ : ℝ} (hρlo : 0 < ρlo) (hρ : ρlo ≤ ρhi) (hρ1 : ρlo ≤ ρ) (hρ2 : ρ ≤ ρhi) (ha : 0 ≤ a) (hg0 : 0 < g) : a + shrinkBeta ρlo ρhi a * (Real.exp (-ρ) + a * shrinkG0 ρlo ρhi a g) ^ 2 ≤ shrinkBeta ρlo ρhi a * Real.exp (-ρ)

The drift condition of the quadratic potential: a + β q₀² ≤ β e^{-ρ} with q₀ = e^{-ρ} + a g₀.

theorem Epidemics.Revisited.shrink_varK {ρlo ρhi a c ρ : ℝ} (hρlo : 0 < ρlo) (hρ2 : ρ ≤ ρhi) (ha : 0 ≤ a) (hc : 0 ≤ c) : shrinkBeta ρlo ρhi a * (1 + c) ≤ Real.exp (-ρ) * shrinkK ρlo ρhi a c

The variance condition of the quadratic potential: β (1 + c) ≤ e^{-ρ} K.

theorem Epidemics.Revisited.shrinkP0_pos {ρlo a g : ℝ} (hag : Real.exp (-ρlo) + a * g < 1) : 0 < shrinkP0 ρlo a g

theorem Epidemics.Revisited.shrinkP0_le_one {ρlo a g : ℝ} (ha : 0 ≤ a) (hg : 0 ≤ g) : shrinkP0 ρlo a g ≤ 1

theorem Epidemics.Revisited.shrinkAlpha_pos {ρlo a g : ℝ} (hρlo : 0 < ρlo) (hag : Real.exp (-ρlo) + a * g < 1) : 0 < shrinkAlpha ρlo a g

theorem Epidemics.Revisited.shrinkA1_nonneg {ρlo ρhi a g : ℝ} (hρlo : 0 < ρlo) (ha : 0 ≤ a) (hg0 : 0 < g) : 0 ≤ shrinkA1 ρlo ρhi a g

theorem Epidemics.Revisited.shrinkA2_nonneg {ρlo ρhi a c g : ℝ} (hρlo : 0 < ρlo) (ha : 0 ≤ a) (hg0 : 0 < g) : 0 ≤ shrinkA2 ρlo ρhi a c g

theorem Epidemics.Revisited.shrinkA_nonneg {ρlo ρhi a c g : ℝ} (hρlo : 0 < ρlo) (ha : 0 ≤ a) (hg0 : 0 < g) : 0 ≤ shrinkA ρlo ρhi a c g

theorem Epidemics.Revisited.shrinkN_facts {ρlo ρhi a c : ℝ} {n : ℕ} (hρlo : 0 < ρlo) (hn : shrinkN ρlo ρhi a c ≤ n) : 1 ≤ ↑n ∧ 2 * shrinkK ρlo ρhi a c ≤ ρlo * ↑n

theorem Epidemics.Revisited.notYet_shrink_stage1 {n : ℕ} (P : RumorProcess n) {ρlo ρ a c g g₀ : ℝ} (hρ1 : ρlo ≤ ρ) (ha : 0 ≤ a) (hg : 0 ≤ g) (hg₀ : 0 < g₀) (hag : Real.exp (-ρlo) + a * g < 1) (hUS : P.UpperShrinking ρ a c g) (hn : 0 < ↑n) (S : Finset (Fin n)) (hS : ↑n - ↑S.card ≤ g * ↑n) (r : ℕ) : P.notYet (↑n - g₀ * ↑n) r S ≤ g / g₀ * Real.exp (-shrinkP0 ρlo a g * ↑r)

Stage one of Theorem 31 (Lemma 19): from at most g n uninformed nodes, at most g₀ n are left after r rounds except with probability (g / g₀) e^{-p₀ r}.

theorem Epidemics.Revisited.notYet_shrink_le {n : ℕ} {ρlo ρhi a c g : ℝ} (hρlo : 0 < ρlo) (hρ : ρlo ≤ ρhi) (ha : 0 ≤ a) (hc : 0 ≤ c) (hg0 : 0 < g) (hag : Real.exp (-ρlo) + a * g < 1) (hn : shrinkN ρlo ρhi a c ≤ n) {ρ : ℝ} (hρ1 : ρlo ≤ ρ) (hρ2 : ρ ≤ ρhi) (P : RumorProcess n) (hUS : P.UpperShrinking ρ a c g) (S : Finset (Fin n)) (hS : ↑n - ↑S.card ≤ g * ↑n) (r : ℕ) : P.notYet (↑n) (⌈Real.log ↑n / ρ⌉₊ + r) S ≤ shrinkA ρlo ρhi a c g * Real.exp (-shrinkAlpha ρlo a g * ↑r)

Theorem 31, tail bound with explicit constants.

theorem Epidemics.Revisited.shrinking_upper_tail_proof {ρlo ρhi a c g : ℝ} (hρlo : 0 < ρlo) (hρ : ρlo ≤ ρhi) (ha : 0 ≤ a) (hc : 0 ≤ c) (hg0 : 0 < g) (hag : Real.exp (-ρlo) + a * g < 1) : ∃ (A : ℝ) (α : ℝ), 0 < α ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (ρ : ℝ), ρlo ≤ ρ → ρ ≤ ρhi → ∀ (P : RumorProcess n), P.UpperShrinking ρ a c g → ∀ (S : Finset (Fin n)), ↑n - ↑S.card ≤ g * ↑n → ∀ (r : ℕ), P.notYet (↑n) (⌈Real.log ↑n / ρ⌉₊ + r) S ≤ A * Real.exp (-α * ↑r)

Theorem 31, tail bound (proof of shrinking_upper_tail).

theorem Epidemics.Revisited.shrinking_upper_expect_proof {ρlo ρhi a c g : ℝ} (hρlo : 0 < ρlo) (hρ : ρlo ≤ ρhi) (ha : 0 ≤ a) (hc : 0 ≤ c) (hg0 : 0 < g) (hag : Real.exp (-ρlo) + a * g < 1) : ∃ (B : ℝ) (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (ρ : ℝ), ρlo ≤ ρ → ρ ≤ ρhi → ∀ (P : RumorProcess n), P.UpperShrinking ρ a c g → ∀ (S : Finset (Fin n)), ↑n - ↑S.card ≤ g * ↑n → ∀ (R : ℕ), ∑ t ∈ Finset.range R, P.notYet (↑n) t S ≤ Real.log ↑n / ρ + B

Theorem 31, expectation (proof of shrinking_upper_expect).