Uniqueness of the branching law

The branching property determines every finite offspring cylinder, by induction on the largest address depth, conditioning on the root count and keeping the zero constraints at absent addresses. These cylinders generate the Borel σ-algebra of Tree. Hence a probability measure with the branching property for ρ is bienaymeLaw ρ. Adapted from Freezing1/PlaneBienaymeUniqueness.lean and exists_unique_bienaymeLaw of Freezing1/PlaneGeometricBienayme.lean.

theorem BGW.LocallyFinite.IsBienayme.degree_mass {μ : MeasureTheory.Measure Tree} {ρ : MeasureTheory.Measure ℕ} (h : IsBienayme μ ρ) (k : ℕ) : μ {T : Tree | degree T = k} = ρ {k}

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

theorem BGW.LocallyFinite.IsBienayme.offspringCylinder_eq {μ ν : MeasureTheory.Measure Tree} {ρ : MeasureTheory.Measure ℕ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : IsBienayme μ ρ) (hν : IsBienayme ν ρ) (n : ℕ) (F : Finset Address) (E : Address → Set ℕ) (hF : ∀ u ∈ F, List.length u ≤ n) : μ (offspringCylinder F E) = ν (offspringCylinder F E)

theorem BGW.LocallyFinite.IsBienayme.unique {μ ν : MeasureTheory.Measure Tree} {ρ : MeasureTheory.Measure ℕ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : IsBienayme μ ρ) (hν : IsBienayme ν ρ) : μ = ν

The branching characterization uniquely determines a probability law on the actual Borel space of locally finite plane trees.

theorem BGW.LocallyFinite.IsBienayme.eq_bienaymeLaw {μ : MeasureTheory.Measure Tree} [MeasureTheory.IsProbabilityMeasure μ] {ρ : MeasureTheory.Measure ℕ} [MeasureTheory.IsProbabilityMeasure ρ] (h : IsBienayme μ ρ) : μ = bienaymeLaw ρ

A probability measure with the branching property for ρ is the constructed law.

theorem BGW.LocallyFinite.exists_unique_bienaymeLaw (ρ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure ρ] : IsBienayme (bienaymeLaw ρ) ρ ∧ ∀ (μ : MeasureTheory.Measure Tree), MeasureTheory.IsProbabilityMeasure μ → IsBienayme μ ρ → μ = bienaymeLaw ρ

For every offspring probability measure ρ, the constructed law has the branching property and is the only probability measure on Tree that has it.