Kurtz's law of large numbers for SIR: the martingale and the good event (CRN-2, helpers)

• incrementSum telescopes (incrementSum_telescope, incrementSum_take);
• the coordinates coord j of ℝ × ℝ × ℝ and the martingale increments mgIncr β γ j y ρ = Δ coord_j (scaled) - coord_j (F (scaled y)) / ((β + γ) N), centred by the drift identity and bounded by 2 / N;
• incrementSum_mgIncr: along the rounds, the partial sums of mgIncr β γ j are the coordinates of X_k - X_0 - h ∑_{i<k} F (X_i), X_i the scaled state after i rounds and h = 1 / ((β + γ) N);
• close_of_good: on the event where the three martingales stay below δ, discrete stability (norm_sub_le_of_euler) keeps the chain within (dist (scaled x₀) x(0) + δ + T (2β + γ) / N) · exp((2β + γ) T) of the solution.

Telescoping incrementSum

theorem Epidemics.Kurtz.incrementSum_telescope {σ : Type u_1} {R : Type u_2} (step : σ → R → σ) (φ ψ : σ → ℝ) (x : σ) (l : List R) : incrementSum step (fun (y : σ) (a : R) => φ (step y a) - φ y - ψ y) x l = φ (List.foldl step x l) - φ x - incrementSum step (fun (y : σ) (x : R) => ψ y) x l

Increments of the form φ (step y a) - φ y - ψ y telescope.

theorem Epidemics.Kurtz.incrementSum_take {σ : Type u_1} {R : Type u_2} (step : σ → R → σ) (ψ : σ → ℝ) (x : σ) (l : List R) (k : ℕ) (hk : k ≤ l.length) : incrementSum step (fun (y : σ) (x : R) => ψ y) x (List.take k l) = ∑ j ∈ Finset.range k, ψ (List.foldl step x (List.take j l))

The sum of a state function along the first k rounds.

theorem Epidemics.Kurtz.incrementSum_neg {σ : Type u_1} {R : Type u_2} (step : σ → R → σ) (D : σ → R → ℝ) (x : σ) (l : List R) : incrementSum step (fun (y : σ) (a : R) => -D y a) x l = -incrementSum step D x l

Negated increments.

Coordinates

def Epidemics.Kurtz.coord : Fin 3 → ℝ × ℝ × ℝ →ₗ[ℝ] ℝ

The three coordinate functionals of ℝ × ℝ × ℝ.

Equations

• Epidemics.Kurtz.coord = ![LinearMap.fst ℝ ℝ (ℝ × ℝ), LinearMap.fst ℝ ℝ ℝ ∘ₗ LinearMap.snd ℝ ℝ (ℝ × ℝ), LinearMap.snd ℝ ℝ ℝ ∘ₗ LinearMap.snd ℝ ℝ (ℝ × ℝ)]

theorem Epidemics.Kurtz.coord_zero (p : ℝ × ℝ × ℝ) : (coord 0) p = p.1

theorem Epidemics.Kurtz.coord_one (p : ℝ × ℝ × ℝ) : (coord 1) p = p.2.1

theorem Epidemics.Kurtz.coord_two (p : ℝ × ℝ × ℝ) : (coord 2) p = p.2.2

theorem Epidemics.Kurtz.abs_coord_le_norm (j : Fin 3) (p : ℝ × ℝ × ℝ) : |(coord j) p| ≤ ‖p‖

theorem Epidemics.Kurtz.norm_le_of_forall_coord {p : ℝ × ℝ × ℝ} {δ : ℝ} (h : ∀ (j : Fin 3), |(coord j) p| ≤ δ) : ‖p‖ ≤ δ

The martingale increments

theorem Epidemics.Kurtz.count_le {N : ℕ} (c : Compartment) (x : Config N) : count c x ≤ N

Every count is at most N.

theorem Epidemics.Kurtz.norm_scaled_le_one {N : ℕ} (x : Config N) : ‖scaled x‖ ≤ 1

The scaled counts lie in the unit ball (sup norm).

theorem Epidemics.Kurtz.round_nonempty {β γ N : ℕ} (hN : 0 < N) (hβ : 0 < β) : Nonempty (Round N β γ)

The rounds form a nonempty type when N > 0 and β > 0.

noncomputable def Epidemics.Kurtz.mgIncr (β γ : ℕ) {N : ℕ} (j : Fin 3) (y : Config N) (ρ : Round N β γ) : ℝ

The martingale increment of the coordinate j: the change of coord j (scaled ·) in one step minus its conditional mean coord j (F (scaled y)) / ((β + γ) N).

Equations

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

theorem Epidemics.Kurtz.avg_mgIncr {β γ N : ℕ} (hN : 0 < N) (hβ : 0 < β) (j : Fin 3) (y : Config N) : Dynamics.avg (mgIncr β γ j y) = 0

The increments mgIncr are centred (the drift identity).

theorem Epidemics.Kurtz.abs_mgIncr_le {β γ N : ℕ} (hN : 0 < N) (hβ : 0 < β) (j : Fin 3) (y : Config N) (ρ : Round N β γ) : |mgIncr β γ j y ρ| ≤ 2 / ↑N

The increments mgIncr are bounded by 2 / N.

theorem Epidemics.Kurtz.incrementSum_mgIncr {β γ N : ℕ} (j : Fin 3) (x₀ : Config N) (l : List (Round N β γ)) (k : ℕ) (hk : k ≤ l.length) : incrementSum (step β γ) (mgIncr β γ j) x₀ (List.take k l) = (coord j) (scaled (List.foldl (step β γ) x₀ (List.take k l)) - scaled x₀ - ((↑β + ↑γ) * ↑N)⁻¹ • ∑ i ∈ Finset.range k, KermackMcKendrick.sirField (↑β) (↑γ) (scaled (List.foldl (step β γ) x₀ (List.take i l))))

Along the rounds l, the partial sums of mgIncr β γ j are the coordinates of X_k - X_0 - h ∑_{i<k} F (X_i).

The good event

theorem Epidemics.Kurtz.close_of_good {β γ 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 ≤ δ) (l : List (Round N β γ)) (hl : ↑l.length ≤ T * (↑β + ↑γ) * ↑N) (hgood : ∀ (j : Fin 3), ∀ k ≤ l.length, |incrementSum (step β γ) (mgIncr β γ j) x₀ (List.take k l)| ≤ δ) (k : ℕ) : k ≤ l.length → dist (scaled (List.foldl (step β γ) x₀ (List.take k l))) (s (↑k / ((↑β + ↑γ) * ↑N)), i (↑k / ((↑β + ↑γ) * ↑N)), r (↑k / ((↑β + ↑γ) * ↑N))) ≤ (dist (scaled x₀) (s 0, i 0, r 0) + δ + T * (2 * ↑β + ↑γ) / ↑N) * Real.exp ((2 * ↑β + ↑γ) * T)

Closeness on the good event. If, along rounds l of length n ≤ T (β + γ) N, the three coordinate martingales stay within δ at every step k ≤ n, then at every step k ≤ n the chain is within (dist (scaled x₀) x(0) + δ + T (2β + γ) / N) · exp((2β + γ) T) of the solution x at time k / ((β + γ) N).