Linear birth–death process

DefinitionKendall's extinction probability for the birth–death process#✓fully proved

Kendall's extinction probability α t = P(X t = 0 | X 0 = 1) of the linear birth–death process with per-capita birth rate b and death rate d: d (E - 1) / (b E - d) with E = exp ((b - d) t) if b ≠ d, and b t / (1 + b t) if b = d. Meaningful for 0 ≤ b, 0 ≤ d, 0 ≤ t.

noncomputable def extinctionProb (b d t : ℝ) : ℝ :=
  if b = d then b * t / (1 + b * t)
  else d * (exp ((b - d) * t) - 1) / (b * exp ((b - d) * t) - d)

Used by 11

Used byUniqueness of the extinction probability solving the backward equation · Backward Kolmogorov equation for the extinction probability · Forward Kolmogorov equation for positive states · Forward Kolmogorov equation for the empty state · Mean population size of the linear birth–death process · Kendall's probabilities sum to one · Kendall's law of the linear birth–death process · Nonnegativity of Kendall's probabilities · Linear birth–death law at time zero · Certain extinction in the critical and subcritical cases · Limiting extinction probability in the supercritical case

DefinitionKendall's geometric tail ratio#✓fully proved

Kendall's ratio β t of the geometric tail of the law of X t: b (E - 1) / (b E - d) with E = exp ((b - d) t) if b ≠ d, and b t / (1 + b t) if b = d.

noncomputable def geomRatio (b d t : ℝ) : ℝ :=
  if b = d then b * t / (1 + b * t)
  else b * (exp ((b - d) * t) - 1) / (b * exp ((b - d) * t) - d)

Used by 8

Used byBackward Kolmogorov equation for the extinction probability · Forward Kolmogorov equation for positive states · Forward Kolmogorov equation for the empty state · Mean population size of the linear birth–death process · Kendall's probabilities sum to one · Kendall's law of the linear birth–death process · Nonnegativity of Kendall's probabilities · Linear birth–death law at time zero

DefinitionKendall's law of the linear birth–death process#✓fully proved

Kendall's law of the linear birth–death process at time t started from one individual: prob b d t 0 = α t and prob b d t (n + 1) = (1 - α t) (1 - β t) (β t) ^ n.

noncomputable def prob (b d t : ℝ) : ℕ → ℝ
  | 0 => extinctionProb b d t
  | n + 1 => (1 - extinctionProb b d t) * (1 - geomRatio b d t) * geomRatio b d t ^ n

Uses 2 · Used by 6

Statement usesKendall's extinction probability for the birth–death process · Kendall's geometric tail ratio

Used byForward Kolmogorov equation for positive states · Forward Kolmogorov equation for the empty state · Mean population size of the linear birth–death process · Kendall's probabilities sum to one · Nonnegativity of Kendall's probabilities · Linear birth–death law at time zero

TheoremLinear birth–death law at time zero#✓fully proved

At time 0 the population is one individual: prob b d 0 = δ₁.

theorem prob_zero_time (b d : ℝ) (n : ℕ) : prob b d 0 n = if n = 1 then 1 else 0

Uses 3

Statement usesKendall's law of the linear birth–death process

Proof usesKendall's extinction probability for the birth–death process · Kendall's geometric tail ratio

TheoremNonnegativity of Kendall's probabilities#✓fully proved

Kendall's probabilities are nonnegative.

theorem prob_nonneg {b d t : ℝ} (hb : 0 ≤ b) (hd : 0 ≤ d) (ht : 0 ≤ t) (n : ℕ) :
    0 ≤ prob b d t n

Uses 3

Statement usesKendall's law of the linear birth–death process

Proof usesKendall's extinction probability for the birth–death process · Kendall's geometric tail ratio

TheoremKendall's probabilities sum to one#✓fully proved

Kendall's probabilities sum to 1: no mass escapes to infinity.

theorem hasSum_prob {b d t : ℝ} (hb : 0 ≤ b) (hd : 0 ≤ d) (ht : 0 ≤ t) :
    HasSum (prob b d t) 1

Uses 3

Statement usesKendall's law of the linear birth–death process

Proof usesKendall's extinction probability for the birth–death process · Kendall's geometric tail ratio

TheoremMean population size of the linear birth–death process#✓fully proved

The mean population size at time t started from one individual is E[X t] = exp ((b - d) t) (Kendall 1948; Bailey 1964, ch. 8).

