Extinction by a finite depth and the least fixed point

extinctBy n is the event that every present address has length strictly less than n: the root has depth zero, so extinctBy 0 = ∅ and extinctBy 1 = {leaf}, and extinctBy n is extinction by generation n. Under bienaymeLaw μ, for every offspring probability measure μ (no mean, nondegeneracy or support condition), the root decomposition and the branching property give P(extinctBy (n + 1)) = f (P(extinctBy n)) with f = offspringGF μ, hence P(extinctBy n) = f^[n] 0. A tree is finite exactly when it lies in some extinctBy n, so the probability q of finiteness is the supremum of these iterates, satisfies f q = q, and is the smallest fixed point of f in [0, 1]. By bienaymeLaw_finiteVertices, it is also the total weight of the finite plane trees. The fixed-point argument follows PoissonDeclumping/Bienayme/Normalization.lean (offspringGF_bienayme_univ) and the height recursion of PoissonDeclumping/Bienayme/Basic.lean, whose convention is shifted by one here. Classification by the mean, generation sizes and conditioning are not part of this module.

def BGW.LocallyFinite.extinctBy (n : ℕ) : Set Tree

Extinction by generation n: no present address of length n or more.

Equations

• BGW.LocallyFinite.extinctBy n = {T : BGW.LocallyFinite.Tree | ∀ (u : BGW.LocallyFinite.Address), BGW.LocallyFinite.Present T u → List.length u < n}

theorem BGW.LocallyFinite.extinctBy_zero : extinctBy 0 = ∅

theorem BGW.LocallyFinite.extinctBy_one : extinctBy 1 = {leaf}

theorem BGW.LocallyFinite.monotone_extinctBy : Monotone extinctBy

theorem BGW.LocallyFinite.mem_extinctBy_succ_iff (T : Tree) (n : ℕ) : T ∈ extinctBy (n + 1) ↔ ∀ (j : ℕ), 1 ≤ j → j ≤ degree T → child T j ∈ extinctBy n

theorem BGW.LocallyFinite.extinctBy_succ_eq (n : ℕ) : extinctBy (n + 1) = ⋃ (k : ℕ), childrenEvent k fun (x : Fin k) => extinctBy n

theorem BGW.LocallyFinite.measurableSet_extinctBy (n : ℕ) : MeasurableSet (extinctBy n)

Finite trees

theorem BGW.LocallyFinite.finiteVertices_child {T : Tree} (hT : FiniteVertices T) {j : ℕ} (h1 : 1 ≤ j) (h2 : j ≤ degree T) : FiniteVertices (child T j)

theorem BGW.LocallyFinite.finiteVertices_iff_children (T : Tree) : FiniteVertices T ↔ ∀ (j : ℕ), 1 ≤ j → j ≤ degree T → FiniteVertices (child T j)

A tree is finite iff all of its existing child subtrees are finite.

theorem BGW.LocallyFinite.extinctBy_subset_finiteVertices (n : ℕ) {T : Tree} (hT : T ∈ extinctBy n) : FiniteVertices T

theorem BGW.LocallyFinite.iUnion_extinctBy : ⋃ (n : ℕ), extinctBy n = {T : Tree | FiniteVertices T}

A finite tree is in extinctBy n for some n, and conversely.

theorem BGW.LocallyFinite.finiteVertices_eq_iUnion_childrenEvent : {T : Tree | FiniteVertices T} = ⋃ (k : ℕ), childrenEvent k fun (x : Fin k) => {T : Tree | FiniteVertices T}

Probabilities

theorem BGW.LocallyFinite.bienaymeLaw_iUnion_childrenEvent (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {A : Set Tree} (hA : MeasurableSet A) : (bienaymeLaw μ) (⋃ (k : ℕ), childrenEvent k fun (x : Fin k) => A) = offspringGF μ ((bienaymeLaw μ) A)

One generation of branching: the mass of "all children in A" is the generating function of the offspring law at the mass of A.

theorem BGW.LocallyFinite.bienaymeLaw_extinctBy_zero (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : (bienaymeLaw μ) (extinctBy 0) = 0

theorem BGW.LocallyFinite.bienaymeLaw_extinctBy_succ (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : (bienaymeLaw μ) (extinctBy (n + 1)) = offspringGF μ ((bienaymeLaw μ) (extinctBy n))

theorem BGW.LocallyFinite.bienaymeLaw_extinctBy (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : (bienaymeLaw μ) (extinctBy n) = (offspringGF μ)^[n] 0

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

theorem BGW.LocallyFinite.monotone_iterate_offspringGF (μ : MeasureTheory.Measure ℕ) : Monotone fun (n : ℕ) => (offspringGF μ)^[n] 0

theorem BGW.LocallyFinite.bienaymeLaw_finiteVertices_eq_iSup (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : (bienaymeLaw μ) {T : Tree | FiniteVertices T} = ⨆ (n : ℕ), (offspringGF μ)^[n] 0

The probability that the tree is finite is the supremum of the iterates of the generating function at 0.

theorem BGW.LocallyFinite.tendsto_iterate_offspringGF (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : Filter.Tendsto (fun (n : ℕ) => (offspringGF μ)^[n] 0) Filter.atTop (nhds ((bienaymeLaw μ) {T : Tree | FiniteVertices T}))

theorem BGW.LocallyFinite.offspringGF_bienaymeLaw_finiteVertices (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : offspringGF μ ((bienaymeLaw μ) {T : Tree | FiniteVertices T}) = (bienaymeLaw μ) {T : Tree | FiniteVertices T}

The probability that the tree is finite is a fixed point of the generating function.

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

Minimality: every fixed point of the generating function bounds the probability of finiteness from above. The bound s ≤ 1 is not needed.

theorem BGW.LocallyFinite.isLeast_bienaymeLaw_finiteVertices (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : IsLeast {s : ENNReal | s ≤ 1 ∧ offspringGF μ s = s} ((bienaymeLaw μ) {T : Tree | FiniteVertices T})

The probability that the tree is finite is the smallest fixed point of the offspring generating function in [0, 1].

theorem BGW.LocallyFinite.isLeast_tsum_weight (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : IsLeast {s : ENNReal | s ≤ 1 ∧ offspringGF μ s = s} (∑' (t : PlaneTree), PlaneTree.weight (fun (d : ℕ) => μ {d}) t)

The total weight of the finite plane trees is the smallest fixed point of the generating function in [0, 1].