Bienaymé trees: weights, the branching property and forests

Source lines 679–704 (Section 2.1) of the paper. For an arbitrary offspring law μ (a PMF on ℕ, no criticality assumed) we prove:

• weight_node: 𝐏_μ(node [t_1,…,t_k]) = μ_k ∏ 𝐏_μ(t_i), and bienayme_apply_singleton: the Bienaymé measure gives each finite tree its weight ∏_{u∈T} μ_{k_u(T)};
• bienayme_apply: the measure of any set of trees is the sum of the weights;
• the branching property (bienayme_children_eq, bienayme_rootDegree_eq_children_mem, bienayme_node_ofFn_mem): given the root degree k, the k child subtrees are independent μ-Bienaymé trees;
• the forest product formulas tsum_forest_fin, tsum_forest_list, and the law of the size bienayme_vertexCount_succ in terms of forest sizes forestSizeWeight;
• bienayme_univ_le_one: the total weight of the finite trees is at most one, so bienayme μ is a finite measure. That it equals one for critical μ with μ 1 ≠ 1 is proved in PoissonDeclumping.Bienayme.Normalization.

Tree combinatorics

theorem PoissonDeclumping.PlaneTree.vertexCount_node (ts : List PlaneTree) : (node ts).vertexCount = (List.map vertexCount ts).sum + 1

The number of vertices is one plus the total size of the root's child trees.

theorem PoissonDeclumping.PlaneTree.eq_node_children (T : PlaneTree) : T = node T.children

A tree is determined by its list of children.

def PoissonDeclumping.PlaneTree.equivList : PlaneTree ≃ List PlaneTree

Finite plane trees are in bijection with lists of finite plane trees (their children).

Equations

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

def PoissonDeclumping.PlaneTree.equivSigma : PlaneTree ≃ (k : ℕ) × (Fin k → PlaneTree)

Finite plane trees are in bijection with pairs (k, (T_0, …, T_{k-1})): the root degree and the ordered tuple of child trees.

Equations

• PoissonDeclumping.PlaneTree.equivSigma = PoissonDeclumping.PlaneTree.equivList.trans List.equivSigmaTuple

@[simp]

theorem PoissonDeclumping.PlaneTree.equivSigma_symm_apply (p : (k : ℕ) × (Fin k → PlaneTree)) : equivSigma.symm p = node (List.ofFn p.snd)

theorem PoissonDeclumping.PlaneTree.tsum_pi_fin_prod {α : Type u_1} (k : ℕ) (g : Fin k → α → ENNReal) : ∑' (f : Fin k → α), ∏ i : Fin k, g i (f i) = ∏ i : Fin k, ∑' (a : α), g i a

Sum over k-tuples of a product of functions of the coordinates (in ℝ≥0∞).

Weights and the Bienaymé measure

theorem PoissonDeclumping.PlaneTree.weight_node (μ : PMF ℕ) (ts : List PlaneTree) : weight μ (node ts) = μ ts.length * (List.map (weight μ) ts).prod

The weight of a tree is μ of the root degree times the weights of the child trees.

theorem PoissonDeclumping.PlaneTree.weight_node_ofFn (μ : PMF ℕ) {k : ℕ} (f : Fin k → PlaneTree) : weight μ (node (List.ofFn f)) = μ k * ∏ i : Fin k, weight μ (f i)

theorem PoissonDeclumping.PlaneTree.bienayme_apply (μ : PMF ℕ) (s : Set PlaneTree) : (bienayme μ) s = ∑' (T : PlaneTree), s.indicator (weight μ) T

𝐏_μ(T ∈ s) = ∑_{T ∈ s} ∏_{u ∈ T} μ_{k_u(T)}.

theorem PoissonDeclumping.PlaneTree.bienayme_apply_singleton (μ : PMF ℕ) (T : PlaneTree) : (bienayme μ) {T} = weight μ T

𝐏_μ(T) = ∏_{u ∈ T} μ_{k_u(T)} (source line 696).

