One-variable calculus on [0, ∞) for the Kermack–McKendrick model (EPI-7)

Generic helpers, independent of the SIR system:

• a function whose derivative within [0, ∞) vanishes there is constant on [0, ∞);
• a function differentiable within [0, ∞) whose derivative is positive (negative) on the interior of a convex subset D ⊆ [0, ∞) is strictly monotone (antitone) on D;
• a function monotone (antitone) on [0, ∞) and bounded above (below) there converges at +∞;
• monotonicity of x ↦ log x - R x: increasing where R x ≤ 1, decreasing where R x ≥ 1 (used for the uniqueness of the final size, Hethcote 2000, Theorem 2.1).

theorem Epidemics.KermackMcKendrick.eq_of_hasDerivWithinAt_zero {f : ℝ → ℝ} (hf : ∀ (t : ℝ), 0 ≤ t → HasDerivWithinAt f 0 (Set.Ici 0) t) {t : ℝ} (ht : 0 ≤ t) : f t = f 0

A function whose derivative within [0, ∞) vanishes at every point of [0, ∞) is constant on [0, ∞).

theorem Epidemics.KermackMcKendrick.continuousOn_of_hasDerivWithinAt {f f' : ℝ → ℝ} (hf : ∀ (t : ℝ), 0 ≤ t → HasDerivWithinAt f (f' t) (Set.Ici 0) t) : ContinuousOn f (Set.Ici 0)

A function differentiable within [0, ∞) is continuous on [0, ∞).

theorem Epidemics.KermackMcKendrick.deriv_eq_of_mem_interior {f f' : ℝ → ℝ} (hf : ∀ (t : ℝ), 0 ≤ t → HasDerivWithinAt f (f' t) (Set.Ici 0) t) {D : Set ℝ} (hD0 : D ⊆ Set.Ici 0) {t : ℝ} (ht : t ∈ interior D) : deriv f t = f' t

At an interior point of D ⊆ [0, ∞), the derivative within [0, ∞) is the derivative.

theorem Epidemics.KermackMcKendrick.strictMonoOn_of_hasDerivWithinAt_pos {f f' : ℝ → ℝ} (hf : ∀ (t : ℝ), 0 ≤ t → HasDerivWithinAt f (f' t) (Set.Ici 0) t) {D : Set ℝ} (hD : Convex ℝ D) (hD0 : D ⊆ Set.Ici 0) (hpos : ∀ t ∈ interior D, 0 < f' t) : StrictMonoOn f D

Positive derivative on the interior of a convex D ⊆ [0, ∞) gives strict monotonicity on D.

theorem Epidemics.KermackMcKendrick.strictAntiOn_of_hasDerivWithinAt_neg {f f' : ℝ → ℝ} (hf : ∀ (t : ℝ), 0 ≤ t → HasDerivWithinAt f (f' t) (Set.Ici 0) t) {D : Set ℝ} (hD : Convex ℝ D) (hD0 : D ⊆ Set.Ici 0) (hneg : ∀ t ∈ interior D, f' t < 0) : StrictAntiOn f D

Negative derivative on the interior of a convex D ⊆ [0, ∞) gives strict antitonicity on D.

theorem Epidemics.KermackMcKendrick.exists_tendsto_of_antitoneOn {f : ℝ → ℝ} (hf : AntitoneOn f (Set.Ici 0)) {m : ℝ} (hm : ∀ (t : ℝ), 0 ≤ t → m ≤ f t) : ∃ (L : ℝ), Filter.Tendsto f Filter.atTop (nhds L)

A function antitone on [0, ∞) and bounded below there converges as t → ∞.

theorem Epidemics.KermackMcKendrick.exists_tendsto_of_monotoneOn {f : ℝ → ℝ} (hf : MonotoneOn f (Set.Ici 0)) {M : ℝ} (hM : ∀ (t : ℝ), 0 ≤ t → f t ≤ M) : ∃ (L : ℝ), Filter.Tendsto f Filter.atTop (nhds L)

A function monotone on [0, ∞) and bounded above there converges as t → ∞.

theorem Epidemics.KermackMcKendrick.log_sub_mul_lt_of_mul_le_one {R a b : ℝ} (ha : 0 < a) (hab : a < b) (hb : R * b ≤ 1) : Real.log a - R * a < Real.log b - R * b

x ↦ log x - R x is strictly increasing on (0, 1 / R]: if 0 < a < b and R b ≤ 1 then log a - R a < log b - R b.

theorem Epidemics.KermackMcKendrick.log_sub_mul_lt_of_one_le_mul {R a b : ℝ} (ha : 0 < a) (hab : a < b) (ha1 : 1 ≤ R * a) : Real.log b - R * b < Real.log a - R * a

x ↦ log x - R x is strictly decreasing on [1 / R, ∞): if 0 < a < b and 1 ≤ R a then log b - R b < log a - R a.