Kurtz's law of large numbers for SIR: discrete stability (CRN-2, helpers)

The deterministic half of the law of large numbers. A sequence X k in ℝ × ℝ × ℝ that follows the Euler scheme X (k+1) ≈ X k + h F (X k) up to a martingale part bounded by δ (‖X k - X 0 - h ∑_{j<k} F (X j)‖ ≤ δ) stays close to a sequence y k with one-step Euler error at most η, provided F is Lip-Lipschitz along the two sequences:

‖X k - y k‖ ≤ (‖X 0 - y 0‖ + δ + n η) · exp(h Lip k) for k ≤ n.

The Grönwall step uses Mathlib's discrete_gronwall (applied to the partial sums, frozen after step n), in the sum form le_mul_exp_of_le_add_sum.

theorem Epidemics.Kurtz.le_mul_exp_of_le_add_sum {u : ℕ → ℝ} {A b : ℝ} {n : ℕ} (hA : 0 ≤ A) (hb : 0 ≤ b) (hu0 : ∀ (k : ℕ), 0 ≤ u k) (hu : ∀ k ≤ n, u k ≤ A + b * ∑ j ∈ Finset.range k, u j) (k : ℕ) : k ≤ n → u k ≤ A * Real.exp (b * ↑k)

Discrete Grönwall inequality, sum form, on a finite range (from Mathlib's discrete_gronwall): if 0 ≤ u k ≤ A + b ∑_{j<k} u j for k ≤ n, then u k ≤ A exp(b k).

theorem Epidemics.Kurtz.norm_sub_sum_le {F : ℝ × ℝ × ℝ → ℝ × ℝ × ℝ} {y : ℕ → ℝ × ℝ × ℝ} {h η : ℝ} {n : ℕ} (hy : ∀ j < n, ‖y (j + 1) - y j - h • F (y j)‖ ≤ η) (k : ℕ) : k ≤ n → ‖y k - y 0 - h • ∑ j ∈ Finset.range k, F (y j)‖ ≤ ↑k * η

The Euler errors accumulate linearly: ‖y k - y 0 - h ∑_{j<k} F (y j)‖ ≤ k η when every step errs by at most η.

theorem Epidemics.Kurtz.norm_sub_le_of_euler {F : ℝ × ℝ × ℝ → ℝ × ℝ × ℝ} {X y : ℕ → ℝ × ℝ × ℝ} {Lip h δ η : ℝ} {n : ℕ} (hLip0 : 0 ≤ Lip) (hh : 0 ≤ h) (hδ : 0 ≤ δ) (hη : 0 ≤ η) (hLip : ∀ j < n, ‖F (X j) - F (y j)‖ ≤ Lip * ‖X j - y j‖) (hX : ∀ k ≤ n, ‖X k - X 0 - h • ∑ j ∈ Finset.range k, F (X j)‖ ≤ δ) (hy : ∀ j < n, ‖y (j + 1) - y j - h • F (y j)‖ ≤ η) (k : ℕ) : k ≤ n → ‖X k - y k‖ ≤ (‖X 0 - y 0‖ + δ + ↑n * η) * Real.exp (h * Lip * ↑k)

Discrete stability of the Euler scheme. If X follows the Euler scheme of F up to a martingale part bounded by δ, y follows it up to one-step errors η, and F is Lip-Lipschitz between X j and y j, then ‖X k - y k‖ ≤ (‖X 0 - y 0‖ + δ + n η) exp(h Lip k) for k ≤ n.