Non-fringe patterns: grafting at the leaves and the conditional law (U06)

Source lines 682 (definition of T' ≺ T), 1433–1445 (inventory U06) and 2468–2476.

T' ≺ T (PlaneTree.Embeds T' T) means that T is obtained from T' by grafting plane trees onto the leaves of T'; internal vertices of T' keep their exact outdegree.

• leafCount T' (number of leaves L), internalCount T' (number of internal vertices C) and patternWeight μ T' = ∏_{v ∈ T' internal} μ_{k_v(T')}.
• leafTrees T' T = (𝒯^{(1)}, …, 𝒯^{(L)}): the trees grafted onto the leaves of T', in DFS order; graftLeaves T' ls = T'[ls] grafts a list of L trees. embedsEquiv T' is the bijection {T : T' ≺ T} ≃ {lists of L trees}; weight_eq_of_embeds: 𝐏(𝒯 = T) = patternWeight μ T' ∏_i 𝐏(𝒯 = 𝒯^{(i)}); vertexCount_eq_of_embeds: |T| = C + ∑_{i ≤ L} |𝒯^{(i)}|.
• forestLaw μ L: the law of a list of L independent μ-Bienaymé trees.
• U06: bienayme_embeds_eq: 𝐏(T' ≺ 𝒯) = ∏_{v ∈ T' internal} μ_{k_v(T')}; bienayme_embeds_leafTrees_mem, map_cond_embeds_leafTrees, cond_embeds_leafTrees_pi: conditionally on T' ≺ 𝒯, the grafted trees 𝒯^{(1)}, …, 𝒯^{(L)} are i.i.d. (unconditioned) μ-Bienaymé trees; cond_embeds_eq_map_graftLeaves: conditionally on T' ≺ 𝒯, 𝒯 has the law of T'[𝒯^{(1)}, …, 𝒯^{(L)}]; skeleton_embeds: the resulting decomposition (𝒯, C, (𝒯^{(1)}, …, 𝒯^{(L)})) is a PoissonDeclumping.Skeleton for the mark T' ≺ · (Assumption (S) shape, used in the proof of Corollary cor:Non-fringe Poisson), with deterministic C = internalCount T' and L = leafCount T' (embedsSkeletonLaw_ae).

Leaves, internal vertices and the pattern weight

def PoissonDeclumping.PlaneTree.leafCount (T : PlaneTree) : ℕ

The number of leaves (vertices of outdegree 0).

Equations

• T.leafCount = List.count 0 T.degSeq

def PoissonDeclumping.PlaneTree.internalCount (T : PlaneTree) : ℕ

The number of internal vertices (vertices of positive outdegree).

Equations

• T.internalCount = List.countP (fun (x : ℕ) => decide (x ≠ 0)) T.degSeq

noncomputable def PoissonDeclumping.PlaneTree.patternWeight (μ : PMF ℕ) (T : PlaneTree) : ENNReal

∏_{v ∈ T internal} μ_{k_v(T)}: the product of the offspring masses over the internal vertices only (leaves of a pattern receive grafted trees and contribute no factor).

Equations

• PoissonDeclumping.PlaneTree.patternWeight μ T = (List.map (⇑μ) (List.filter (fun (x : ℕ) => decide (x ≠ 0)) T.degSeq)).prod

@[simp]

theorem PoissonDeclumping.PlaneTree.degSeq_leaf : (node []).degSeq = [0]

@[simp]

theorem PoissonDeclumping.PlaneTree.leafCount_leaf : (node []).leafCount = 1

@[simp]

theorem PoissonDeclumping.PlaneTree.internalCount_leaf : (node []).internalCount = 0

@[simp]

theorem PoissonDeclumping.PlaneTree.patternWeight_leaf (μ : PMF ℕ) : patternWeight μ (node []) = 1

theorem PoissonDeclumping.PlaneTree.leafCount_node {ts : List PlaneTree} (hts : ts ≠ []) : (node ts).leafCount = (List.map leafCount ts).sum

theorem PoissonDeclumping.PlaneTree.internalCount_node {ts : List PlaneTree} (hts : ts ≠ []) : (node ts).internalCount = (List.map internalCount ts).sum + 1

theorem PoissonDeclumping.PlaneTree.patternWeight_node (μ : PMF ℕ) {ts : List PlaneTree} (hts : ts ≠ []) : patternWeight μ (node ts) = μ ts.length * (List.map (patternWeight μ) ts).prod

theorem PoissonDeclumping.PlaneTree.leafCount_add_internalCount (T : PlaneTree) : T.leafCount + T.internalCount = T.vertexCount

Embeddings

theorem PoissonDeclumping.PlaneTree.embeds_node_iff {cs : List PlaneTree} (hcs : cs ≠ []) {T : PlaneTree} : (node cs).Embeds T ↔ List.Forall₂ Embeds cs T.children

theorem PoissonDeclumping.PlaneTree.Embeds.induction' {P : PlaneTree → PlaneTree → Prop} (hleaf : ∀ (T : PlaneTree), P (PlaneTree.node []) T) (hnode : ∀ (cs ts : List PlaneTree), cs ≠ [] → List.Forall₂ (fun (c t : PlaneTree) => c.Embeds t ∧ P c t) cs ts → P (PlaneTree.node cs) (PlaneTree.node ts)) {T' T : PlaneTree} (h : T'.Embeds T) : P T' T

Induction principle for Embeds with the children handled by List.Forall₂.

def PoissonDeclumping.PlaneTree.leafTrees : PlaneTree → PlaneTree → List PlaneTree

leafTrees T' T: for T' ≺ T, the list (𝒯^{(1)}, …, 𝒯^{(L)}) of the fringe subtrees of T at the images of the leaves of T', in DFS order (meaningful only when Embeds T' T).

Equations

• (PoissonDeclumping.PlaneTree.node []).leafTrees x✝ = [x✝]
• (PoissonDeclumping.PlaneTree.node (c :: cs)).leafTrees x✝ = PoissonDeclumping.PlaneTree.leafTreesForest (c :: cs) x✝.children

def PoissonDeclumping.PlaneTree.leafTreesForest : List PlaneTree → List PlaneTree → List PlaneTree

Forest version of leafTrees: concatenation over matched children.

Equations

• PoissonDeclumping.PlaneTree.leafTreesForest (c :: cs) (t :: ts) = c.leafTrees t ++ PoissonDeclumping.PlaneTree.leafTreesForest cs ts
• PoissonDeclumping.PlaneTree.leafTreesForest x✝¹ x✝ = []

@[simp]

theorem PoissonDeclumping.PlaneTree.leafTrees_leaf (T : PlaneTree) : (node []).leafTrees T = [T]

theorem PoissonDeclumping.PlaneTree.leafTrees_node {cs : List PlaneTree} (hcs : cs ≠ []) (T : PlaneTree) : (node cs).leafTrees T = leafTreesForest cs T.children

@[simp]

theorem PoissonDeclumping.PlaneTree.leafTreesForest_cons (c t : PlaneTree) (cs ts : List PlaneTree) : leafTreesForest (c :: cs) (t :: ts) = c.leafTrees t ++ leafTreesForest cs ts

@[simp]

theorem PoissonDeclumping.PlaneTree.leafTreesForest_nil_left (ts : List PlaneTree) : leafTreesForest [] ts = []

theorem PoissonDeclumping.PlaneTree.length_leafTrees {T' T : PlaneTree} (h : T'.Embeds T) : (T'.leafTrees T).length = T'.leafCount

theorem PoissonDeclumping.PlaneTree.weight_eq_of_embeds (μ : PMF ℕ) {T' T : PlaneTree} (h : T'.Embeds T) : weight μ T = patternWeight μ T' * (List.map (weight μ) (T'.leafTrees T)).prod

theorem PoissonDeclumping.PlaneTree.vertexCount_eq_of_embeds {T' T : PlaneTree} (h : T'.Embeds T) : T.vertexCount = T'.internalCount + (List.map vertexCount (T'.leafTrees T)).sum