theorem PoissonDeclumping.PlaneTree.bienayme_apply_eq_tsum_sigma (μ : PMF ℕ) (s : Set PlaneTree) : (bienayme μ) s = ∑' (k : ℕ) (f : Fin k → PlaneTree), s.indicator (weight μ) (node (List.ofFn f))

Decomposition of 𝐏_μ(T ∈ s) according to the root degree k and the tuple of child trees.

theorem PoissonDeclumping.PlaneTree.tsum_weight_node_ofFn_indicator (μ : PMF ℕ) (k : ℕ) (A : Fin k → Set PlaneTree) : ∑' (f : Fin k → PlaneTree), {f : Fin k → PlaneTree | ∀ (i : Fin k), f i ∈ A i}.indicator (fun (f : Fin k → PlaneTree) => weight μ (node (List.ofFn f))) f = μ k * ∏ i : Fin k, (bienayme μ) (A i)

For a fixed root degree k, summing the weight of node [T_0, …, T_{k-1}] over the tuples with T_i ∈ A_i gives μ_k ∏_i 𝐏_μ(A_i).

theorem PoissonDeclumping.PlaneTree.bienayme_eq_tsum_of_mem_iff (μ : PMF ℕ) (s : Set PlaneTree) (D : Set ℕ) (A : (k : ℕ) → Fin k → Set PlaneTree) (hs : ∀ (k : ℕ) (f : Fin k → PlaneTree), node (List.ofFn f) ∈ s ↔ k ∈ D ∧ ∀ (i : Fin k), f i ∈ A k i) : (bienayme μ) s = ∑' (k : ℕ), D.indicator (fun (k : ℕ) => μ k * ∏ i : Fin k, (bienayme μ) (A k i)) k

General branching decomposition: if membership of node [T_0, …, T_{k-1}] in s means k ∈ D and T_i ∈ A k i for all i, then 𝐏_μ(s) = ∑_{k ∈ D} μ_k ∏_i 𝐏_μ(A k i).

Branching property

theorem PoissonDeclumping.PlaneTree.bienayme_children_eq (μ : PMF ℕ) (ts : List PlaneTree) : (bienayme μ) {T : PlaneTree | T.children = ts} = μ ts.length * (List.map (fun (U : PlaneTree) => (bienayme μ) {U}) ts).prod

The law of the root's children: 𝐏_μ(children = [t_1, …, t_k]) = μ_k ∏_i 𝐏_μ(t_i).

theorem PoissonDeclumping.PlaneTree.bienayme_rootDegree_eq_children_mem (μ : PMF ℕ) (k : ℕ) (A : ℕ → Set PlaneTree) : (bienayme μ) {T : PlaneTree | T.rootDegree = k ∧ ∀ (i : ℕ) (hi : i < T.children.length), T.children[i] ∈ A i} = μ k * ∏ i ∈ Finset.range k, (bienayme μ) (A i)

Branching property (source lines 696–698): given root degree k, the k child subtrees are independent μ-Bienaymé trees: 𝐏_μ(k_∅ = k, T_i ∈ A_i for all i < k) = μ_k ∏_{i<k} 𝐏_μ(A_i).

theorem PoissonDeclumping.PlaneTree.bienayme_node_ofFn_mem (μ : PMF ℕ) (k : ℕ) (A : Fin k → Set PlaneTree) : (bienayme μ) {T : PlaneTree | ∃ (f : Fin k → PlaneTree), T = node (List.ofFn f) ∧ ∀ (i : Fin k), f i ∈ A i} = μ k * ∏ i : Fin k, (bienayme μ) (A i)

Branching property, Fin-indexed form: for sets A_0, …, A_{k-1}, 𝐏_μ(k_∅ = k, T_i ∈ A_i for all i) = μ_k ∏_i 𝐏_μ(A_i).

theorem PoissonDeclumping.PlaneTree.bienayme_forall_children_mem (μ : PMF ℕ) (A : Set PlaneTree) : (bienayme μ) {T : PlaneTree | ∀ U ∈ T.children, U ∈ A} = ∑' (k : ℕ), μ k * (bienayme μ) A ^ k

