Finite trees under the Bienaymé–Galton–Watson law

Through the bridge PlaneTree.toLocallyFinite, the law of a finite tree t is the product, over all vertices of t, of the offspring probability of its outdegree (bienaymeLaw_toLocallyFinite). No criticality or finiteness assumption is made. The finite trees form a measurable set of probability at most one: its mass is the total weight of finite plane trees, which is the probability that the tree is finite. Equality with one is not claimed here.

PlaneTree carries no MeasurableSpace instance. It is countable, so the measurability that the transport needs is that of singletons and of the finite part in Tree, and the law of the finite part is expressed as a sum of weighted Dirac masses at the images of finite trees. With the discrete σ-algebra written explicitly, toLocallyFinite is a measurable embedding (measurableEmbedding_toLocallyFinite).

theorem BGW.LocallyFinite.bienaymeLaw_toLocallyFinite (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (t : PlaneTree) : (bienaymeLaw μ) {t.toLocallyFinite} = PlaneTree.weight (fun (d : ℕ) => μ {d}) t

The atom of a finite tree: the product of the offspring masses of all its outdegrees.

theorem BGW.LocallyFinite.range_toLocallyFinite : Set.range PlaneTree.toLocallyFinite = {T : Tree | FiniteVertices T}

theorem BGW.LocallyFinite.measurableSet_finiteVertices : MeasurableSet {T : Tree | FiniteVertices T}

theorem BGW.LocallyFinite.measurableEmbedding_toLocallyFinite : MeasurableEmbedding PlaneTree.toLocallyFinite

With the discrete σ-algebra on the countable type PlaneTree (not installed as an instance), the bridge is a measurable embedding into Tree.

theorem BGW.LocallyFinite.pairwise_disjoint_singleton_toLocallyFinite : Pairwise (Function.onFun Disjoint fun (t : PlaneTree) => {t.toLocallyFinite})

theorem BGW.LocallyFinite.bienaymeLaw_finiteVertices (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : (bienaymeLaw μ) {T : Tree | FiniteVertices T} = ∑' (t : PlaneTree), PlaneTree.weight (fun (d : ℕ) => μ {d}) t

The probability that the tree is finite is the total weight of finite plane trees.

theorem BGW.LocallyFinite.tsum_weight_le_one (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : ∑' (t : PlaneTree), PlaneTree.weight (fun (d : ℕ) => μ {d}) t ≤ 1

The total weight of finite plane trees is at most one, for every offspring law.

theorem BGW.LocallyFinite.bienaymeLaw_restrict_finiteVertices (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : (bienaymeLaw μ).restrict {T : Tree | FiniteVertices T} = MeasureTheory.Measure.sum fun (t : PlaneTree) => PlaneTree.weight (fun (d : ℕ) => μ {d}) t • MeasureTheory.Measure.dirac t.toLocallyFinite

On finite trees, the law is the sum of the weighted Dirac masses at their images.