Classification of the extinction probability by the mean

Let q = bienaymeLaw μ {T | FiniteVertices T} be the probability that the tree is finite, for an offspring probability measure μ with mean ∫⁻ k, k ∂μ in [0, ∞] (infinite mean allowed).

• q ≤ s as soon as offspringGF μ s ≤ s (a sub-fixed point bounds the iterates from above);
• if the mean exceeds one, there is s < 1 with offspringGF μ s ≤ s (exists_lt_one_offspringGF_le), hence q < 1 (bienaymeLaw_finiteVertices_lt_one);
• q = 1 exactly when the mean is at most one and μ {1} ≠ 1 (bienaymeLaw_finiteVertices_eq_one_iff): for μ {1} = 1 the tree is an infinite line and q = 0.

No source in PoissonDeclumping states the supercritical case, which the paper does not need. Convexity and derivatives are not used: the bound 1 - f x ≥ x ^ N (1 - x) M comes from the elementary inequality k x ^ N (1 - x) ≤ 1 - x ^ k for k ≤ N.

theorem BGW.LocallyFinite.bienaymeLaw_finiteVertices_le_of_offspringGF_le (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {s : ENNReal} (hs : offspringGF μ s ≤ s) : (bienaymeLaw μ) {T : Tree | FiniteVertices T} ≤ s

A sub-fixed point of the generating function bounds the probability of finiteness from above.

theorem BGW.LocallyFinite.bienaymeLaw_finiteVertices_lt_one (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (hm : 1 < ∫⁻ (k : ℕ), ↑k ∂μ) : (bienaymeLaw μ) {T : Tree | FiniteVertices T} < 1

Supercritical case. For every offspring probability measure of mean greater than one, possibly infinite, the tree is infinite with positive probability: q < 1.

theorem BGW.LocallyFinite.bienaymeLaw_finiteVertices_eq_zero_of_singleton_one (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (h1 : μ {1} = 1) : (bienaymeLaw μ) {T : Tree | FiniteVertices T} = 0

For μ {1} = 1 the tree is an infinite line: the probability of finiteness is zero.

theorem BGW.LocallyFinite.bienaymeLaw_finiteVertices_eq_one_iff (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : (bienaymeLaw μ) {T : Tree | FiniteVertices T} = 1 ↔ ∫⁻ (k : ℕ), ↑k ∂μ ≤ 1 ∧ μ {1} ≠ 1

Classification. The probability that the tree is finite is 1 exactly when the mean is at most one and μ {1} ≠ 1; otherwise it is < 1.