Galton–Watson process

DefinitionGeneration-size law of a Galton–Watson process#✓fully proved

The law of the generation size Z_n of the Galton–Watson process with offspring law ν started from one individual: Z_0 = 1 and, given Z_n = z, Z_{n+1} has law ν^{∗z} (Measure.convPow ν z).

noncomputable def law : ℕ → Measure ℕ
  | 0 => Measure.dirac 1
  | n + 1 => (law n).bind (Measure.convPow ν)

Uses 1 · Used by 11

Statement usesConvolution power of a measure

Used byComparison principle for Galton–Watson extinction · Extinction probability of a Galton–Watson process · Galton–Watson extinction criterion · Extinction probability is the least fixed point · Probability of extinction by generation n · Mean generation size of a Galton–Watson process · Extinction by generation n is nondecreasing in n · Generating function of the n-th generation size · Extinction by generation n converges to the extinction probability · Mean total progeny of a Galton–Watson process · Mean total progeny equals \(1/(1-m)\)

DefinitionMean offspring number#✓fully proved

The mean offspring number m = E ξ = ∑ k ν{k} ∈ [0, ∞].

noncomputable def mean : ℝ≥0∞ :=
  ∫⁻ k, (k : ℝ≥0∞) ∂ν

Used by 6

Used byMean of the Poisson distribution · Beneficial mutant survives with positive probability · Galton–Watson extinction criterion · Least fixed point equals one iff mean offspring is at most one · Mean generation size of a Galton–Watson process · Mean total progeny equals \(1/(1-m)\)

DefinitionExtinction probability of a Galton–Watson process#✓fully proved

The extinction probability q = sup_n P(Z_n = 0), the limit of the probabilities of extinction by generation n (tendsto_law_real_zero). On a path space carrying the process the events {Z_n = 0} increase with n (0 is absorbing), so q is the probability of eventual extinction; this file describes the process through its generation laws and does not construct the path space.

noncomputable def extinctionProb : ℝ :=
  ⨆ n, (law ν n).real {0}

Uses 1 · Used by 11

Statement usesGeneration-size law of a Galton–Watson process

Used byComparison principle for Galton–Watson extinction · Superspreading raises the extinction probability · Negative-binomial extinction probability is the least fixed point · Haldane's equation for the survival probability · Haldane's survival probability of a mutant · Survival probability is less than one · Nonnegativity of the survival probability · Beneficial mutant survives with positive probability · Galton–Watson extinction criterion · Extinction probability is the least fixed point · Extinction by generation n converges to the extinction probability

14 fully proved

Iterates of the generating function

TheoremIterates of the offspring generating function stay in (0, 1)#✓fully proved

The iterates f^[n](s) of the offspring generating function stay in [0, 1] for s ∈ [0, 1].

theorem iterate_pgf_mem_Icc [IsProbabilityMeasure ν] (n : ℕ) {s : ℝ}
    (hs : s ∈ Icc (0 : ℝ) 1) : (pgf id ν)^[n] s ∈ Icc (0 : ℝ) 1

Uses 2 · Used by 5

Statement usesProbability generating function

Proof usesIntegrability of \(s^X\) for \(|s| \le 1\)

Used byComparison principle for Galton–Watson extinction · Least fixed point equals one iff mean offspring is at most one · Limit of generating-function iterates is the least fixed point · Iterates of the generating function at zero are nondecreasing · Generating function of the n-th generation size

TheoremIterates of the generating function at zero are nondecreasing#✓fully proved

The iterates f^[n](0) of the offspring generating function are non-decreasing.

theorem monotone_iterate_pgf_zero [IsProbabilityMeasure ν] :
    Monotone fun n => (pgf id ν)^[n] 0

Uses 3 · Used by 2

Statement usesProbability generating function

Proof usesIterates of the offspring generating function stay in (0, 1) · Integrability of \(s^X\) for \(|s| \le 1\)

Used byLimit of generating-function iterates is the least fixed point · Extinction by generation n is nondecreasing in n

TheoremLimit of generating-function iterates is the least fixed point#✓fully proved

sup_n f^[n](0) is the least fixed point of f in [0, 1] (Athreya–Ney 1972, ch. I).

theorem isLeast_iSup_iterate_pgf_zero [IsProbabilityMeasure ν] :
    IsLeast {s | s ∈ Icc (0 : ℝ) 1 ∧ pgf id ν s = s} (⨆ n, (pgf id ν)^[n] 0)

Uses 4 · Used by 2

Statement usesProbability generating function

Proof usesIterates of the offspring generating function stay in (0, 1) · Iterates of the generating function at zero are nondecreasing · Integrability of \(s^X\) for \(|s| \le 1\)

Used byLeast fixed point equals one iff mean offspring is at most one · Extinction probability is the least fixed point

TheoremLeast fixed point equals one iff mean offspring is at most one#✓fully proved

The least fixed point is 1 iff the mean offspring number is at most 1, provided the offspring number is not almost surely 1 (Athreya–Ney 1972, ch. I).

