Leaf-height marks: Assumptions (S) and (C) (Lemmas lem:S_lh and lem:C_lh)

Section 7.2 of the paper, source lines 3029–3236 (inventory L7.3 (i), L7.5, P23 (use), P25). Marks: G_k(T) = 1{λ_∅(T) ≥ k} and Ghat_k = 1{k_∅ ≥ κ + 1} 1{∃ child c, λ_∅(T_c) ≥ k} (RootDeclumping.lhDeclumpedMark μ k), with κ = min{j ≥ 1 : μ_j > 0} (LeafHeight.kappa μ), π_k = P(λ_∅(𝒯) ≥ k) (LeafHeight.piSeq μ k), π̂_k = P(Ghat_k(𝒯) = 1) and c = 1 - κ μ_κ (LeafHeight.cConst μ).

Main statements

• lem_S_lh (Lemma lem:S_lh(i)): if k_n = n^{o(1)} (κ = 1), resp. κ^{k_n} = n^{o(1)} (κ ≥ 2), then (G_k) satisfies Assumption (S) along (k_n) with respect to M_n = max 1 ⌊n^{1-η}⌋₊, η ∈ (0, 1 - 1/α): Lemma lem:critM applied to the decomposition RootDeclumping.lhSkeleton (P23, already proved) with E_k[C_k + L_k] ≤ C k + 1 resp. ≤ C κ^k. Part (ii) (E[N_{k_n}(𝒯^n)] ∼ n π_{k_n}) is Corollary cor:SM(ii) and is not included.
• le_rootLeafHeight_replaceAt: if λ_∅(T) ≥ k, re-grafting at a vertex u a tree S with λ_∅(S) ≥ min(λ_∅(T_u), k) keeps λ_∅ ≥ k (P25, condition (a) of the cut-and-graft lemma).
• pair_lhDeclumped_le (P25): one constant C with P(|𝒯| ≥ ℓ+1, Ghat_k(𝒯) = 1, Ghat_k(𝒯_{u_{ℓ+1}}) = 1) ≤ C π_k π̂_k for all k and ℓ ≥ 1.
• lem_C_lh (Lemma lem:C_lh): if c > 0, then (Ghat_k) satisfies Assumption (C) for every level sequence and every cutoff with M_n = o(n).

Departure in the proof of P25

The paper's selector is τ(A) = 0 if a root child other than the one above ⋆ witnesses the root event, and τ(A) = (k - h(A))_+ otherwise (h(A) the depth of ⋆ below that child). We use instead the minimal admissible selector τ(A) = min{m ≤ k : λ_∅(S) ≥ m ⇒ A[S] ∈ {Ghat_k = 1}}. Condition (a) of Lemma lem:cut_graft then holds by definition, and condition (b) follows from le_rootLeafHeight_replaceAt: on the double event 𝒯 = A[S], m = min(λ_∅(S), k) is admissible, so τ(A) ≤ λ_∅(S). The rest (Lemma lem:lh_conditional_mark and π̂_k ≥ b π_k) is as in the paper. No case distinction on the witness, and no notion of depth of ⋆, is needed.

theorem PoissonDeclumping.PlaneTree.le_rootLeafHeight_replaceAt (k : ℕ) {T : PlaneTree} {ℓ : ℕ} {S : PlaneTree} : k ≤ T.rootLeafHeight → ℓ < T.vertexCount → min (T.fringeAt ℓ).rootLeafHeight k ≤ S.rootLeafHeight → k ≤ (T.replaceAt ℓ S).rootLeafHeight

If λ_∅(T) ≥ k and the vertex u of DFS index ℓ is replaced by a tree S with λ_∅(S) ≥ min(λ_∅(T_u), k), then still λ_∅ ≥ k: the new leaves are at depth depth(u) + (depth in S) ≥ k, since λ_∅(T_u) ≥ k - depth(u).

Lemma lem:S_lh(i)

theorem PoissonDeclumping.Applications.lintegral_lhSkeleton_zero_le (μ : PMF ℕ) : ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ↑(ω.2.1 + ω.2.2.length) ∂RootDeclumping.lhSkeleton μ 0 ≤ 1

E_0[C_0 + L_0] = 1 (no skeleton, one frontier vertex: the root).

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

