The offspring generating function in [0, ∞] #
For an offspring law μ on ℕ, offspringGF μ s = ∑ k, μ {k} * s ^ k in ℝ≥0∞, with
0 ^ 0 = 1. Only elementary facts are proved: the values at 0 and 1, monotonicity, and the
uniqueness of the fixed point 1 in [0, 1] for a law of mean at most one with μ {1} ≠ 1
(eq_one_of_offspringGF_eq), and, for a law of mean greater than one (infinite mean allowed), a
point s < 1 with f s ≤ s (exists_lt_one_offspringGF_le). The extinction results use
monotonicity; the normalization results use the uniqueness; the supercritical classification uses
the point below one. Adapted from PoissonDeclumping/Bienayme/Normalization.lean, where the
generating function is defined on a probability mass function.
The generating function s ↦ ∑ k, μ {k} * s ^ k of an offspring law, with values in ℝ≥0∞.
Instances For
f 0 = μ {0}.
The point masses of a probability measure on ℕ sum to one.
f 1 = 1 for a probability measure.
The generating function is monotone on [0, ∞]; no hypothesis on μ is needed.
The fixed point 1 is unique for mean at most one #
For an offspring law of mean at most one with μ {1} ≠ 1, the only fixed point of the
generating function in [0, 1] is 1.
A point below one for mean greater than one #
For an offspring law of mean greater than one, possibly infinite, there is s < 1 with
f s ≤ s. The mean is truncated to a finite part M > 1; with x ^ N = M⁻¹ one has
1 - f x ≥ ∑_{k < N} μ {k} (1 - x ^ k) ≥ x ^ N (1 - x) M = 1 - x.