The Kermack–McKendrick SIR model: the epidemic peak (EPI-7)

Above the threshold (R₀ s(0) > 1), the infected fraction increases until the susceptible fraction reaches 1 / R₀, and decreases afterwards; its maximum is i_max = i(0) + s(0) - 1 / R₀ - log(R₀ s(0)) / R₀ (Hethcote 2000, Theorem 2.1).

theorem Epidemics.KermackMcKendrick.IsSolution.exists_peak {β γ : ℝ} {s i r : ℝ → ℝ} (h : IsSolution β γ s i r) (hR : 1 < R₀ β γ * s 0) : ∃ tmax > 0, s tmax = 1 / R₀ β γ ∧ StrictMonoOn i (Set.Icc 0 tmax) ∧ StrictAntiOn i (Set.Ici tmax) ∧ i tmax = i 0 + s 0 - 1 / R₀ β γ - Real.log (R₀ β γ * s 0) / R₀ β γ

Threshold theorem, supercritical case (Hethcote 2000, Theorem 2.1): if R₀ s(0) > 1, there is a time tmax > 0 with s(tmax) = 1 / R₀ such that i is strictly increasing on [0, tmax] and strictly decreasing on [tmax, ∞), and the peak value is i(tmax) = i(0) + s(0) - 1 / R₀ - log(R₀ s(0)) / R₀.