Laws of generation sizes

The root-conditioned child generation sizes are independent copies of the corresponding generation size. Root decomposition gives the iterated offspring generating function and the extended first moment. These marginal statements do not assert the Markov property conditional on the entire generation history. All offspring probability measures are allowed.

theorem BGW.LocallyFinite.measurable_generationSize (n : ℕ) : Measurable fun (T : Tree) => generationSize T n

theorem BGW.LocallyFinite.cond_map_children_generationSize (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n k : ℕ) (hk : μ {k} ≠ 0) : MeasureTheory.Measure.map (fun (T : Tree) (i : Fin k) => generationSize (child T (↑i + 1)) n) (bienaymeLaw μ)[|{T : Tree | degree T = k}] = MeasureTheory.Measure.pi fun (x : Fin k) => MeasureTheory.Measure.map (fun (T : Tree) => generationSize T n) (bienaymeLaw μ)

Given the root degree k of positive probability, child generation sizes are iid.

theorem BGW.LocallyFinite.lintegral_children_of_degree (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) {g : (Fin k → Tree) → ENNReal} (hg : Measurable g) : ∫⁻ (T : Tree) in {T : Tree | degree T = k}, g fun (i : Fin k) => child T (↑i + 1) ∂bienaymeLaw μ = μ {k} * ∫⁻ (ts : Fin k → Tree), g ts ∂MeasureTheory.Measure.pi fun (x : Fin k) => bienaymeLaw μ

Integral form of root branching, also valid when the root-degree event is null.

theorem BGW.LocallyFinite.lintegral_pow_generationSize_succ (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (s : ENNReal) : ∫⁻ (T : Tree), s ^ generationSize T (n + 1) ∂bienaymeLaw μ = offspringGF μ (∫⁻ (T : Tree), s ^ generationSize T n ∂bienaymeLaw μ)

Root branching gives one composition by the offspring generating function.

theorem BGW.LocallyFinite.lintegral_pow_generationSize (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (s : ENNReal) : ∫⁻ (T : Tree), s ^ generationSize T n ∂bienaymeLaw μ = (offspringGF μ)^[n] s

The generating function of the nth generation is the nfold iterate of the offspring generating function. This holds throughout ℝ≥0∞, including s = 0 and s = ∞.

theorem BGW.LocallyFinite.lintegral_generationSize_succ (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : ∫⁻ (T : Tree), ↑(generationSize T (n + 1)) ∂bienaymeLaw μ = (∫⁻ (k : ℕ), ↑k ∂μ) * ∫⁻ (T : Tree), ↑(generationSize T n) ∂bienaymeLaw μ

The expected next-generation size is the offspring mean times the current expectation, with extended nonnegative expectations and no moment assumption.

theorem BGW.LocallyFinite.lintegral_generationSize (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : ∫⁻ (T : Tree), ↑(generationSize T n) ∂bienaymeLaw μ = (∫⁻ (k : ℕ), ↑k ∂μ) ^ n

The nth generation has mean m ^ n, where m is the possibly infinite offspring mean.