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

For a solution x(t) = (s t, i t, r t) of the Kermack–McKendrick system on [0, ∞), given only as an integral curve of sirField β γ (no IsSolution: the initial point is any point of the simplex):

• the simplex is invariant: s, i, r ≥ 0 and s + i + r = 1 on [0, ∞) (first integral s exp((β/γ) r) for s, integrating factor i exp(-∫ (β s - γ)) for i, monotonicity for r), so ‖x(t)‖ ≤ 1 in the sup norm of ℝ × ℝ × ℝ;
• on the unit ball, sirField β γ is (2β + γ)-Lipschitz and bounded by β + γ;
• the Euler step error ‖x(t+h) - x(t) - h F(x(t))‖ ≤ (2β + γ)(β + γ) h² (mean value inequality).

Components of an integral curve

theorem Epidemics.Kurtz.sir_hasDerivWithinAt_s {β γ : ℝ} {s i r : ℝ → ℝ} (hx : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField β γ) (Set.Ici 0)) {t : ℝ} (ht : 0 ≤ t) : HasDerivWithinAt s (-(β * s t * i t)) (Set.Ici 0) t

theorem Epidemics.Kurtz.sir_hasDerivWithinAt_i {β γ : ℝ} {s i r : ℝ → ℝ} (hx : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField β γ) (Set.Ici 0)) {t : ℝ} (ht : 0 ≤ t) : HasDerivWithinAt i (β * s t * i t - γ * i t) (Set.Ici 0) t

theorem Epidemics.Kurtz.sir_hasDerivWithinAt_r {β γ : ℝ} {s i r : ℝ → ℝ} (hx : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField β γ) (Set.Ici 0)) {t : ℝ} (ht : 0 ≤ t) : HasDerivWithinAt r (γ * i t) (Set.Ici 0) t

theorem Epidemics.Kurtz.sir_sum_eq {β γ : ℝ} {s i r : ℝ → ℝ} (hx : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField β γ) (Set.Ici 0)) {t : ℝ} (ht : 0 ≤ t) : s t + i t + r t = s 0 + i 0 + r 0

Conservation: s + i + r is constant on [0, ∞).

theorem Epidemics.Kurtz.sir_s_mul_exp {β γ : ℝ} {s i r : ℝ → ℝ} (hx : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField β γ) (Set.Ici 0)) (hγ : γ ≠ 0) {t : ℝ} (ht : 0 ≤ t) : s t * Real.exp (β / γ * r t) = s 0 * Real.exp (β / γ * r 0)

The first integral s · exp((β/γ) r) is constant on [0, ∞) (Kermack–McKendrick 1927).

theorem Epidemics.Kurtz.sir_s_nonneg {β γ : ℝ} {s i r : ℝ → ℝ} (hx : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField β γ) (Set.Ici 0)) (hγ : γ ≠ 0) (hs : 0 ≤ s 0) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ s t

s ≥ 0 on [0, ∞) if s 0 ≥ 0.

theorem Epidemics.Kurtz.sir_i_nonneg {β γ : ℝ} {s i r : ℝ → ℝ} (hx : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField β γ) (Set.Ici 0)) (hi : 0 ≤ i 0) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ i t

i ≥ 0 on [0, ∞) if i 0 ≥ 0: with G t = ∫₀ᵗ (β s - γ) (for s extended by s 0 to negative times), i · exp(-G) is constant.

theorem Epidemics.Kurtz.sir_r_ge {β γ : ℝ} {s i r : ℝ → ℝ} (hx : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField β γ) (Set.Ici 0)) (hγ : 0 ≤ γ) (hi : 0 ≤ i 0) {t : ℝ} (ht : 0 ≤ t) : r 0 ≤ r t

r ≥ r 0 on [0, ∞) when i ≥ 0 there and γ ≥ 0 (r' = γ i ≥ 0).

theorem Epidemics.Kurtz.sir_norm_le_one {β γ : ℝ} {s i r : ℝ → ℝ} (hx : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField β γ) (Set.Ici 0)) (hγ : 0 < γ) (hs : 0 ≤ s 0) (hi : 0 ≤ i 0) (hr : 0 ≤ r 0) (hsum : s 0 + i 0 + r 0 = 1) {t : ℝ} (ht : 0 ≤ t) : ‖(s t, i t, r t)‖ ≤ 1

Invariance of the simplex: a solution started in the simplex stays in the sup-norm unit ball (indeed in the simplex) on [0, ∞).

The field on the unit ball

theorem Epidemics.Kurtz.abs_mul_sub_mul_le {a b c d : ℝ} (ha : |a| ≤ 1) (hd : |d| ≤ 1) : |a * b - c * d| ≤ |b - d| + |a - c|

|a b - c d| ≤ |b - d| + |a - c| when |a|, |d| ≤ 1.

theorem Epidemics.Kurtz.norm_sirField_sub_le {β γ : ℝ} (hβ : 0 ≤ β) (hγ : 0 ≤ γ) {p q : ℝ × ℝ × ℝ} (hp : ‖p‖ ≤ 1) (hq : ‖q‖ ≤ 1) : ‖KermackMcKendrick.sirField β γ p - KermackMcKendrick.sirField β γ q‖ ≤ (2 * β + γ) * ‖p - q‖

On the unit ball, the Kermack–McKendrick field is (2β + γ)-Lipschitz (sup norm).

theorem Epidemics.Kurtz.norm_sirField_le {β γ : ℝ} (hβ : 0 ≤ β) (hγ : 0 ≤ γ) {p : ℝ × ℝ × ℝ} (hp : ‖p‖ ≤ 1) : ‖KermackMcKendrick.sirField β γ p‖ ≤ β + γ

On the unit ball, the Kermack–McKendrick field is bounded by β + γ (sup norm).

Euler step error

theorem Epidemics.Kurtz.sir_euler_le {β γ : ℝ} {s i r : ℝ → ℝ} (hx : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => KermackMcKendrick.sirField β γ) (Set.Ici 0)) (hβ : 0 ≤ β) (hγ : 0 ≤ γ) {t h : ℝ} (ht : 0 ≤ t) (hh : 0 ≤ h) (hball : ∀ u ∈ Set.Icc t (t + h), ‖(s u, i u, r u)‖ ≤ 1) : ‖(s (t + h), i (t + h), r (t + h)) - (s t, i t, r t) - h • KermackMcKendrick.sirField β γ (s t, i t, r t)‖ ≤ (2 * β + γ) * (β + γ) * h ^ 2

Euler step error. If the solution stays in the unit ball on [t, t + h], then ‖x(t + h) - x(t) - h F(x(t))‖ ≤ (2β + γ)(β + γ) h².