𝐏_μ(all children in A) = ∑_k μ_k 𝐏_μ(A)^k, i.e. the generating function of μ evaluated at 𝐏_μ(A).

Forests

theorem PoissonDeclumping.PlaneTree.tsum_forest_fin (μ : PMF ℕ) (k : ℕ) (A : Fin k → Set PlaneTree) : ∑' (f : Fin k → PlaneTree), ∏ i : Fin k, (A i).indicator (weight μ) (f i) = ∏ i : Fin k, (bienayme μ) (A i)

Forest product formula: the total weight of k-tuples of trees with T_i ∈ A_i is ∏_i 𝐏_μ(A_i) (independence of the trees of a forest).

theorem PoissonDeclumping.PlaneTree.tsum_forest_list (μ : PMF ℕ) (k : ℕ) (A : Set PlaneTree) : ∑' (ts : List PlaneTree), {ts : List PlaneTree | ts.length = k ∧ ∀ U ∈ ts, U ∈ A}.indicator (fun (ts : List PlaneTree) => (List.map (weight μ) ts).prod) ts = (bienayme μ) A ^ k

Forest product formula for lists: the total weight of lists of k trees all in A is 𝐏_μ(A)^k.

noncomputable def PoissonDeclumping.PlaneTree.forestSizeWeight (μ : PMF ℕ) (k n : ℕ) : ENNReal

Total weight of the k-tuples of trees with n vertices in total: the probability that a forest of k independent μ-Bienaymé trees has n vertices.

Equations

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

theorem PoissonDeclumping.PlaneTree.bienayme_vertexCount_succ (μ : PMF ℕ) (n : ℕ) : (bienayme μ) {T : PlaneTree | T.vertexCount = n + 1} = ∑' (k : ℕ), μ k * forestSizeWeight μ k n

Law of the size: 𝐏_μ(|T| = n + 1) = ∑_k μ_k 𝐏(|F_k| = n), where F_k is a forest of k independent μ-Bienaymé trees.

theorem PoissonDeclumping.PlaneTree.tsum_forestSizeWeight (μ : PMF ℕ) (k : ℕ) : ∑' (n : ℕ), forestSizeWeight μ k n = (bienayme μ) Set.univ ^ k

Summing over sizes, a forest of k trees has total weight 𝐏_μ(univ)^k.

Total mass at most one

def PoissonDeclumping.PlaneTree.heightLE : ℕ → Set PlaneTree

Trees of height at most h (an auxiliary truncation).

Equations

• PoissonDeclumping.PlaneTree.heightLE 0 = {T : PoissonDeclumping.PlaneTree | T.children = []}
• PoissonDeclumping.PlaneTree.heightLE h.succ = {T : PoissonDeclumping.PlaneTree | ∀ U ∈ T.children, U ∈ PoissonDeclumping.PlaneTree.heightLE h}

theorem PoissonDeclumping.PlaneTree.heightLE_subset_succ (h : ℕ) : heightLE h ⊆ heightLE (h + 1)

theorem PoissonDeclumping.PlaneTree.heightLE_mono : Monotone heightLE

theorem PoissonDeclumping.PlaneTree.exists_mem_heightLE (T : PlaneTree) : ∃ (h : ℕ), T ∈ heightLE h

theorem PoissonDeclumping.PlaneTree.iUnion_heightLE : ⋃ (h : ℕ), heightLE h = Set.univ

theorem PoissonDeclumping.PlaneTree.bienayme_heightLE_le_one (μ : PMF ℕ) (h : ℕ) : (bienayme μ) (heightLE h) ≤ 1

theorem PoissonDeclumping.PlaneTree.bienayme_univ_le_one (μ : PMF ℕ) : (bienayme μ) Set.univ ≤ 1

For every offspring law μ (critical or not), the total Bienaymé weight of the finite plane trees is at most one.

instance PoissonDeclumping.PlaneTree.isFiniteMeasure_bienayme (μ : PMF ℕ) : MeasureTheory.IsFiniteMeasure (bienayme μ)