The branching property of the Bienaymé–Galton–Watson law

IsBienayme μ ρ says that the root degree has law ρ and that, conditionally on the root degree being k (when this has positive probability), the k ordered child subtrees have the joint law μ ⊗ ⋯ ⊗ μ. The statement is about the whole finite family of children, so no independence is built into the carrier. The constructed law satisfies it for every offspring probability measure ρ. Adapted from Freezing1/PlaneTreeBranching.lean (the definition IsBienayme) and Freezing1/PlaneBienaymeBranching.lean, with childrenEvent stated directly instead of through the geometric FirstChildStructure.

def BGW.LocallyFinite.childrenEvent (k : ℕ) (E : Fin k → Set Tree) : Set Tree

Exact root degree k together with a rectangle E i for the i-th child, i < k.

Equations

• BGW.LocallyFinite.childrenEvent k E = {T : BGW.LocallyFinite.Tree | BGW.LocallyFinite.degree T = k ∧ ∀ (i : Fin k), BGW.LocallyFinite.child T (↑i + 1) ∈ E i}

theorem BGW.LocallyFinite.measurableSet_childrenEvent (k : ℕ) (E : Fin k → Set Tree) (hE : ∀ (i : Fin k), MeasurableSet (E i)) : MeasurableSet (childrenEvent k E)

def BGW.LocallyFinite.IsBienayme (μ : MeasureTheory.Measure Tree) (offspringLaw : MeasureTheory.Measure ℕ) : Prop

The branching characterization of a Bienaymé–Galton–Watson law with offspring law offspringLaw: the root has the offspring law and, conditionally on its count k, the children are k independent copies of the law itself. It is meant for probability measures; the guard μ {degree = k} ≠ 0 is needed because conditioning on a null event gives the zero measure.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.LocallyFinite.raw_childrenEvent_measure (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) (E : Fin k → Set Tree) (hE : ∀ (i : Fin k), MeasurableSet (E i)) : (offspringFieldLaw μ) {f : Offspring | f [] = k ∧ ∀ (i : Fin k), (prune fun (u : Address) => f ((↑i + 1) :: u)) ∈ E i} = μ {k} * ∏ i : Fin k, (bienaymeLaw μ) (E i)

theorem BGW.LocallyFinite.bienaymeLaw_childrenEvent (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) (E : Fin k → Set Tree) (hE : ∀ (i : Fin k), MeasurableSet (E i)) : (bienaymeLaw μ) (childrenEvent k E) = μ {k} * ∏ i : Fin k, (bienaymeLaw μ) (E i)

theorem BGW.LocallyFinite.isBienayme_bienaymeLaw (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] : IsBienayme (bienaymeLaw μ) μ

For every offspring probability measure, the constructed law has the branching property.