The branching property at generation k

Source lines 3070–3083 (proof of Lemma lem:S_lh, inventory P23): "conditionally on the first k generations, the fringe subtrees rooted at generation k are independent Bienaymé trees".

• trunc k T: the truncation of T at height k (generation-k vertices become leaves); λ_∅ ≥ k and C_k are functions of it (le_rootLeafHeight_trunc_iff, skelSize_trunc), and so is Z_k (genCount_trunc).
• bienayme_trunc_gen_eq (point form): P(𝒯^{≤k} = S, (𝒯_v)_{|v|=k} = (t_1,…,t_L)) equals W_k(S) ∏_j P(𝒯 = t_j) if S is a truncation with Z_k(S) = L, and 0 otherwise (skelWeight: the product of the offspring masses of the vertices of S at depth < k).
• bienayme_trunc_mem_gen_eq (critical μ, μ_1 ≠ 1): P(𝒯^{≤k} ∈ 𝒮, (𝒯_v)_{|v|=k} = (t_1,…,t_L)) = P(𝒯^{≤k} ∈ 𝒮, Z_k = L) ∏_j P(𝒯 = t_j).

def PoissonDeclumping.PlaneTree.trunc : ℕ → PlaneTree → PlaneTree

The truncation T^{≤k} of T at height k: the first k + 1 generations, the vertices of generation k becoming leaves.

Equations

• PoissonDeclumping.PlaneTree.trunc 0 x✝ = PoissonDeclumping.PlaneTree.node []
• PoissonDeclumping.PlaneTree.trunc k.succ x✝ = PoissonDeclumping.PlaneTree.node (List.map (PoissonDeclumping.PlaneTree.trunc k) x✝.children)

@[simp]

theorem PoissonDeclumping.PlaneTree.trunc_zero (T : PlaneTree) : trunc 0 T = node []

@[simp]

theorem PoissonDeclumping.PlaneTree.trunc_succ_node (k : ℕ) (ts : List PlaneTree) : trunc (k + 1) (node ts) = node (List.map (trunc k) ts)

theorem PoissonDeclumping.PlaneTree.genCount_trunc (k : ℕ) (T : PlaneTree) : genCount k (trunc k T) = genCount k T

The number of generation-k vertices is read off the truncation.

theorem PoissonDeclumping.PlaneTree.trunc_trunc (k : ℕ) (T : PlaneTree) : trunc k (trunc k T) = trunc k T

theorem PoissonDeclumping.PlaneTree.skelSize_trunc (k : ℕ) (T : PlaneTree) : skelSize k (trunc k T) = skelSize k T

C_k is read off the truncation.

theorem PoissonDeclumping.PlaneTree.le_rootLeafHeight_trunc_iff (k : ℕ) (T : PlaneTree) : k ≤ (trunc k T).rootLeafHeight ↔ k ≤ T.rootLeafHeight

λ_∅(T) ≥ k is read off the truncation at height k.

theorem PoissonDeclumping.PlaneTree.splitLengths_flatten {α : Type u_1} (L : List (List α)) : (List.map List.length L).splitLengths L.flatten = L

Splitting a flattened list along the lengths of its blocks recovers the blocks.

noncomputable def PoissonDeclumping.PlaneTree.skelWeight (μ : PMF ℕ) : ℕ → PlaneTree → ENNReal

The Bienaymé weight of the first k generations of a skeleton: ∏_{u ∈ S, |u| < k} μ_{k_u(S)}.

Equations

• PoissonDeclumping.PlaneTree.skelWeight μ 0 x✝ = 1
• PoissonDeclumping.PlaneTree.skelWeight μ k.succ x✝ = μ x✝.rootDegree * (List.map (PoissonDeclumping.PlaneTree.skelWeight μ k) x✝.children).prod

theorem PoissonDeclumping.PlaneTree.bienayme_trunc_gen_eq (μ : PMF ℕ) (k : ℕ) (S : PlaneTree) (ts : List PlaneTree) : (bienayme μ) {T : PlaneTree | trunc k T = S ∧ gen k T = ts} = if trunc k S = S ∧ ts.length = genCount k S then skelWeight μ k S * (List.map (weight μ) ts).prod else 0

Branching property at generation k, point form: the truncation at height k and the list of generation-k fringe subtrees of a μ-Bienaymé tree satisfy P(𝒯^{≤k} = S, (𝒯_v)_{|v| = k} = (t_1, …, t_L)) = W_k(S) ∏_j P(𝒯 = t_j) whenever S is a truncation and L = Z_k(S) (and 0 otherwise).

theorem PoissonDeclumping.PlaneTree.bienayme_eq_tsum_inter_fiber {α : Type u_1} (μ : PMF ℕ) (f : PlaneTree → α) (E : Set PlaneTree) : (bienayme μ) E = ∑' (a : α), (bienayme μ) (E ∩ f ⁻¹' {a})

Disintegration of a Bienaymé probability along the fibres of any map.

theorem PoissonDeclumping.PlaneTree.bienayme_trunc_mem_gen_eq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) (𝒮 : Set PlaneTree) (ts : List PlaneTree) : (bienayme μ) {T : PlaneTree | trunc k T ∈ 𝒮 ∧ gen k T = ts} = (bienayme μ) {T : PlaneTree | trunc k T ∈ 𝒮 ∧ (gen k T).length = ts.length} * (List.map (weight μ) ts).prod

Branching property at generation k (source lines 3070–3083): for a critical μ with μ_1 ≠ 1, every event {𝒯^{≤k} ∈ 𝒮} determined by the first k generations, and every list (t_1, …, t_L), P(𝒯^{≤k} ∈ 𝒮, (𝒯_v)_{|v| = k} = (t_1, …, t_L)) = P(𝒯^{≤k} ∈ 𝒮, Z_k = L) ∏_j P(𝒯 = t_j): conditionally on the first k generations, the fringe subtrees rooted at generation k are independent μ-Bienaymé trees.