The Kermack–McKendrick SIR model: helpers for the limits (EPI-7)

• s and r converge (monotone and bounded on [0, ∞));
• every limit of i is 0: if i → L > 0, then r' = γ i ≥ γ L / 2 eventually, and the mean value theorem makes r grow by more than 1, contradicting 0 ≤ r < 1;
• a limit of s lies strictly below every value of s on [0, ∞);
• a root x of the final-size equation satisfies log x - R₀ x = log s(0) - R₀.

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

r(t) < 1 for all t ≥ 0, since s(t), i(t) > 0 and s + i + r = 1.

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

The susceptible fraction converges as t → ∞ (antitone, bounded below by 0).

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

The recovered fraction converges as t → ∞ (monotone, bounded above by 1).

theorem Epidemics.KermackMcKendrick.IsSolution.not_tendsto_i_pos {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {L : ℝ} (hL : 0 < L) (hi : Filter.Tendsto i Filter.atTop (nhds L)) : False

A limit of i cannot be positive: otherwise r would grow without bound.

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

Every limit of i is 0.

theorem Epidemics.KermackMcKendrick.IsSolution.limit_lt_s {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {L : ℝ} (hs : Filter.Tendsto s Filter.atTop (nhds L)) {t : ℝ} (ht : 0 ≤ t) : L < s t

A limit L of s lies strictly below s(t) for every t ≥ 0.

theorem Epidemics.KermackMcKendrick.IsSolution.log_sub_eq_of_final_size {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) {x : ℝ} (hx : x = s 0 * Real.exp (-(R₀ β γ * (1 - x)))) : Real.log x - R₀ β γ * x = Real.log (s 0) - R₀ β γ

A root x of the final-size equation x = s(0) exp(-R₀ (1 - x)) satisfies log x - R₀ x = log s(0) - R₀.