Superspreading and negative-binomial offspring

DefinitionNegative-binomial offspring probabilities#✓fully proved

The negative-binomial offspring probability with mean R and dispersion k: P(Z = n) = C(k + n - 1, n) p^k (1 - p)^n with p = k / (k + R) (Lloyd-Smith et al. 2005). Meaningful for k > 0, R ≥ 0.

noncomputable def nbPmf (R k : ℝ) (n : ℕ) : ℝ :=
  Ring.choose (k + n - 1) n * (k / (k + R)) ^ k * (R / (k + R)) ^ n

Used by 5

Used byGenerating-function identity · Negative-binomial offspring law is a probability measure · Negative-binomial offspring distribution · Nonnegativity of the negative-binomial probabilities · Generating function of the negative-binomial law in closed form

DefinitionNegative-binomial probability generating function#✓fully proved

The negative-binomial generating function G_k(s) = (1 + (R / k) (1 - s))^{-k}.

noncomputable def nbPgf (R k s : ℝ) : ℝ :=
  (1 + R / k * (1 - s)) ^ (-k)

Used by 8

Used bySuperspreading raises the extinction probability · Generating-function identity · Negative-binomial extinction probability is the least fixed point · Negative-binomial offspring law is a probability measure · Monotonicity in the dispersion · Negative-binomial law with dispersion one is geometric · Generating function of the negative-binomial law in closed form · Poisson limit

DefinitionNegative-binomial offspring distribution#✓fully proved

The negative-binomial offspring law as a measure on ℕ.

noncomputable def nbOffspring (R k : ℝ) : Measure ℕ :=
  Measure.sum fun n => ENNReal.ofReal (nbPmf R k n) • Measure.dirac n

Uses 1 · Used by 4

Statement usesNegative-binomial offspring probabilities

Used bySuperspreading raises the extinction probability · Negative-binomial extinction probability is the least fixed point · Negative-binomial offspring law is a probability measure · Generating function of the negative-binomial law in closed form

TheoremNonnegativity of the negative-binomial probabilities#✓fully proved

The negative-binomial probabilities are nonnegative for k > 0, R ≥ 0.

theorem nbPmf_nonneg {R k : ℝ} (hk : 0 < k) (hR : 0 ≤ R) (n : ℕ) : 0 ≤ nbPmf R k n

Uses 1 · Used by 2

Statement usesNegative-binomial offspring probabilities

Used byNegative-binomial offspring law is a probability measure · Generating function of the negative-binomial law in closed form

TheoremGenerating-function identity#✓fully proved

For k > 0, R ≥ 0 and s ∈ [0, 1], ∑ₙ P(Z = n) sⁿ = (1 + (R / k) (1 - s))^{-k}.

theorem hasSum_nbPmf_mul_pow {R k : ℝ} (hk : 0 < k) (hR : 0 ≤ R) {s : ℝ}
    (hs : s ∈ Icc (0 : ℝ) 1) : HasSum (fun n => nbPmf R k n * s ^ n) (nbPgf R k s)

Uses 2 · Used by 2

Statement usesNegative-binomial probability generating function · Negative-binomial offspring probabilities

Used byNegative-binomial offspring law is a probability measure · Generating function of the negative-binomial law in closed form

TheoremNegative-binomial offspring law is a probability measure#✓fully proved

The negative-binomial offspring law is a probability measure (k > 0, R ≥ 0).

theorem isProbabilityMeasure_nbOffspring {R k : ℝ} (hk : 0 < k) (hR : 0 ≤ R) :
    IsProbabilityMeasure (nbOffspring R k)

Uses 5 · Used by 3

Statement usesNegative-binomial offspring distribution

Proof usesGenerating-function identity · Negative-binomial probability generating function · Negative-binomial offspring probabilities · Nonnegativity of the negative-binomial probabilities

Used bySuperspreading raises the extinction probability · Negative-binomial extinction probability is the least fixed point · Generating function of the negative-binomial law in closed form

TheoremGenerating function of the negative-binomial law in closed form#✓fully proved

The generating function of the negative-binomial offspring law is nbPgf on [0, 1].

theorem pgf_nbOffspring {R k : ℝ} (hk : 0 < k) (hR : 0 ≤ R) {s : ℝ}
    (hs : s ∈ Icc (0 : ℝ) 1) : pgf id (nbOffspring R k) s = nbPgf R k s

Uses 7 · Used by 2

Statement usesNegative-binomial offspring distribution · Negative-binomial probability generating function · Probability generating function

Proof usesGenerating-function identity · Negative-binomial offspring law is a probability measure · Negative-binomial offspring probabilities · Nonnegativity of the negative-binomial probabilities