theorem iSup_iterate_pgf_zero_eq_one_iff [IsProbabilityMeasure ν]
    (h1 : ν {1} ≠ 1) :
    (⨆ n, (pgf id ν)^[n] 0) = 1 ↔ mean ν ≤ 1

Uses 5 · Used by 1

Statement usesMean offspring number · Probability generating function

Proof usesLimit of generating-function iterates is the least fixed point · Iterates of the offspring generating function stay in (0, 1) · Integrability of \(s^X\) for \(|s| \le 1\)

Used byGalton–Watson extinction criterion

Generation sizes

TheoremGenerating function of the n-th generation size#✓fully proved

The generating function of Z_n is the n-th iterate of the offspring generating function on [0, 1] (Athreya–Ney 1972, ch. I).

theorem pgf_law [IsProbabilityMeasure ν] (n : ℕ) {s : ℝ} (hs : s ∈ Icc (0 : ℝ) 1) :
    pgf id (law ν n) s = (pgf id ν)^[n] s

Uses 7 · Used by 1

Statement usesGeneration-size law of a Galton–Watson process · Probability generating function

Proof usesIterates of the offspring generating function stay in (0, 1) · Integrability of \(s^X\) for \(|s| \le 1\) · Convolution power of a measure · Recursion for convolution powers · Convolution powers of a probability measure are probability measures

Used byProbability of extinction by generation n

TheoremProbability of extinction by generation n#✓fully proved

P(Z_n = 0) = f^[n](0).

theorem law_real_zero [IsProbabilityMeasure ν] (n : ℕ) :
    (law ν n).real {0} = (pgf id ν)^[n] 0

Uses 4 · Used by 4

Statement usesGeneration-size law of a Galton–Watson process · Probability generating function

Proof usesGenerating function of the n-th generation size · The generating function at \(s = 0\)

Used byComparison principle for Galton–Watson extinction · Galton–Watson extinction criterion · Extinction probability is the least fixed point · Extinction by generation n is nondecreasing in n

TheoremMean generation size of a Galton–Watson process#✓fully proved

The mean generation size is E Z_n = m ^ n (Athreya–Ney 1972, ch. I).

theorem lintegral_law [IsProbabilityMeasure ν] (n : ℕ) :
    ∫⁻ k, (k : ℝ≥0∞) ∂(law ν n) = mean ν ^ n

Uses 5 · Used by 1

Statement usesGeneration-size law of a Galton–Watson process · Mean offspring number

Proof usesConvolution power of a measure · Recursion for convolution powers · Convolution powers of a probability measure are probability measures

Used byMean total progeny equals \(1/(1-m)\)

Extinction

TheoremExtinction by generation n is nondecreasing in n#✓fully proved

P(Z_n = 0) is non-decreasing in n.

theorem monotone_law_real_zero [IsProbabilityMeasure ν] :
    Monotone fun n => (law ν n).real {0}

Uses 4 · Used by 1

Statement usesGeneration-size law of a Galton–Watson process

Proof usesProbability of extinction by generation n · Iterates of the generating function at zero are nondecreasing · Probability generating function

Used byExtinction by generation n converges to the extinction probability

TheoremExtinction by generation n converges to the extinction probability#✓fully proved

P(Z_n = 0) converges to the extinction probability.

theorem tendsto_law_real_zero [IsProbabilityMeasure ν] :
    Tendsto (fun n => (law ν n).real {0}) atTop (𝓝 (extinctionProb ν))

Uses 5

Statement usesExtinction probability of a Galton–Watson process · Generation-size law of a Galton–Watson process

Proof usesExtinction by generation n is nondecreasing in n · Convolution power of a measure · Convolution powers of a probability measure are probability measures

TheoremExtinction probability is the least fixed point#✓fully proved

The extinction probability is the least fixed point of the offspring generating function in [0, 1] (Athreya–Ney 1972, ch. I).

theorem isLeast_extinctionProb [IsProbabilityMeasure ν] :
    IsLeast {s | s ∈ Icc (0 : ℝ) 1 ∧ pgf id ν s = s} (extinctionProb ν)

Uses 5 · Used by 6

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

Proof usesLimit of generating-function iterates is the least fixed point · Generation-size law of a Galton–Watson process · Probability of extinction by generation n

Used byComparison principle for Galton–Watson extinction · Negative-binomial extinction probability is the least fixed point · Haldane's equation for the survival probability · Survival probability is less than one · Nonnegativity of the survival probability · Beneficial mutant survives with positive probability

TheoremGalton–Watson extinction criterion#✓fully proved

Extinction is certain iff the mean offspring number is at most 1, provided the offspring number is not almost surely 1 (Athreya–Ney 1972, ch. I).

theorem extinctionProb_eq_one_iff [IsProbabilityMeasure ν] (h1 : ν {1} ≠ 1) :
    extinctionProb ν = 1 ↔ mean ν ≤ 1

Uses 6 · Used by 1

Statement usesExtinction probability of a Galton–Watson process · Mean offspring number

Proof usesLeast fixed point equals one iff mean offspring is at most one · Generation-size law of a Galton–Watson process · Probability of extinction by generation n · Probability generating function

Used byBeneficial mutant survives with positive probability

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.