theorem PoissonDeclumping.PlaneTree.eq_of_leafTrees_eq {T' T₁ T₂ : PlaneTree} (h₁ : T'.Embeds T₁) (h₂ : T'.Embeds T₂) (h : T'.leafTrees T₁ = T'.leafTrees T₂) : T₁ = T₂

theorem PoissonDeclumping.PlaneTree.exists_embeds_leafTrees_eq (T' : PlaneTree) (ls : List PlaneTree) : ls.length = T'.leafCount → ∃ (T : PlaneTree), T'.Embeds T ∧ T'.leafTrees T = ls

noncomputable def PoissonDeclumping.PlaneTree.graftLeaves (T' : PlaneTree) (ls : List PlaneTree) : PlaneTree

T'[ls]: the tree obtained by grafting the trees of the list ls (of length leafCount T') onto the leaves of T', in DFS order; characterized by embeds_graftLeaves and graftLeaves_leafTrees (for lists of the wrong length it is the junk value T').

Equations

• T'.graftLeaves ls = if h : ∃ (T : PoissonDeclumping.PlaneTree), T'.Embeds T ∧ T'.leafTrees T = ls then h.choose else T'

theorem PoissonDeclumping.PlaneTree.embeds_graftLeaves {T' : PlaneTree} {ls : List PlaneTree} (hls : ls.length = T'.leafCount) : T'.Embeds (T'.graftLeaves ls) ∧ T'.leafTrees (T'.graftLeaves ls) = ls

