Next-generation matrix and the basic reproduction number

DefinitionBasic reproduction number of the next-generation matrix#✓fully proved

The basic reproduction number R₀ = ρ(F V⁻¹): the spectral radius (largest modulus of a complex eigenvalue) of the next-generation matrix F V⁻¹ (van den Driessche–Watmough 2002, Eq. (4)). It is meaningful when V is invertible (for a nonsingular M-matrix it is).

noncomputable def R0 (F V : Matrix ι ι ℝ) : ℝ :=
  (spectralRadius ℂ ((F * V⁻¹).map (algebraMap ℝ ℂ))).toReal

Used by 4

Used byR₀ > 1 gives an unstable mode · Threshold theorem, instability half, spectral form · Threshold theorem, stability half, conditional decay form · R₀ as a threshold for the linearized infected subsystem

TheoremR₀ as a threshold for the linearized infected subsystem#✓fully proved

R₀ as a threshold for the linearized infected subsystem (van den Driessche–Watmough 2002, proof of Theorem 2). If F is entrywise nonnegative and V is a nonsingular M-matrix, then every eigenvalue of F - V has negative real part iff R₀ = ρ(F V⁻¹) < 1.

theorem isHurwitz_sub_iff_R0_lt_one {F V : Matrix ι ι ℝ} (hF : ∀ i j, 0 ≤ F i j)
    (hV : V.IsNonsingularMMatrix) : (F - V).IsHurwitz ↔ R0 F V < 1

Uses 7 · Used by 1

Statement usesBasic reproduction number of the next-generation matrix · Hurwitz matrix · Nonsingular M-matrix

Proof usesInverse positivity of M-matrices · Nonsingular M-matrices are invertible · Z-matrix · Collatz–Wielandt lower bound

Used byThreshold theorem, stability half, conditional decay form

TheoremR₀ > 1 gives an unstable mode#✓fully proved

R₀ > 1 gives an unstable mode (van den Driessche–Watmough 2002, proof of Theorem 2). If F is entrywise nonnegative and V is a nonsingular M-matrix, then F - V has an eigenvalue with positive real part iff R₀ = ρ(F V⁻¹) > 1.

theorem exists_re_pos_iff_one_lt_R0 {F V : Matrix ι ι ℝ} (hF : ∀ i j, 0 ≤ F i j)
    (hV : V.IsNonsingularMMatrix) :
    (∃ μ ∈ spectrum ℂ ((F - V).map (algebraMap ℝ ℂ)), 0 < μ.re) ↔ 1 < R0 F V

Uses 7 · Used by 1

Statement usesBasic reproduction number of the next-generation matrix · Nonsingular M-matrix

Proof usesHurwitz matrix · Inverse positivity of M-matrices · Nonsingular M-matrices are invertible · Z-matrix · Collatz–Wielandt lower bound

Used byThreshold theorem, instability half, spectral form

TheoremEigenvalues of a block lower-triangular matrix#✓fully proved

The complex eigenvalues of a block lower-triangular real matrix [[A, 0], [C, D]] are those of A together with those of D.

theorem mem_spectrum_fromBlocks_zero₁₂ {A : Matrix ι ι ℝ} {C : Matrix κ ι ℝ}
    {D : Matrix κ κ ℝ} {μ : ℂ} :
    μ ∈ spectrum ℂ ((fromBlocks A 0 C D).map (algebraMap ℝ ℂ)) ↔
      μ ∈ spectrum ℂ (A.map (algebraMap ℝ ℂ)) ∨ μ ∈ spectrum ℂ (D.map (algebraMap ℝ ℂ))

Used by 2

Used byThreshold theorem, instability half, spectral form · Hurwitz criterion for block lower-triangular matrices

TheoremHurwitz criterion for block lower-triangular matrices#✓fully proved

A block lower-triangular real matrix [[A, 0], [C, D]] is Hurwitz iff both diagonal blocks are.

