Kurtz's law of large numbers for SIR: the probability bound (CRN-2, helpers)

If the tube width θ exceeds the deterministic bound of close_of_good for a martingale level δ, a deviation larger than θ forces one of the three coordinate martingales ±mgIncr β γ j to reach δ (fail_indicator_le), and the maximal Azuma–Hoeffding inequality bounds each of the six events: deviationProb ≤ 6 exp(-δ² / (2 n (2/N)²)) (deviationProb_le_azuma).

theorem Epidemics.Kurtz.deviationProb_nonneg {β γ N : ℕ} (x₀ : Config N) (x : ℝ → ℝ × ℝ × ℝ) (θ : ℝ) (n : ℕ) : 0 ≤ deviationProb β γ x₀ x θ n

Probabilities are nonnegative.

theorem Epidemics.Kurtz.deviationProb_anti {β γ N : ℕ} (x₀ : Config N) (x : ℝ → ℝ × ℝ × ℝ) {θ₁ θ₂ : ℝ} (h : θ₁ ≤ θ₂) (n : ℕ) : deviationProb β γ x₀ x θ₂ n ≤ deviationProb β γ x₀ x θ₁ n

A wider tube is left with smaller probability.

noncomputable def Epidemics.Kurtz.mgEvent (β γ : ℕ) {N : ℕ} (x₀ : Config N) (δ : ℝ) (n : ℕ) (j : Fin 3) (neg : Bool) (l : List (Round N β γ)) : ℝ

The indicator that the coordinate-j martingale (or its negative, neg = true) reaches δ within n rounds.

Equations

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

theorem Epidemics.Kurtz.mgEvent_nonneg {β γ N : ℕ} (x₀ : Config N) (δ : ℝ) (n : ℕ) (j : Fin 3) (neg : Bool) (l : List (Round N β γ)) : 0 ≤ mgEvent β γ x₀ δ n j neg l

theorem Epidemics.Kurtz.fail_indicator_le {β γ N : ℕ} (hβ : 0 < β) (hγ : 0 < γ) (hN : 0 < N) {x₀ : Config N} {s i r : ℝ → ℝ} (hx : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField ↑β ↑γ) (Set.Ici 0)) (hs : 0 ≤ s 0) (hi : 0 ≤ i 0) (hr : 0 ≤ r 0) (hsum : s 0 + i 0 + r 0 = 1) {T δ θ : ℝ} (hδ : 0 ≤ δ) {n : ℕ} (hnT : ↑n ≤ T * (↑β + ↑γ) * ↑N) (hθ : (dist (scaled x₀) (s 0, i 0, r 0) + δ + T * (2 * ↑β + ↑γ) / ↑N) * Real.exp ((2 * ↑β + ↑γ) * T) ≤ θ) (l : List (Round N β γ)) (hl : l.length = n) : (if ∃ k ≤ n, θ < dist (scaled (List.foldl (step β γ) x₀ (List.take k l))) ((fun (t : ℝ) => (s t, i t, r t)) (↑k / ((↑β + ↑γ) * ↑N))) then 1 else 0) ≤ ∑ j : Fin 3, (mgEvent β γ x₀ δ n j false l + mgEvent β γ x₀ δ n j true l)

Failure forces a martingale deviation. Along rounds l of length n ≤ T (β + γ) N, if the tube width θ is at least the bound of close_of_good at level δ, a deviation larger than θ makes one of the six martingale events happen.

theorem Epidemics.Kurtz.deviationProb_le_azuma {β γ N : ℕ} (hβ : 0 < β) (hγ : 0 < γ) (hN : 0 < N) {x₀ : Config N} {s i r : ℝ → ℝ} (hx : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField ↑β ↑γ) (Set.Ici 0)) (hs : 0 ≤ s 0) (hi : 0 ≤ i 0) (hr : 0 ≤ r 0) (hsum : s 0 + i 0 + r 0 = 1) {T δ θ : ℝ} (hδ : 0 ≤ δ) {n : ℕ} (hnT : ↑n ≤ T * (↑β + ↑γ) * ↑N) (hθ : (dist (scaled x₀) (s 0, i 0, r 0) + δ + T * (2 * ↑β + ↑γ) / ↑N) * Real.exp ((2 * ↑β + ↑γ) * T) ≤ θ) : deviationProb β γ x₀ (fun (t : ℝ) => (s t, i t, r t)) θ n ≤ 6 * Real.exp (-(δ ^ 2 / (2 * ↑n * (2 / ↑N) ^ 2)))

The six Azuma bounds. Under the hypotheses of fail_indicator_le with 0 < δ and 0 < n, the probability of a deviation larger than θ within n steps is at most 6 exp(-δ² / (2 n (2/N)²)).