Kermack–McKendrick SIR model

6 fully proved

SIR

StructureSolution of the Kermack–McKendrick SIR system#✓fully proved

(S, I, R) solves the Kermack–McKendrick SIR system with transmission rate β, removal rate γ and population size N for all times t ≥ 0: S' = -β S I / N, I' = β S I / N - γ I, R' = γ I.

structure IsSolution (β γ N : ℝ) (S I R : ℝ → ℝ) : Prop where
  /-- Susceptibles are infected at rate `β S I / N`. -/
  hasDerivAt_susceptible : ∀ t, 0 ≤ t → HasDerivAt S (-(β * S t * I t / N)) t
  /-- Infectives gain new infections and are removed at rate `γ`. -/
  hasDerivAt_infected : ∀ t, 0 ≤ t → HasDerivAt I (β * S t * I t / N - γ * I t) t
  /-- Removed individuals accumulate at rate `γ I`. -/
  hasDerivAt_removed : ∀ t, 0 ≤ t → HasDerivAt R (γ * I t) t

Used by 5

Used byThreshold theorem (Kermack–McKendrick 1927) · Final-size relation (Kermack–McKendrick 1927) · Final-size equation (Kermack–McKendrick 1927) · Conserved quantity behind the final-size relation · Conservation of the population

Is Solution

TheoremConservation of the population#✓fully proved

Along a solution, S + I + R is constant on [0, ∞).

theorem total_eq (h : IsSolution β γ N S I R) {t : ℝ} (ht : 0 ≤ t) :
    S t + I t + R t = S 0 + I 0 + R 0

Uses 1 · Used by 1

Statement usesSolution of the Kermack–McKendrick SIR system

Used byFinal-size equation (Kermack–McKendrick 1927)

TheoremThreshold theorem (Kermack–McKendrick 1927)#✓fully proved

If initially I(0) > 0, with γ > 0 and N > 0, the number of infectives initially increases, I'(0) > 0, iff R₀ S(0) / N > 1 with R₀ = β / γ.

theorem deriv_infected_pos_iff (h : IsSolution β γ N S I R) (hγ : 0 < γ) (hN : 0 < N)
    (hI : 0 < I 0) : 0 < deriv I 0 ↔ 1 < β / γ * S 0 / N

Uses 1

Statement usesSolution of the Kermack–McKendrick SIR system

TheoremConserved quantity behind the final-size relation#✓fully proved

For γ ≠ 0, the quantity S(t) e^{R₀ R(t) / N} (R₀ = β / γ) is constant along a solution on [0, ∞).

theorem susceptible_mul_exp_eq (h : IsSolution β γ N S I R) (hγ : γ ≠ 0) {t : ℝ}
    (ht : 0 ≤ t) :
    S t * exp (β / γ * R t / N) = S 0 * exp (β / γ * R 0 / N)

Uses 1 · Used by 1

Statement usesSolution of the Kermack–McKendrick SIR system

Used byFinal-size relation (Kermack–McKendrick 1927)

TheoremFinal-size relation (Kermack–McKendrick 1927)#✓fully proved

If along a solution (γ ≠ 0) S(t) → S∞ and R(t) → R∞ as t → ∞, then S∞ = S(0) e^{-R₀ (R∞ - R(0)) / N} with R₀ = β / γ. See final_size_eq for the classical form.

theorem final_size (h : IsSolution β γ N S I R) (hγ : γ ≠ 0) {Sinf Rinf : ℝ}
    (hS : Tendsto S atTop (𝓝 Sinf)) (hR : Tendsto R atTop (𝓝 Rinf)) :
    Sinf = S 0 * exp (-(β / γ * (Rinf - R 0) / N))

Uses 2 · Used by 1

Statement usesSolution of the Kermack–McKendrick SIR system

Proof usesConserved quantity behind the final-size relation

Used byFinal-size equation (Kermack–McKendrick 1927)

TheoremFinal-size equation (Kermack–McKendrick 1927)#✓fully proved

If the population is N = S + I + R, nobody is removed initially (R(0) = 0), γ ≠ 0, S(t) → S∞ and the epidemic dies out (I(t) → 0), then S∞ = S(0) e^{-R₀ (N - S∞) / N} with R₀ = β / γ.

theorem final_size_eq (h : IsSolution β γ N S I R) (hγ : γ ≠ 0)
    (hN : S 0 + I 0 + R 0 = N) (hR0 : R 0 = 0) {Sinf : ℝ} (hS : Tendsto S atTop (𝓝 Sinf))
    (hI : Tendsto I atTop (𝓝 0)) :
    Sinf = S 0 * exp (-(β / γ * (N - Sinf) / N))

Uses 3

Statement usesSolution of the Kermack–McKendrick SIR system

Proof usesFinal-size relation (Kermack–McKendrick 1927) · Conservation of the population

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.