Normalization for offspring laws of mean at most one

If the offspring law μ has mean ∫⁻ k, k ∂μ ≤ 1 and μ {1} ≠ 1, then 1 is the only fixed point of the generating function in [0, 1] (eq_one_of_offspringGF_eq). Since the probability of finiteness is such a fixed point (isLeast_bienaymeLaw_finiteVertices), it equals one: the tree is almost surely finite, and the weights of the finite plane trees sum to one. The hypothesis μ {1} ≠ 1 is necessary: for μ = dirac 1 the mean is one, f s = s for all s, and the probability of finiteness is zero. The mean is the expectation ∫⁻ k, k ∂μ in [0, ∞]; laws of infinite mean and the supercritical classification are not treated here. Adapted from PoissonDeclumping/Bienayme/Normalization.lean, where the mean is exactly one.

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

For mean at most one and μ {1} ≠ 1, the tree is finite with probability one.

theorem BGW.LocallyFinite.tsum_weight_eq_one (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (hm : ∫⁻ (k : ℕ), ↑k ∂μ ≤ 1) (hne : μ {1} ≠ 1) : ∑' (t : PlaneTree), PlaneTree.weight (fun (d : ℕ) => μ {d}) t = 1

For mean at most one and μ {1} ≠ 1, the weights of the finite plane trees sum to one.

theorem BGW.LocallyFinite.ae_finiteVertices_bienaymeLaw (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (hm : ∫⁻ (k : ℕ), ↑k ∂μ ≤ 1) (hne : μ {1} ≠ 1) : ∀ᵐ (T : Tree) ∂bienaymeLaw μ, FiniteVertices T

For mean at most one and μ {1} ≠ 1, almost every tree has finitely many vertices.