theorem PoissonDeclumping.PlaneTree.graftLeaves_leafTrees {T' T : PlaneTree} (h : T'.Embeds T) : T'.graftLeaves (T'.leafTrees T) = T

noncomputable def PoissonDeclumping.PlaneTree.embedsEquiv (T' : PlaneTree) : { T : PlaneTree // T'.Embeds T } ≃ { ls : List PlaneTree // ls.length = T'.leafCount }

The bijection {T : T' ≺ T} ≃ {(𝒯^{(1)}, …, 𝒯^{(L)})}.

Equations

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

Forest law

noncomputable def PoissonDeclumping.PlaneTree.forestLaw (μ : PMF ℕ) (L : ℕ) : MeasureTheory.Measure (List PlaneTree)

The law of L independent μ-Bienaymé trees, as a measure on lists of trees: forestLaw μ L {[t_1, …, t_L]} = ∏_i 𝐏_μ(t_i), and lists of other lengths have mass zero.

Equations

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

theorem PoissonDeclumping.PlaneTree.forestLaw_apply (μ : PMF ℕ) (L : ℕ) (B : Set (List PlaneTree)) : (forestLaw μ L) B = ∑' (ls : List PlaneTree), (B ∩ {ls : List PlaneTree | ls.length = L}).indicator (fun (ls : List PlaneTree) => (List.map (weight μ) ls).prod) ls

theorem PoissonDeclumping.PlaneTree.forestLaw_univ (μ : PMF ℕ) (L : ℕ) : (forestLaw μ L) Set.univ = (bienayme μ) Set.univ ^ L

theorem PoissonDeclumping.PlaneTree.forestLaw_pi (μ : PMF ℕ) (L : ℕ) (A : ℕ → Set PlaneTree) : (forestLaw μ L) {ls : List PlaneTree | ∀ (i : ℕ) (hi : i < ls.length), ls[i] ∈ A i} = ∏ i ∈ Finset.range L, (bienayme μ) (A i)

theorem PoissonDeclumping.PlaneTree.forestLaw_singleton (μ : PMF ℕ) (L : ℕ) (ls : List PlaneTree) : (forestLaw μ L) {ls} = {ls : List PlaneTree | ls.length = L}.indicator (fun (ls : List PlaneTree) => (List.map (weight μ) ls).prod) ls

U06: the law of a non-fringe pattern occurrence

theorem PoissonDeclumping.PlaneTree.bienayme_embeds_leafTrees_mem (μ : PMF ℕ) (T' : PlaneTree) (B : Set (List PlaneTree)) : (bienayme μ) {T : PlaneTree | T'.Embeds T ∧ T'.leafTrees T ∈ B} = patternWeight μ T' * (forestLaw μ T'.leafCount) B

𝐏_μ(T' ≺ 𝒯, (𝒯^{(1)}, …, 𝒯^{(L)}) ∈ B) = (∏_{v ∈ T' internal} μ_{k_v}) 𝐏(F_L ∈ B), where F_L is a list of L independent μ-Bienaymé trees (any offspring law).

theorem PoissonDeclumping.PlaneTree.bienayme_embeds (μ : PMF ℕ) (T' : PlaneTree) : (bienayme μ) {T : PlaneTree | T'.Embeds T} = patternWeight μ T' * (bienayme μ) Set.univ ^ T'.leafCount

theorem PoissonDeclumping.PlaneTree.bienayme_embeds_eq {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (T' : PlaneTree) : (bienayme μ) {T : PlaneTree | T'.Embeds T} = patternWeight μ T'

U06/U07: 𝐏(T' ≺ 𝒯) = ∏_{v ∈ T' internal} μ_{k_v(T')} for critical μ with μ_1 ≠ 1.

theorem PoissonDeclumping.PlaneTree.bienayme_embeds_leafTrees_pi (μ : PMF ℕ) (T' : PlaneTree) (A : ℕ → Set PlaneTree) : (bienayme μ) {T : PlaneTree | T'.Embeds T ∧ ∀ (i : ℕ) (hi : i < (T'.leafTrees T).length), (T'.leafTrees T)[i] ∈ A i} = patternWeight μ T' * ∏ i ∈ Finset.range T'.leafCount, (bienayme μ) (A i)

The grafted trees are independent μ-Bienaymé trees: 𝐏(T' ≺ 𝒯, 𝒯^{(i)} ∈ A_i ∀ i) = patternWeight μ T' ∏_{i < L} 𝐏(𝒯 ∈ A_i).

theorem PoissonDeclumping.PlaneTree.cond_embeds_leafTrees_mem {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {T' : PlaneTree} (hpos : 0 < (bienayme μ) {T : PlaneTree | T'.Embeds T}) (B : Set (List PlaneTree)) : (bienayme μ)[{T : PlaneTree | T'.leafTrees T ∈ B} | {T : PlaneTree | T'.Embeds T}] = (forestLaw μ T'.leafCount) B

U06: conditionally on T' ≺ 𝒯, the grafted list (𝒯^{(1)}, …, 𝒯^{(L)}) has the law of L independent unconditioned μ-Bienaymé trees.

theorem PoissonDeclumping.PlaneTree.map_cond_embeds_leafTrees {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {T' : PlaneTree} (hpos : 0 < (bienayme μ) {T : PlaneTree | T'.Embeds T}) : MeasureTheory.Measure.map T'.leafTrees (bienayme μ)[|{T : PlaneTree | T'.Embeds T}] = forestLaw μ T'.leafCount

U06, law form: the image of 𝐏(· | T' ≺ 𝒯) under T ↦ (𝒯^{(1)}, …, 𝒯^{(L)}) is the law of L independent μ-Bienaymé trees.

theorem PoissonDeclumping.PlaneTree.cond_embeds_leafTrees_pi {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {T' : PlaneTree} (hpos : 0 < (bienayme μ) {T : PlaneTree | T'.Embeds T}) (A : ℕ → Set PlaneTree) : (bienayme μ)[{T : PlaneTree | ∀ (i : ℕ) (hi : i < (T'.leafTrees T).length), (T'.leafTrees T)[i] ∈ A i} | {T : PlaneTree | T'.Embeds T}] = ∏ i ∈ Finset.range T'.leafCount, (bienayme μ) (A i)

U06, product form: 𝐏(𝒯^{(i)} ∈ A_i for all i < L | T' ≺ 𝒯) = ∏_{i < L} 𝐏(𝒯 ∈ A_i).

theorem PoissonDeclumping.PlaneTree.forestLaw_length_eq (μ : PMF ℕ) (L n : ℕ) : (forestLaw μ L) {ls : List PlaneTree | ls.length = n} = if n = L then (bienayme μ) Set.univ ^ L else 0

noncomputable def PoissonDeclumping.PlaneTree.embedsSkeletonLaw (μ : PMF ℕ) (T' : PlaneTree) : MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)

The law ρ of (𝒯, C, (𝒯^{(1)}, …, 𝒯^{(L)})) under 𝐏(· | T' ≺ 𝒯), with the deterministic number C = internalCount T' of internal vertices of the pattern.

Equations

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

theorem PoissonDeclumping.PlaneTree.embedsSkeletonLaw_apply (μ : PMF ℕ) (T' : PlaneTree) (S : Set (PlaneTree × ℕ × List PlaneTree)) : (embedsSkeletonLaw μ T') S = (bienayme μ)[{T : PlaneTree | (T, T'.internalCount, T'.leafTrees T) ∈ S} | {T : PlaneTree | T'.Embeds T}]

theorem PoissonDeclumping.PlaneTree.skeleton_embeds {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {T' : PlaneTree} (hpos : 0 < (bienayme μ) {T : PlaneTree | T'.Embeds T}) : Skeleton μ T'.Embeds (embedsSkeletonLaw μ T')

U06 in the shape of Assumption (S) (source lines 1437–1440): for critical μ with μ_1 ≠ 1 and 𝐏(T' ≺ 𝒯) > 0, embedsSkeletonLaw μ T' is a skeleton decomposition for the mark T' ≺ ·: under 𝐏(· | T' ≺ 𝒯), |𝒯| = C + ∑_{i ≤ L} |𝒯^{(i)}| with i.i.d. unconditioned 𝒯^{(i)}.

theorem PoissonDeclumping.PlaneTree.embedsSkeletonLaw_ae (μ : PMF ℕ) (T' : PlaneTree) : ∀ᵐ (ω : PlaneTree × ℕ × List PlaneTree) ∂embedsSkeletonLaw μ T', ω.2.1 = T'.internalCount ∧ ω.2.2.length = T'.leafCount ∧ ω.1 = T'.graftLeaves ω.2.2

Under ρ, C and L are deterministic and 𝒯 = T'[𝒯^{(1)}, …, 𝒯^{(L)}].

theorem PoissonDeclumping.PlaneTree.cond_embeds_eq_map_graftLeaves {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {T' : PlaneTree} (hpos : 0 < (bienayme μ) {T : PlaneTree | T'.Embeds T}) : (bienayme μ)[|{T : PlaneTree | T'.Embeds T}] = MeasureTheory.Measure.map T'.graftLeaves (forestLaw μ T'.leafCount)

U06, tree form: conditionally on T' ≺ 𝒯, the tree 𝒯 has the law of T'[𝒯^{(1)}, …, 𝒯^{(L)}] with 𝒯^{(1)}, …, 𝒯^{(L)} independent μ-Bienaymé trees.