Used bySuperspreading raises the extinction probability · Negative-binomial extinction probability is the least fixed point

TheoremMonotonicity in the dispersion#✓fully proved

For R ≥ 0, s ∈ [0, 1] and 0 < k₁ ≤ k₂, G_{k₂}(s) ≤ G_{k₁}(s); equivalently k ↦ k log (1 + x / k) is nondecreasing for x ≥ 0.

theorem nbPgf_antitone {R : ℝ} (hR : 0 ≤ R) {s : ℝ} (hs : s ∈ Icc (0 : ℝ) 1) {k₁ k₂ : ℝ}
    (hk₁ : 0 < k₁) (hk : k₁ ≤ k₂) : nbPgf R k₂ s ≤ nbPgf R k₁ s

Uses 1 · Used by 1

Statement usesNegative-binomial probability generating function

Used bySuperspreading raises the extinction probability

TheoremNegative-binomial law with dispersion one is geometric#✓fully proved

k = 1 is the geometric offspring law: G_1(s) = 1 / (1 + R (1 - s)).

theorem nbPgf_one_dispersion (R s : ℝ) : nbPgf R 1 s = 1 / (1 + R * (1 - s))

Uses 1

Statement usesNegative-binomial probability generating function

TheoremPoisson limit#✓fully proved

As k → ∞, G_k(s) → e^{-R (1 - s)} (for all real R, s).

theorem tendsto_nbPgf_atTop (R s : ℝ) :
    Tendsto (fun k => nbPgf R k s) atTop (𝓝 (Real.exp (-(R * (1 - s)))))

Uses 1

Statement usesNegative-binomial probability generating function

TheoremComparison principle for Galton–Watson extinction#✓fully proved

If the offspring generating functions satisfy f₂ ≤ f₁ on [0, 1], then the extinction probabilities satisfy q₂ ≤ q₁.

theorem extinctionProb_le_of_pgf_le (ν₁ ν₂ : Measure ℕ) [IsProbabilityMeasure ν₁]
    [IsProbabilityMeasure ν₂] (h : ∀ s ∈ Icc (0 : ℝ) 1, pgf id ν₂ s ≤ pgf id ν₁ s) :
    extinctionProb ν₂ ≤ extinctionProb ν₁

Uses 7 · Used by 1

Statement usesExtinction probability of a Galton–Watson process · Probability generating function

Proof usesExtinction probability is the least fixed point · Iterates of the offspring generating function stay in (0, 1) · Generation-size law of a Galton–Watson process · Probability of extinction by generation n · Integrability of \(s^X\) for \(|s| \le 1\)

Used bySuperspreading raises the extinction probability

TheoremNegative-binomial extinction probability is the least fixed point#✓fully proved

The extinction probability of the negative-binomial epidemic is the least fixed point of G_k in [0, 1].

theorem isLeast_extinctionProb_nbOffspring {R k : ℝ} (hk : 0 < k) (hR : 0 ≤ R) :
    have := isProbabilityMeasure_nbOffspring hk hR
    IsLeast {s | s ∈ Icc (0 : ℝ) 1 ∧ nbPgf R k s = s} (extinctionProb (nbOffspring R k))

Uses 7

Statement usesNegative-binomial offspring law is a probability measure · Negative-binomial offspring distribution · Negative-binomial probability generating function · Extinction probability of a Galton–Watson process

Proof usesGenerating function of the negative-binomial law in closed form · Extinction probability is the least fixed point · Probability generating function

TheoremSuperspreading raises the extinction probability#✓fully proved

Superspreading raises the extinction probability (Lloyd-Smith et al. 2005): at a fixed mean R ≥ 0, the probability q_k that the outbreak started by one case goes extinct is nonincreasing in the dispersion k > 0.

theorem extinctionProb_nbOffspring_antitone {R : ℝ} (hR : 0 ≤ R) {k₁ k₂ : ℝ} (hk₁ : 0 < k₁)
    (hk : k₁ ≤ k₂) :
    have := isProbabilityMeasure_nbOffspring hk₁ hR
    have := isProbabilityMeasure_nbOffspring (hk₁.trans_le hk) hR
    extinctionProb (nbOffspring R k₂) ≤ extinctionProb (nbOffspring R k₁)

Uses 8

Statement usesNegative-binomial offspring law is a probability measure · Negative-binomial offspring distribution · Extinction probability of a Galton–Watson process

Proof usesComparison principle for Galton–Watson extinction · Negative-binomial probability generating function · Monotonicity in the dispersion · Generating function of the negative-binomial law in closed form · Probability generating function

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.