The Kermack–McKendrick SIR model: invariants and the threshold (EPI-7) #

For every solution of the Kermack–McKendrick system on [0, ∞) (IsSolution β γ s i r, see Epidemics.KermackMcKendrickDefs):

conservation s + i + r = 1 and positivity s, i > 0, r ≥ 0;
s is strictly decreasing and r strictly increasing (Hethcote 2000, Theorem 2.1);
the first integral s(t) = s(0) exp(-R₀ r(t)), from ds/dr = -R₀ s (Kermack–McKendrick 1927);
the threshold: if R₀ s(0) ≤ 1 then i is strictly decreasing (Hethcote 2000, Theorem 2.1), and i initially increases iff R₀ s(0) > 1.

Limits and the final-size equation are in Epidemics.KermackMcKendrickLimits, the epidemic peak in Epidemics.KermackMcKendrickPeak.

source

theorem Epidemics.KermackMcKendrick.IsSolution.sum_eq_one {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {t : ℝ} (ht : 0 ≤ t) :

s t + i t + r t = 1

Conservation of the population: s(t) + i(t) + r(t) = 1 for all t ≥ 0 (the derivative of s + i + r vanishes; Hethcote 2000, §2.3).

source

theorem Epidemics.KermackMcKendrick.IsSolution.s_pos {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {t : ℝ} (ht : 0 ≤ t) :

0 < s t

Positivity of the susceptible fraction: s(t) > 0 for all t ≥ 0.

source

theorem Epidemics.KermackMcKendrick.IsSolution.i_pos {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {t : ℝ} (ht : 0 ≤ t) :

0 < i t

Positivity of the infected fraction: i(t) > 0 for all t ≥ 0.

source

theorem Epidemics.KermackMcKendrick.IsSolution.r_nonneg {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {t : ℝ} (ht : 0 ≤ t) :

0 ≤ r t

Nonnegativity of the recovered fraction: r(t) ≥ 0 for all t ≥ 0.

source

theorem Epidemics.KermackMcKendrick.IsSolution.strictAntiOn_s {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) :

StrictAntiOn s (Set.Ici 0)

The susceptible fraction is strictly decreasing on [0, ∞) (Hethcote 2000, Theorem 2.1).

source

theorem Epidemics.KermackMcKendrick.IsSolution.strictMonoOn_r {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) :

StrictMonoOn r (Set.Ici 0)

The recovered fraction is strictly increasing on [0, ∞).

source

theorem Epidemics.KermackMcKendrick.IsSolution.s_eq_mul_exp {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {t : ℝ} (ht : 0 ≤ t) :

s t = s 0 * Real.exp (-(R₀ β γ * r t))

The first integral of Kermack–McKendrick (1927): since ds/dr = -R₀ s and r(0) = 0, s(t) = s(0) exp(-R₀ r(t)) for all t ≥ 0.

source

theorem Epidemics.KermackMcKendrick.IsSolution.strictAntiOn_i {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) (hR : R₀ β γ * s 0 ≤ 1) :

StrictAntiOn i (Set.Ici 0)

Threshold theorem, subcritical case (Hethcote 2000, Theorem 2.1): if R₀ s(0) ≤ 1, the infected fraction is strictly decreasing on [0, ∞), so there is no epidemic.

source

theorem Epidemics.KermackMcKendrick.IsSolution.initially_increasing_iff {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) :

(∃ ε > 0, StrictMonoOn i (Set.Icc 0 ε)) ↔ 1 < R₀ β γ * s 0

Threshold theorem (Kermack–McKendrick 1927; Hethcote 2000, Theorem 2.1): the infected fraction initially increases, i.e. is strictly increasing on some interval [0, ε] with ε > 0, iff R₀ s(0) > 1.