theorem isHurwitz_fromBlocks_zero₁₂_iff {A : Matrix ι ι ℝ} {C : Matrix κ ι ℝ}
    {D : Matrix κ κ ℝ} : (fromBlocks A 0 C D).IsHurwitz ↔ A.IsHurwitz ∧ D.IsHurwitz

Uses 2 · Used by 1

Statement usesHurwitz matrix

Proof usesEigenvalues of a block lower-triangular matrix

Used byThreshold theorem, stability half, conditional decay form

TheoremThreshold theorem, stability half, conditional decay form#✓fully proved

Threshold theorem, stability half, conditional decay form (van den Driessche–Watmough 2002, Theorem 2). Let x₀ be an equilibrium of x' = f(x) on ℝ^{ι ⊕ κ} (infected compartments ι, the others κ), with f differentiable at x₀ and Jacobian [[F - V, 0], [C, D]] as in their Lemma 1, where F ≥ 0, V is a nonsingular M-matrix and D is Hurwitz. If R₀ = ρ(F V⁻¹) < 1, then every solution defined on all of [0, ∞) starting near x₀ decays exponentially. The statement concerns only solutions defined on all of [0, ∞), so it is not by itself local exponential stability.

theorem globalSolution_decay_of_R0_lt_one {f : (ι ⊕ κ → ℝ) → ι ⊕ κ → ℝ}
    {x₀ : ι ⊕ κ → ℝ} {F V : Matrix ι ι ℝ} {C : Matrix κ ι ℝ} {D : Matrix κ κ ℝ}
    (hf : f x₀ = 0)
    (hfJ : HasFDerivAt f
      (LinearMap.toContinuousLinearMap (Matrix.toLin' (fromBlocks (F - V) 0 C D))) x₀)
    (hF : ∀ i j, 0 ≤ F i j) (hV : V.IsNonsingularMMatrix) (hD : D.IsHurwitz)
    (hR0 : R0 F V < 1) :
    ∃ δ K α : ℝ, 0 < δ ∧ 0 < K ∧ 0 < α ∧ ∀ x : ℝ → ι ⊕ κ → ℝ,
      (∀ t, 0 ≤ t → HasDerivAt x (f (x t)) t) → ‖x 0 - x₀‖ < δ →
        ∀ t, 0 ≤ t → ‖x t - x₀‖ ≤ K * Real.exp (-(α * t)) * ‖x 0 - x₀‖

Uses 6

Statement usesBasic reproduction number of the next-generation matrix · Hurwitz matrix · Nonsingular M-matrix

Proof usesLyapunov's indirect method (linearized stability), conditional decay form · Hurwitz criterion for block lower-triangular matrices · R₀ as a threshold for the linearized infected subsystem

TheoremThreshold theorem, instability half, spectral form#✓fully proved

Threshold theorem, instability half, spectral form (van den Driessche–Watmough 2002, Theorem 2). With F ≥ 0 and V a nonsingular M-matrix, if R₀ = ρ(F V⁻¹) > 1 then the Jacobian [[F - V, 0], [C, D]] at the disease-free equilibrium has an eigenvalue with positive real part (whatever C and D).

theorem exists_re_pos_jacobian_of_one_lt_R0 {F V : Matrix ι ι ℝ} (C : Matrix κ ι ℝ)
    (D : Matrix κ κ ℝ) (hF : ∀ i j, 0 ≤ F i j) (hV : V.IsNonsingularMMatrix)
    (hR0 : 1 < R0 F V) :
    ∃ μ ∈ spectrum ℂ ((fromBlocks (F - V) 0 C D).map (algebraMap ℝ ℂ)), 0 < μ.re

Uses 4

Statement usesBasic reproduction number of the next-generation matrix · Nonsingular M-matrix

Proof usesR₀ > 1 gives an unstable mode · Eigenvalues of a block lower-triangular matrix

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.