The skeleton decomposition for the leaf-height marks

The tree-law input of Lemma lem:S_lh (source lines 3066–3114, inventory P23) for the marks G_k(T) = 1{λ_∅(T) ≥ k}. Under P_k = P(· | λ_∅(𝒯) ≥ k) put C_k = Z_0 + ⋯ + Z_{k-1} (skelSize), L_k = Z_k, and let 𝒯^{(1)}, …, 𝒯^{(L_k)} be the fringe subtrees rooted at generation k (gen k). The law lhSkeleton μ k of (𝒯, C_k, (𝒯^{(i)})_{i ≤ L_k}) under P_k is a decomposition in the sense of Assumption (S) (Skeleton, Setup.Marks):

• lhSkeleton_skeleton: its first marginal is P_k; conditionally on (C_k, L_k) the trees 𝒯^{(i)} are independent μ-Bienaymé trees (from bienayme_trunc_mem_gen_eq); and |𝒯| = C_k + ∑_{i ≤ L_k} |𝒯^{(i)}|;
• lintegral_lhSkeleton_le: E_k[C_k + L_k] ≤ C k (κ = 1, k ≥ 1) and ≤ C κ^k (κ ≥ 2).

The remaining step of Lemma lem:S_lh (Lemma lem:critM, which needs the regular variation of (a_n), and Corollary cor:SM) is not proved here.

noncomputable def PoissonDeclumping.RootDeclumping.lhSkeleton (μ : PMF ℕ) (k : ℕ) : MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)

The law of (𝒯, C_k(𝒯), (𝒯_v)_{|v| = k}) under P(· | λ_∅(𝒯) ≥ k).

Equations

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

theorem PoissonDeclumping.RootDeclumping.lintegral_lhSkeleton {μ : PMF ℕ} (k : ℕ) (F : PlaneTree × ℕ × List PlaneTree → ENNReal) : ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), F ω ∂lhSkeleton μ k = ∫⁻ (T : PlaneTree), F (T, PlaneTree.skelSize k T, PlaneTree.gen k T) ∂(PlaneTree.bienayme μ)[|{T : PlaneTree | k ≤ T.rootLeafHeight}]

theorem PoissonDeclumping.RootDeclumping.setOf_le_rootLeafHeight_skelSize_eq (k c : ℕ) (P : List PlaneTree → Prop) : {T : PlaneTree | k ≤ T.rootLeafHeight} ∩ {T : PlaneTree | PlaneTree.skelSize k T = c ∧ P (PlaneTree.gen k T)} = {T : PlaneTree | PlaneTree.trunc k T ∈ {S : PlaneTree | k ≤ S.rootLeafHeight ∧ PlaneTree.skelSize k S = c} ∧ P (PlaneTree.gen k T)}

{λ_∅ ≥ k, C_k = c} is determined by the truncation at height k.

theorem PoissonDeclumping.RootDeclumping.lhSkeleton_skeleton {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : Skeleton μ (fun (T : PlaneTree) => k ≤ T.rootLeafHeight) (lhSkeleton μ k)

Assumption (S) decomposition for G_k = 1{λ_∅ ≥ k} (source lines 3066–3083): for a critical μ with μ_1 ≠ 1 and every k, lhSkeleton μ k is a decomposition (𝒯, C_k, 𝒯^{(1)}, …, 𝒯^{(L_k)}) as in Assumption (S).

theorem PoissonDeclumping.RootDeclumping.lintegral_lhSkeleton_le {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : ∃ (C : ℝ), 0 < C ∧ (LeafHeight.kappa μ = 1 → ∀ (k : ℕ), 1 ≤ k → ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ↑(ω.2.1 + ω.2.2.length) ∂lhSkeleton μ k ≤ ENNReal.ofReal (C * ↑k)) ∧ (2 ≤ LeafHeight.kappa μ → ∀ (k : ℕ), ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ↑(ω.2.1 + ω.2.2.length) ∂lhSkeleton μ k ≤ ENNReal.ofReal (C * ↑(LeafHeight.kappa μ) ^ k))

E_k[C_k + L_k] for the skeleton decomposition (source lines 3108–3114): there is C > 0 with E_k[C_k + L_k] ≤ C k for k ≥ 1 if κ = 1, and ≤ C κ^k if κ ≥ 2.

theorem PoissonDeclumping.RootDeclumping.lem_S_lh_tree_input {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : ∃ (ρ : ℕ → MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)), (∀ (k : ℕ), Skeleton μ (fun (T : PlaneTree) => k ≤ T.rootLeafHeight) (ρ k)) ∧ ∃ (C : ℝ), 0 < C ∧ (LeafHeight.kappa μ = 1 → ∀ (k : ℕ), 1 ≤ k → ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ↑(ω.2.1 + ω.2.2.length) ∂ρ k ≤ ENNReal.ofReal (C * ↑k)) ∧ (2 ≤ LeafHeight.kappa μ → ∀ (k : ℕ), ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ↑(ω.2.1 + ω.2.2.length) ∂ρ k ≤ ENNReal.ofReal (C * ↑(LeafHeight.kappa μ) ^ k))

The tree-law input of Lemma lem:S_lh, combined: for every k a decomposition as in Assumption (S) for G_k = 1{λ_∅ ≥ k} exists, with E_k[C_k + L_k] ≤ C k (κ = 1, k ≥ 1) or ≤ C κ^k (κ ≥ 2) for one constant C.