The Bienaymé–Galton–Watson law on locally finite trees

For an arbitrary probability measure μ on ℕ, offspringFieldLaw μ makes the potential offspring counts at all addresses independent with law μ, and bienaymeLaw μ is the law of the pruned tree. Nothing is assumed about the mean or support of μ; the tree may be infinite. This is the general part of Freezing1/PlaneBienaymeLaw.lean, without its geometric specialization.

The branching property, uniqueness and the law of the finite trees are in Branching.lean, Unique.lean and Atoms.lean.

noncomputable def BGW.LocallyFinite.offspringFieldLaw (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.Measure Offspring

Independent potential offspring counts, one for each address.

The probability hypothesis is not used by the formula, but it fixes the domain of the definition: Measure.infinitePi is the zero measure unless every component is a probability measure, so without it the definition would expose that default value instead of an offspring law.

Equations

• BGW.LocallyFinite.offspringFieldLaw μ = MeasureTheory.Measure.infinitePi fun (x : BGW.LocallyFinite.Address) => μ

instance BGW.LocallyFinite.offspringFieldLaw_probability (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsProbabilityMeasure (offspringFieldLaw μ)

noncomputable def BGW.LocallyFinite.bienaymeLaw (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.Measure Tree

The Bienaymé–Galton–Watson law with offspring law μ.

Equations

• BGW.LocallyFinite.bienaymeLaw μ = MeasureTheory.Measure.map BGW.LocallyFinite.prune (BGW.LocallyFinite.offspringFieldLaw μ)

instance BGW.LocallyFinite.bienaymeLaw_probability (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsProbabilityMeasure (bienaymeLaw μ)

theorem BGW.LocallyFinite.bienaymeLaw_apply (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {A : Set Tree} (hA : MeasurableSet A) : (bienaymeLaw μ) A = (offspringFieldLaw μ) (prune ⁻¹' A)

theorem BGW.LocallyFinite.measurePreserving_prune (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.MeasurePreserving prune (offspringFieldLaw μ) (bienaymeLaw μ)

theorem BGW.LocallyFinite.bienaymeLaw_map_degree (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.Measure.map degree (bienaymeLaw μ) = μ

The root degree has the offspring law.

theorem BGW.LocallyFinite.bienaymeLaw_leaf (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : (bienaymeLaw μ) {leaf} = μ {0}

The root is a leaf with probability μ {0}.