Normalization of the critical Bienaymé law

Source lines 694–699 (and B13 of the inventory): for a critical offspring law μ with μ_1 ≠ 1 (the paper's standing nondegeneracy assumption), the weights ∏_{u∈T} μ_{k_u(T)} of the finite plane trees sum to one, so bienayme μ is a probability measure (PlaneTree.bienayme_isProbabilityMeasure). Equivalently, the critical nondegenerate Bienaymé tree is almost surely finite (extinction).

Route: the total weight q = 𝐏_μ(univ) satisfies q ≤ 1 for every μ (PlaneTree.bienayme_univ_le_one, by truncation in height) and, by the branching property, q = f_μ(q) for the generating function f_μ(s) = ∑ μ_k s^k. For critical μ with μ_1 ≠ 1, Bernoulli's inequality s^k ≥ 1 + k (s - 1), strict for k ≥ 2 and s < 1, and ∑ k μ_k = 1 show that 1 is the only fixed point of f_μ in [0, 1]. Along the way: μ_0 ≠ 0 and μ_j ≠ 0 for some j ≥ 2.

noncomputable def PoissonDeclumping.offspringGF (μ : PMF ℕ) (s : ENNReal) : ENNReal

The generating function f_μ(s) = ∑_k μ_k s^k of an offspring law, on [0, ∞].

Equations

• PoissonDeclumping.offspringGF μ s = ∑' (k : ℕ), μ k * s ^ k

theorem PoissonDeclumping.offspringGF_zero (μ : PMF ℕ) : offspringGF μ 0 = μ 0

theorem PoissonDeclumping.offspringGF_one (μ : PMF ℕ) : offspringGF μ 1 = 1

theorem PoissonDeclumping.offspringGF_le_one (μ : PMF ℕ) {s : ENNReal} (hs : s ≤ 1) : offspringGF μ s ≤ 1

theorem PoissonDeclumping.IsCritical.exists_two_le_ne_zero {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : ∃ (j : ℕ), 2 ≤ j ∧ μ j ≠ 0

A critical law with μ_1 ≠ 1 puts mass on some j ≥ 2.

theorem PoissonDeclumping.IsCritical.eq_one_of_offspringGF_eq {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {s : ENNReal} (hs : s ≤ 1) (hfix : offspringGF μ s = s) : s = 1

For critical μ with μ_1 ≠ 1, the only fixed point of f_μ in [0, 1] is 1 (convexity of the generating function, f_μ(1) = 1, f_μ'(1) = 1).

theorem PoissonDeclumping.IsCritical.apply_zero_ne_zero {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : μ 0 ≠ 0

A critical law with μ_1 ≠ 1 gives positive mass to 0.

theorem PoissonDeclumping.PlaneTree.offspringGF_bienayme_univ (μ : PMF ℕ) : offspringGF μ ((bienayme μ) Set.univ) = (bienayme μ) Set.univ

The total weight q = 𝐏_μ(T finite) is a fixed point of the generating function.

theorem PoissonDeclumping.PlaneTree.bienayme_univ {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : (bienayme μ) Set.univ = 1

Normalization (source lines 694–699, "implicitly μ_1 ≠ 1"): for a critical offspring law with μ_1 ≠ 1, the Bienaymé weights of the finite plane trees sum to one, i.e. the critical Bienaymé tree is almost surely finite.

theorem PoissonDeclumping.PlaneTree.bienayme_isProbabilityMeasure {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : MeasureTheory.IsProbabilityMeasure (bienayme μ)

instance PoissonDeclumping.PlaneTree.isProbabilityMeasure_bienayme {μ : PMF ℕ} [hc : Fact (IsCritical μ)] [hne : Fact (μ 1 ≠ 1)] : MeasureTheory.IsProbabilityMeasure (bienayme μ)

Instance form of bienayme_isProbabilityMeasure, for use with Fact hypotheses.

theorem PoissonDeclumping.PlaneTree.tsum_weight {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : ∑' (T : PlaneTree), weight μ T = 1

The weights ∏_{u∈T} μ_{k_u(T)} of all finite plane trees sum to one.

The root degree and the conditional branching property

theorem PoissonDeclumping.PlaneTree.bienayme_rootDegree_eq_mul_pow (μ : PMF ℕ) (k : ℕ) : (bienayme μ) {T : PlaneTree | T.rootDegree = k} = μ k * (bienayme μ) Set.univ ^ k

𝐏_μ(k_∅ = k) = μ_k 𝐏_μ(univ)^k for every offspring law.

theorem PoissonDeclumping.PlaneTree.bienayme_rootDegree_eq {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (k : ℕ) : (bienayme μ) {T : PlaneTree | T.rootDegree = k} = μ k

For critical μ with μ_1 ≠ 1, the root degree of a μ-Bienaymé tree has law μ.

theorem PoissonDeclumping.PlaneTree.map_rootDegree_bienayme {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : MeasureTheory.Measure.map rootDegree (bienayme μ) = μ.toMeasure

theorem PoissonDeclumping.PlaneTree.cond_rootDegree_children_mem {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {k : ℕ} (hk : μ k ≠ 0) (A : ℕ → Set PlaneTree) : (bienayme μ)[{T : PlaneTree | ∀ (i : ℕ) (hi : i < T.children.length), T.children[i] ∈ A i} | {T : PlaneTree | T.rootDegree = k}] = ∏ i ∈ Finset.range k, (bienayme μ) (A i)

Branching property, conditional form (source lines 696–698): for critical μ with μ_1 ≠ 1 and μ_k ≠ 0, conditionally on the root having k children, the child subtrees T_0, …, T_{k-1} are independent μ-Bienaymé trees: 𝐏_μ(T_i ∈ A_i for all i < k | k_∅ = k) = ∏_{i<k} 𝐏_μ(A_i).