Kurtz's law of large numbers for SIR, in discrete time (CRN-2) #

For the uniformized SIR chain of Epidemics.KurtzDefs (N agents, infection weight β, recovery weight γ, one step per unit 1 / ((β + γ) N) of time), the scaled counts (S, I, R) / N stay, with probability exponentially close to one in N, uniformly close on a finite horizon [0, T] to the solution of the Kermack–McKendrick system of EPI-7 (sirField β γ), in the form of the differential-equation method of N. Wormald (The differential equation method for random graph processes and greedy algorithms, 1999, Theorem 5.1) and of T. G. Kurtz's law of large numbers for density-dependent Markov chains (Solutions of ordinary differential equations as limits of pure jump Markov processes, J. Appl. Probab. 7, 1970).

law_of_large_numbers: constants C, c, L depending only on β, γ, T such that, for every N, every initial configuration x₀, every solution (s, i, r) on [0, ∞) started in the simplex and every ε > 0, the chain stays within L · dist (scaled x₀) (s 0, i 0, r 0) + ε of (s, i, r) at all steps k ≤ T (β + γ) N, compared at times k / ((β + γ) N), except with probability at most C exp(-c ε² N). When scaled x₀ = (s 0, i 0, r 0) (Wormald's choice of the initial value), the distance is just ε.
tendsto_deviationProb: convergence in probability, uniformly on the horizon, to a fixed solution, when the scaled initial configurations converge to its initial point.

The intended proof: the drift identity and bounded increments (Epidemics.KurtzDrift) make the deviation of the scaled counts from their compensator a martingale with increments O(1 / N), controlled by the maximal Azuma–Hoeffding inequality expList_azuma; on the good event, the discrete Grönwall inequality (Mathlib's discrete_gronwall) bounds the distance to the solution, the Euler discretization error being O(1 / N).

source

theorem Epidemics.Kurtz.law_of_large_numbers {β γ : ℕ} (hβ : 0 < β) (hγ : 0 < γ) {T : ℝ} (hT : 0 < T) :

∃ (C : ℝ) (c : ℝ) (L : ℝ), 0 < C ∧ 0 < c ∧ ∀ (N : ℕ), 0 < N → ∀ (x₀ : Config N) (s i r : ℝ → ℝ), IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField ↑β ↑γ) (Set.Ici 0) → 0 ≤ s 0 → 0 ≤ i 0 → 0 ≤ r 0 → s 0 + i 0 + r 0 = 1 → ∀ (ε : ℝ), 0 < ε → deviationProb β γ x₀ (fun (t : ℝ) => (s t, i t, r t)) (L * dist (scaled x₀) (s 0, i 0, r 0) + ε) ⌊T * (↑β + ↑γ) * ↑N⌋₊ ≤ C * Real.exp (-(c * ε ^ 2 * ↑N))

Kurtz's law of large numbers for SIR, in discrete time, with an exponential bound (Wormald 1999, Theorem 5.1; Kurtz 1970). Let β, γ > 0 and T > 0. There are constants C, c > 0 and L such that for every number of agents N > 0, every initial configuration x₀, every solution (s, i, r) of the Kermack–McKendrick system s' = -β s i, i' = β s i - γ i, r' = γ i on [0, ∞) whose initial point lies in the simplex, and every ε > 0: with probability at least 1 - C exp(-c ε² N), at every step k ≤ T (β + γ) N the scaled counts of the chain are within L · dist (scaled x₀) (s 0, i 0, r 0) + ε (sup distance) of (s, i, r) at time k / ((β + γ) N).

source

theorem Epidemics.Kurtz.tendsto_deviationProb {β γ : ℕ} (hβ : 0 < β) (hγ : 0 < γ) {T : ℝ} (hT : 0 < T) {s i r : ℝ → ℝ} (hsol : 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) (x₀ : (N : ℕ) → Config N) (hx₀ : Filter.Tendsto (fun (N : ℕ) => scaled (x₀ N)) Filter.atTop (nhds (s 0, i 0, r 0))) {ε : ℝ} (hε : 0 < ε) :

Filter.Tendsto (fun (N : ℕ) => deviationProb β γ (x₀ N) (fun (t : ℝ) => (s t, i t, r t)) ε ⌊T * (↑β + ↑γ) * ↑N⌋₊) Filter.atTop (nhds 0)

Kurtz's law of large numbers for SIR, in probability, uniformly on [0, T] (Kurtz 1970; roadmap row CRN-2). Let (s, i, r) be a solution on [0, ∞) of the Kermack–McKendrick system with rates β, γ > 0, started in the simplex, and let x₀ N be configurations of N agents whose scaled counts converge to (s 0, i 0, r 0). Then for every ε > 0, the probability that the chain started at x₀ N is farther than ε from (s, i, r) at some step k ≤ T (β + γ) N (compared at time k / ((β + γ) N)) tends to 0 as N → ∞.