Conditioning the Bienaymé–Galton–Watson law on the number of vertices

sizeEvent n is the event that the tree is finite and has exactly n present addresses. It is measurable, empty for n = 0, and equals the image of the finite plane trees of size n under the bridge. For every offspring probability measure μ (no criticality, no aperiodicity), its mass is the total weight of the plane trees of size n; the size is admissible when this mass is positive, which holds iff some tree of size n has positive weight. At an admissible size the conditioned law is a probability measure with atoms weight t / P(size = n); at an inadmissible size it is the zero measure, not a probability law. Through the Łukasiewicz coding, the mass is also the total walk weight of the tree excursions of length n, and n times it is the total walk weight of the bridge words of length n (Kemperman–Dwass in weight form, from the cycle lemma). Adapted from PoissonDeclumping/Bienayme/Conditioned.lean with the constructed law in place of the source's finite-tree measure. The set of admissible sizes and limits along it are not treated here.

theorem BGW.LocallyFinite.present_toLocallyFinite_eq (t : PlaneTree) : {u : Address | Present t.toLocallyFinite u} = PlaneTree.positiveAddress '' {u : List ℕ | t.IsVertex u}

The present addresses of a finite tree's image are the positive addresses of its vertices.

theorem BGW.LocallyFinite.ncard_present_toLocallyFinite (t : PlaneTree) : {u : Address | Present t.toLocallyFinite u}.ncard = t.size

The number of present addresses of a finite tree is its size.

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

The tree is finite and has exactly n present addresses (vertices, leaves included). The finiteness conjunct is needed at n = 0: Set.ncard of an infinite set is 0.

Equations

• BGW.LocallyFinite.sizeEvent n = {T : BGW.LocallyFinite.Tree | BGW.LocallyFinite.FiniteVertices T ∧ {u : BGW.LocallyFinite.Address | BGW.LocallyFinite.Present T u}.ncard = n}

theorem BGW.LocallyFinite.toLocallyFinite_mem_sizeEvent_iff (t : PlaneTree) (n : ℕ) : t.toLocallyFinite ∈ sizeEvent n ↔ t.size = n

theorem BGW.LocallyFinite.sizeEvent_eq_image (n : ℕ) : sizeEvent n = PlaneTree.toLocallyFinite '' {t : PlaneTree | t.size = n}

theorem BGW.LocallyFinite.measurableSet_sizeEvent (n : ℕ) : MeasurableSet (sizeEvent n)

theorem BGW.LocallyFinite.sizeEvent_zero : sizeEvent 0 = ∅

A tree has at least one vertex.

theorem BGW.LocallyFinite.bienaymeLaw_sizeEvent (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : (bienaymeLaw μ) (sizeEvent n) = ∑' (t : PlaneTree), if t.size = n then PlaneTree.weight (fun (d : ℕ) => μ {d}) t else 0

The mass of the size event is the total weight of the plane trees of that size.

theorem BGW.LocallyFinite.bienaymeLaw_sizeEvent_ne_zero_iff (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : (bienaymeLaw μ) (sizeEvent n) ≠ 0 ↔ ∃ (t : PlaneTree), t.size = n ∧ PlaneTree.weight (fun (d : ℕ) => μ {d}) t ≠ 0

A size is admissible iff some tree of that size has positive weight.

theorem BGW.LocallyFinite.bienaymeLaw_sizeEvent_eq_tsum_excursions (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : (bienaymeLaw μ) (sizeEvent n) = ∑' (x : List ℤ), {x : List ℤ | IsTreeExcursion x ∧ x.length = n}.indicator (walkWeight fun (d : ℕ) => μ {d}) x

The mass of the size event is the total walk weight of the tree excursions of length n.

theorem BGW.LocallyFinite.natCast_mul_bienaymeLaw_sizeEvent (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : ↑n * (bienaymeLaw μ) (sizeEvent n) = ∑' (x : List ℤ), (bridgeWords n).indicator (walkWeight fun (d : ℕ) => μ {d}) x

Kemperman–Dwass identity in weight form: n * P(size = n) is the total walk weight of the bridge words of length n, with no hypothesis on μ beyond being a probability measure.

theorem BGW.LocallyFinite.bienaymeLaw_sizeEvent_ne_zero_iff_excursion (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : (bienaymeLaw μ) (sizeEvent n) ≠ 0 ↔ ∃ (x : List ℤ), IsTreeExcursion x ∧ x.length = n ∧ walkWeight (fun (d : ℕ) => μ {d}) x ≠ 0

A size is admissible iff some tree excursion of that length has positive walk weight.

theorem BGW.LocallyFinite.isProbabilityMeasure_cond_sizeEvent (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (h : (bienaymeLaw μ) (sizeEvent n) ≠ 0) : MeasureTheory.IsProbabilityMeasure (bienaymeLaw μ)[|sizeEvent n]

At an admissible size, conditioning on the size gives a probability measure.

theorem BGW.LocallyFinite.cond_sizeEvent_self (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (h : (bienaymeLaw μ) (sizeEvent n) ≠ 0) : (bienaymeLaw μ)[sizeEvent n | sizeEvent n] = 1

At an admissible size, the conditioned law gives mass one to the size event.

theorem BGW.LocallyFinite.cond_sizeEvent_eq_zero (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (h : (bienaymeLaw μ) (sizeEvent n) = 0) : (bienaymeLaw μ)[|sizeEvent n] = 0

At an inadmissible size, the conditioned measure is zero, not a probability law.

theorem BGW.LocallyFinite.cond_sizeEvent_singleton (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (t : PlaneTree) : (bienaymeLaw μ)[{t.toLocallyFinite} | sizeEvent n] = if t.size = n then PlaneTree.weight (fun (d : ℕ) => μ {d}) t / (bienaymeLaw μ) (sizeEvent n) else 0

The atom of a finite tree in the conditioned law: its weight divided by the mass of the size class when it has the right size, and zero otherwise.