The Kermack–McKendrick SIR model: limits and the final-size equation (EPI-7)

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

• the epidemic dies out, i(t) → 0, and the limit s∞ = lim s(t) exists; then r(t) → 1 - s∞;
• the final-size equation s∞ = s(0) exp(-R₀ (1 - s∞)) (Kermack–McKendrick 1927; Hethcote 2000, Theorem 2.1, with i(0) + s(0) = 1);
• 0 < s∞ < 1 / R₀, and s∞ is the unique root of the final-size equation in (0, 1 / R₀] (Hethcote 2000, Theorem 2.1) and also in (0, 1].

theorem Epidemics.KermackMcKendrick.IsSolution.tendsto_i {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) : Filter.Tendsto i Filter.atTop (nhds 0)

The epidemic dies out: i(t) → 0 as t → ∞ (Hethcote 2000, Theorem 2.1).

theorem Epidemics.KermackMcKendrick.IsSolution.exists_tendsto_s {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) : ∃ (sInfty : ℝ), Filter.Tendsto s Filter.atTop (nhds sInfty)

The final susceptible fraction s∞ = lim_{t → ∞} s(t) exists.

theorem Epidemics.KermackMcKendrick.IsSolution.tendsto_r {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {sInfty : ℝ} (hs : Filter.Tendsto s Filter.atTop (nhds sInfty)) : Filter.Tendsto r Filter.atTop (nhds (1 - sInfty))

The recovered fraction tends to 1 - s∞ (since i(t) → 0 and s + i + r = 1).

theorem Epidemics.KermackMcKendrick.IsSolution.final_size {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {sInfty : ℝ} (hs : Filter.Tendsto s Filter.atTop (nhds sInfty)) : sInfty = s 0 * Real.exp (-(R₀ β γ * (1 - sInfty)))

The final-size equation (Kermack–McKendrick 1927; Hethcote 2000, Theorem 2.1 with i(0) + s(0) = 1): s∞ = s(0) exp(-R₀ (1 - s∞)).

theorem Epidemics.KermackMcKendrick.IsSolution.limit_pos {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {sInfty : ℝ} (hs : Filter.Tendsto s Filter.atTop (nhds sInfty)) : 0 < sInfty

Some individuals escape the epidemic: s∞ > 0 (Hethcote 2000, Theorem 2.1).

theorem Epidemics.KermackMcKendrick.IsSolution.R₀_mul_limit_lt_one {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {sInfty : ℝ} (hs : Filter.Tendsto s Filter.atTop (nhds sInfty)) : R₀ β γ * sInfty < 1

The epidemic ends below the threshold: R₀ s∞ < 1, i.e. s∞ < 1 / R₀ (Hethcote 2000, Theorem 2.1).

theorem Epidemics.KermackMcKendrick.IsSolution.final_size_unique {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {sInfty : ℝ} (hs : Filter.Tendsto s Filter.atTop (nhds sInfty)) {x : ℝ} (hx0 : 0 < x) (hx1 : R₀ β γ * x ≤ 1) (hx : x = s 0 * Real.exp (-(R₀ β γ * (1 - x)))) : x = sInfty

Uniqueness (Hethcote 2000, Theorem 2.1): s∞ is the only root x of the final-size equation x = s(0) exp(-R₀ (1 - x)) with 0 < x ≤ 1 / R₀.

theorem Epidemics.KermackMcKendrick.IsSolution.final_size_unique_of_le_one {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {sInfty : ℝ} (hs : Filter.Tendsto s Filter.atTop (nhds sInfty)) {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) (hx : x = s 0 * Real.exp (-(R₀ β γ * (1 - x)))) : x = sInfty

Uniqueness among fractions: s∞ is the only root x of the final-size equation x = s(0) exp(-R₀ (1 - x)) with 0 < x ≤ 1.