Euler–Lotka equation and the reproduction number

DefinitionReproductive number from growth rate and generation interval#✓fully proved

The reproductive number implied by growth rate r and generation-interval law g: R = 1 / M_g(-r) (Wallinga–Lipsitch 2007, eq. 2.9).

noncomputable def reproductionNumber (g : Measure ℝ) (r : ℝ) : ℝ :=
  (mgf id g (-r))⁻¹

Used by 7

Used byEuler–Lotka · Fixed generation interval · Exponential generation interval · Gamma generation interval · Jensen bound · More spread lowers R · Positivity of the reproductive number

DefinitionConvex order#✓fully proved

g₁ ≤cx g₂ if ∫ φ dg₁ ≤ ∫ φ dg₂ for every convex φ : ℝ → ℝ that is integrable under both laws (Shaked–Shanthikumar 2007, §3.A).

def ConvexOrderLE (g₁ g₂ : Measure ℝ) : Prop :=
  ∀ φ : ℝ → ℝ, ConvexOn ℝ Set.univ φ → Integrable φ g₁ → Integrable φ g₂ →
    ∫ a, φ a ∂g₁ ≤ ∫ a, φ a ∂g₂

Used by 1

Used byMore spread lowers R

TheoremRenewal equation for exponential growth#✓fully proved

For c ≠ 0, the exponential b(t) = c e^{r t} solves b(t) = R ∫ b(t - a) g(da) for every t iff R M_g(-r) = 1. This is meaningful when a ↦ e^{-r a} is g-integrable; otherwise Lean's integral and M_g(-r) are both 0 and both sides of the equivalence are false.

theorem renewal_exp_iff (g : Measure ℝ) {r c : ℝ} (R : ℝ) (hc : c ≠ 0) :
    (∀ t, c * exp (r * t) = R * ∫ a, c * exp (r * (t - a)) ∂g) ↔ R * mgf id g (-r) = 1

Used by 1

Used byEuler–Lotka

TheoremEuler–Lotka#✓fully proved

Under the hypotheses of renewal_exp_iff, exponential growth at rate r solves the renewal equation iff R = 1 / M_g(-r).

theorem renewal_exp_iff_reproductionNumber (g : Measure ℝ) [IsProbabilityMeasure g]
    {r c : ℝ} (R : ℝ) (hc : c ≠ 0) (hint : Integrable (fun a => exp (-r * a)) g) :
    (∀ t, c * exp (r * t) = R * ∫ a, c * exp (r * (t - a)) ∂g) ↔
      R = reproductionNumber g r

Uses 2

Statement usesReproductive number from growth rate and generation interval

Proof usesRenewal equation for exponential growth

TheoremPositivity of the reproductive number#✓fully proved

The reproductive number is positive when M_g(-r) is finite.

theorem reproductionNumber_pos (g : Measure ℝ) [IsProbabilityMeasure g] {r : ℝ}
    (hint : Integrable (fun a => exp (-r * a)) g) : 0 < reproductionNumber g r

Uses 1

Statement usesReproductive number from growth rate and generation interval

TheoremFixed generation interval#✓fully proved

Fixed generation interval T: R = e^{r T} (for all real r, T).

theorem reproductionNumber_dirac (r T : ℝ) : reproductionNumber (Measure.dirac T) r =
    exp (r * T)

Uses 1

Statement usesReproductive number from growth rate and generation interval

TheoremGamma generation interval#✓fully proved

Gamma generation interval with shape α > 0 and rate β > 0: for r > -β, R = (1 + r / β)^α.

theorem reproductionNumber_gammaMeasure {α β r : ℝ} (hα : 0 < α) (hβ : 0 < β)
    (hr : -β < r) : reproductionNumber (gammaMeasure α β) r = (1 + r / β) ^ α

Uses 2 · Used by 1

Statement usesReproductive number from growth rate and generation interval

Proof usesMoment generating function of the gamma distribution

Used byExponential generation interval

TheoremExponential generation interval#✓fully proved

Exponential generation interval with mean T > 0 (rate 1 / T): for r T > -1, R = 1 + r T (Wallinga–Lipsitch 2007, eq. 3.1).

theorem reproductionNumber_expMeasure {r T : ℝ} (hT : 0 < T) (hr : -1 < r * T) :
    reproductionNumber (expMeasure T⁻¹) r = 1 + r * T

Uses 2

Statement usesReproductive number from growth rate and generation interval

Proof usesGamma generation interval

TheoremMore spread lowers R#✓fully proved

If g₁ ≤cx g₂ and both have finite M(-r), then R(g₂) ≤ R(g₁) at growth rate r (any real r). In particular, among generation intervals with a given mean, the fixed interval maximizes R.

theorem reproductionNumber_le_of_convexOrderLE {g₁ g₂ : Measure ℝ} [IsProbabilityMeasure g₁]
    [IsProbabilityMeasure g₂] (h : ConvexOrderLE g₁ g₂) {r : ℝ}
    (h₁ : Integrable (fun a => exp (-r * a)) g₁) (h₂ : Integrable (fun a => exp (-r * a)) g₂) :
    reproductionNumber g₂ r ≤ reproductionNumber g₁ r

Uses 2

Statement usesConvex order · Reproductive number from growth rate and generation interval

TheoremJensen bound#✓fully proved

If the generation interval has finite mean T̄ = ∫ a g(da) and finite M_g(-r), then R ≤ e^{r T̄} (any real r); Wallinga and Lipsitch (2007, §3) note that the fixed interval gives this upper bound.

theorem reproductionNumber_le_exp_mean (g : Measure ℝ) [IsProbabilityMeasure g] {r : ℝ}
    (hid : Integrable id g) (hint : Integrable (fun a => exp (-r * a)) g) :
    reproductionNumber g r ≤ exp (r * ∫ a, a ∂g)

Uses 1

Statement usesReproductive number from growth rate and generation interval

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.