The Kermack–McKendrick SIR model: definitions (EPI-7)

The deterministic SIR epidemic of Kermack and McKendrick (Proc. R. Soc. A 115, 1927), in the normalized form of Hethcote (The mathematics of infectious diseases, SIAM Review 42, 2000, system (2.2)): the fractions s, i, r of susceptible, infected and recovered individuals evolve by

s' = -β s i, i' = β s i - γ i, r' = γ i,

with contact rate β > 0 and recovery rate γ > 0. The basic reproduction number (Hethcote's contact number σ) is R₀ = β / γ.

A solution is taken as a hypothesis (it is not constructed): IsSolution β γ s i r says that t ↦ (s t, i t, r t) is an integral curve of the vector field sirField β γ on [0, ∞), in the sense of Mathlib's IsIntegralCurveOn (derivatives within [0, ∞), so one-sided at 0), and that it starts from s(0), i(0) > 0, r(0) = 0 and s(0) + i(0) + r(0) = 1.

noncomputable def Epidemics.KermackMcKendrick.R₀ (β γ : ℝ) : ℝ

The basic reproduction number R₀ = β / γ (Hethcote's contact number σ = β / γ).

Equations

• Epidemics.KermackMcKendrick.R₀ β γ = β / γ

def Epidemics.KermackMcKendrick.sirField (β γ : ℝ) (x : ℝ × ℝ × ℝ) : ℝ × ℝ × ℝ

The Kermack–McKendrick vector field (s, i, r) ↦ (-β s i, β s i - γ i, γ i) on ℝ × ℝ × ℝ (Hethcote 2000, system (2.2), with r' = γ i).

Equations

• Epidemics.KermackMcKendrick.sirField β γ x = (-(β * x.1 * x.2.1), β * x.1 * x.2.1 - γ * x.2.1, γ * x.2.1)

structure Epidemics.KermackMcKendrick.IsSolution (β γ : ℝ) (s i r : ℝ → ℝ) : Prop

The standing hypotheses of the Kermack–McKendrick SIR model (Hethcote 2000, §2.3, with r(0) = 0): positive rates β, γ; t ↦ (s t, i t, r t) solves s' = -β s i, i' = β s i - γ i, r' = γ i on [0, ∞) (an integral curve of sirField β γ on Set.Ici 0, with one-sided derivatives at 0); and the initial state has s(0), i(0) > 0, r(0) = 0, s(0) + i(0) + r(0) = 1.

• beta_pos : 0 < β

  The contact rate is positive.

• gamma_pos : 0 < γ

  The recovery rate is positive.

• isIntegralCurveOn : IsIntegralCurveOn (fun (t : ℝ) => (s t, i t, r t)) (fun (x : ℝ) => sirField β γ) (Set.Ici 0)

  (s, i, r) solves the SIR system on [0, ∞).

• s_zero_pos : 0 < s 0

  Some individuals are initially susceptible.

• i_zero_pos : 0 < i 0

  Some individuals are initially infected.

• r_zero : r 0 = 0

  Nobody has initially recovered.

• sum_zero : s 0 + i 0 + r 0 = 1

  The three fractions initially sum to one.