The Kermack–McKendrick SIR model: basic API of solutions (EPI-7)

From IsSolution β γ s i r: the derivatives of the three components within [0, ∞), their continuity on [0, ∞), and the algebra of R₀ = β / γ.

theorem Epidemics.KermackMcKendrick.IsSolution.hasDerivWithinAt_s {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {t : ℝ} (ht : 0 ≤ t) : HasDerivWithinAt s (-(β * s t * i t)) (Set.Ici 0) t

s' = -β s i on [0, ∞).

theorem Epidemics.KermackMcKendrick.IsSolution.hasDerivWithinAt_i {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {t : ℝ} (ht : 0 ≤ t) : HasDerivWithinAt i (β * s t * i t - γ * i t) (Set.Ici 0) t

i' = β s i - γ i on [0, ∞).

theorem Epidemics.KermackMcKendrick.IsSolution.hasDerivWithinAt_r {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {t : ℝ} (ht : 0 ≤ t) : HasDerivWithinAt r (γ * i t) (Set.Ici 0) t

r' = γ i on [0, ∞).

theorem Epidemics.KermackMcKendrick.IsSolution.continuousOn_s {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) : ContinuousOn s (Set.Ici 0)

s is continuous on [0, ∞).

theorem Epidemics.KermackMcKendrick.IsSolution.continuousOn_i {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) : ContinuousOn i (Set.Ici 0)

i is continuous on [0, ∞).

theorem Epidemics.KermackMcKendrick.IsSolution.continuousOn_r {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) : ContinuousOn r (Set.Ici 0)

r is continuous on [0, ∞).

theorem Epidemics.KermackMcKendrick.IsSolution.hasDerivAt_r {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {t : ℝ} (ht : 0 < t) : HasDerivAt r (γ * i t) t

r' = γ i at every t > 0 (two-sided derivative).

theorem Epidemics.KermackMcKendrick.IsSolution.R₀_pos {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) : 0 < R₀ β γ

R₀ > 0.

theorem Epidemics.KermackMcKendrick.IsSolution.R₀_mul_gamma {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) : R₀ β γ * γ = β

R₀ γ = β.

theorem Epidemics.KermackMcKendrick.IsSolution.R₀_mul_le_one_iff {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {x : ℝ} : R₀ β γ * x ≤ 1 ↔ β * x ≤ γ

R₀ x ≤ 1 ↔ β x ≤ γ.

theorem Epidemics.KermackMcKendrick.IsSolution.R₀_mul_lt_one_iff {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {x : ℝ} : R₀ β γ * x < 1 ↔ β * x < γ

R₀ x < 1 ↔ β x < γ.

theorem Epidemics.KermackMcKendrick.IsSolution.one_lt_R₀_mul_iff {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {x : ℝ} : 1 < R₀ β γ * x ↔ γ < β * x

1 < R₀ x ↔ γ < β x.

theorem Epidemics.KermackMcKendrick.IsSolution.s_zero_lt_one {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) : s 0 < 1

s(0) < 1, since i(0) > 0, r(0) = 0 and the fractions sum to one.

theorem Epidemics.KermackMcKendrick.IsSolution.i_zero_add_s_zero {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) : i 0 + s 0 = 1

i(0) + s(0) = 1.

theorem Epidemics.KermackMcKendrick.IsSolution.s_mul_exp_eq {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {t : ℝ} (ht : 0 ≤ t) : s t * Real.exp (R₀ β γ * r t) = s 0

The first integral of Kermack–McKendrick (1927): s · exp(R₀ r) is constant on [0, ∞) (its derivative is exp(R₀ r) (-β s i + R₀ s γ i) = 0), hence equal to s(0) as r(0) = 0.

theorem Epidemics.KermackMcKendrick.IsSolution.half_mul_exp_le_i {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) (hs : ∀ (u : ℝ), 0 ≤ u → 0 < s u) {t : ℝ} (ht : 0 ≤ t) : i 0 / 2 * Real.exp (-γ * t) ≤ i t

A barrier keeping the infected fraction positive: if s > 0 on [0, ∞), then i(t) ≥ i(0) e^{-γ t} / 2 for all t ≥ 0. Where i would touch the barrier b, b' = -γ b = -γ i < β s i - γ i = i', so i cannot cross it.

theorem Epidemics.KermackMcKendrick.IsSolution.strictMonoOn_r_of_pos {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) (hi : ∀ (u : ℝ), 0 ≤ u → 0 < i u) : StrictMonoOn r (Set.Ici 0)

If i > 0 on [0, ∞), then r (with r' = γ i) is strictly increasing on [0, ∞).