The moment bound of the leaf-height skeleton for all levels (P23): one C > 0 with E_k[C_k + L_k] ≤ C k + 1 if κ = 1 and ≤ C κ^k if κ ≥ 2, for every k ≥ 0.

theorem PoissonDeclumping.Applications.lem_S_lh {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {η : ℝ} (hη : 0 < η ∧ η < 1 - 1 / α) {k : ℕ → ℕ} (hk1 : LeafHeight.kappa μ = 1 → ∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑(k n) ≤ ↑n ^ δ) (hk2 : 2 ≤ LeafHeight.kappa μ → ∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑(LeafHeight.kappa μ) ^ k n ≤ ↑n ^ δ) : StructuralMicroscopic μ a (fun (j : ℕ) (T : PlaneTree) => j ≤ T.rootLeafHeight) k fun (n : ℕ) => max 1 ⌊↑n ^ (1 - η)⌋₊

Lemma lem:S_lh(i) (source lines 3053–3130): let (k_n) be such that k_n = n^{o(1)} if κ = 1, and κ^{k_n} = n^{o(1)} if κ ≥ 2 (used through the upper halves ≤ n^δ, for every δ > 0, eventually along admissible sizes). Then for every η ∈ (0, 1 - 1/α) the leaf-height marks G_k = 1{λ_∅ ≥ k} satisfy Assumption (S) along (k_n) with respect to M_n = max 1 ⌊n^{1-η}⌋₊ (= ⌊n^{1-η}⌋ for n ≥ 1).

Lemma lem:C_lh

theorem PoissonDeclumping.Applications.pair_lhDeclumped_le {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : ∃ (C : ℝ), 0 < C ∧ ∀ (k ℓ : ℕ), 1 ≤ ℓ → (PlaneTree.bienayme μ).real {T : PlaneTree | ℓ + 1 ≤ T.vertexCount ∧ RootDeclumping.lhDeclumpedMark μ k T ∧ ∃ U ∈ T.fringeTrees[ℓ]?, RootDeclumping.lhDeclumpedMark μ k U} ≤ C * LeafHeight.piSeq μ k * (PlaneTree.bienayme μ).real {T : PlaneTree | RootDeclumping.lhDeclumpedMark μ k T}

P25 (source lines 3190–3234, before the final use of c > 0): there is one C > 0 such that for all k and all ℓ ≥ 1, P(|𝒯| ≥ ℓ+1, Ghat_k(𝒯) = 1, Ghat_k(𝒯_{u_{ℓ+1}(𝒯)}) = 1) ≤ C π_k π̂_k. Lemma lem:cut_graft is applied with 𝓔 = {Ghat_k = 1}, 𝓠_m = {λ_∅ ≥ m} (0 ≤ m ≤ k) and the minimal admissible selector, then Lemma lem:lh_conditional_mark.

theorem PoissonDeclumping.Applications.lem_C_lh {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hcpos : 0 < LeafHeight.cConst μ) (k M : ℕ → ℕ) (hM : (fun (n : ℕ) => ↑(M n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) : NonClustering μ (fun (j : ℕ) => RootDeclumping.lhDeclumpedMark μ j) k M

Lemma lem:C_lh (source lines 3183–3236): if c = 1 - κ μ_κ > 0, then for every level sequence (k_n) and every cutoff sequence with M_n = o(n), the declumped leaf-height marks Ghat_k satisfy Assumption (C): Â_n(ℓ) ≤ C' π̂_{k_n}² uniformly in ℓ ≥ 1 (with C' = C / b, b = P(k_∅ ≥ κ + 1) > 0), hence ∑_{ℓ=1}^{M_n} Â_n(ℓ) ≤ C' M_n π̂_{k_n}² = o(n π̂_{k_n}²).

theorem PoissonDeclumping.Applications.lem_C_lh_of_isCutoff {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hcpos : 0 < LeafHeight.cConst μ) (k : ℕ → ℕ) {M : ℕ → ℕ} (hM : IsCutoff M) : NonClustering μ (fun (j : ℕ) => RootDeclumping.lhDeclumpedMark μ j) k M

Lemma lem:C_lh for every cutoff sequence (IsCutoff M).