theorem hasSum_mul_prob {b d t : ℝ} (hb : 0 ≤ b) (hd : 0 ≤ d) (ht : 0 ≤ t) :
    HasSum (fun n : ℕ ↦ (n : ℝ) * prob b d t n) (exp ((b - d) * t))

Uses 3

Statement usesKendall's law of the linear birth–death process

Proof usesKendall's extinction probability for the birth–death process · Kendall's geometric tail ratio

TheoremForward Kolmogorov equation for the empty state#✓fully proved

Forward Kolmogorov equation for state 0: p_0' = d p_1.

theorem hasDerivAt_prob_zero {b d t : ℝ} (hb : 0 ≤ b) (hd : 0 ≤ d) (ht : 0 ≤ t) :
    HasDerivAt (fun s ↦ prob b d s 0) (d * prob b d t 1) t

Uses 3

Statement usesKendall's law of the linear birth–death process

Proof usesKendall's extinction probability for the birth–death process · Kendall's geometric tail ratio

TheoremForward Kolmogorov equation for positive states#✓fully proved

Forward Kolmogorov equation for state n + 1: p_(n+1)' = b n p_n - (b + d) (n + 1) p_(n+1) + d (n + 2) p_(n+2).

theorem hasDerivAt_prob_succ {b d t : ℝ} (hb : 0 ≤ b) (hd : 0 ≤ d) (ht : 0 ≤ t) (n : ℕ) :
    HasDerivAt (fun s ↦ prob b d s (n + 1))
      (b * n * prob b d t n - (b + d) * (n + 1) * prob b d t (n + 1)
        + d * (n + 2) * prob b d t (n + 2)) t

Uses 3

Statement usesKendall's law of the linear birth–death process

Proof usesKendall's extinction probability for the birth–death process · Kendall's geometric tail ratio

TheoremBackward Kolmogorov equation for the extinction probability#✓fully proved

Backward Kolmogorov equation for the extinction probability: α' = d - (b + d) α + b α² (Karlin–Taylor 1975, ch. 4).

theorem hasDerivAt_extinctionProb {b d t : ℝ} (hb : 0 ≤ b) (hd : 0 ≤ d) (ht : 0 ≤ t) :
    HasDerivAt (extinctionProb b d)
      (d - (b + d) * extinctionProb b d t + b * extinctionProb b d t ^ 2) t

Uses 2 · Used by 1

Statement usesKendall's extinction probability for the birth–death process

Proof usesKendall's geometric tail ratio

Used byUniqueness of the extinction probability solving the backward equation

TheoremUniqueness of the extinction probability solving the backward equation#✓fully proved

The extinction probability is the only [0, 1]-valued solution q on [0, ∞) of the backward equation q' = d - (b + d) q + b q² with q 0 = 0.

theorem eq_extinctionProb_of_hasDerivWithinAt {b d : ℝ} (hb : 0 ≤ b) (hd : 0 ≤ d) {q : ℝ → ℝ}
    (hc : ContinuousOn q (Ici 0))
    (hq : ∀ t, 0 ≤ t → HasDerivWithinAt q (d - (b + d) * q t + b * q t ^ 2) (Ici t) t)
    (hq01 : ∀ t, 0 ≤ t → q t ∈ Icc 0 1) (hq0 : q 0 = 0) {t : ℝ} (ht : 0 ≤ t) :
    q t = extinctionProb b d t

Uses 2

Statement usesKendall's extinction probability for the birth–death process

Proof usesBackward Kolmogorov equation for the extinction probability

TheoremLimiting extinction probability in the supercritical case#✓fully proved

Supercritical case: if d < b, the extinction probability tends to d / b.

theorem tendsto_extinctionProb_of_lt {b d : ℝ} (hd : 0 ≤ d) (hdb : d < b) :
    Tendsto (extinctionProb b d) atTop (𝓝 (d / b))

Uses 1

Statement usesKendall's extinction probability for the birth–death process

TheoremCertain extinction in the critical and subcritical cases#✓fully proved

Critical and subcritical cases: if b ≤ d and 0 < d, extinction is certain in the limit.

theorem tendsto_extinctionProb_of_le {b d : ℝ} (hd : 0 < d) (hbd : b ≤ d) :
    Tendsto (extinctionProb b d) atTop (𝓝 1)

Uses 1

Statement usesKendall's extinction probability for the birth–death process

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.