Lemma lem:root_declumping(i),(ii) in the paper's notation

Source lines 2197–2229. This restates the general results of PoissonDeclumping.RootDeclumping.ParentFormula with the paper's objects: the sequence π_n = P(G_{k_n}(𝒯) = 1) = markProb μ G k n, the declumped marks Ghat_k = declumpedMark B G_k, the constant c_B = cB μ B of Statements.Main (an extended nonnegative real, finite for critical μ), and limits along admissible sizes (admissibleSizes μ).

Part (iii) (raw Assumption (S) implies declumped Assumption (M)) needs forest and local-limit estimates and is not proved here.

theorem PoissonDeclumping.RootDeclumping.cB_ne_top {μ : PMF ℕ} (hc : IsCritical μ) (B : Set ℕ) : cB μ B ≠ ⊤

For critical μ, the constant c_B of Statements.Main is finite.

theorem PoissonDeclumping.RootDeclumping.cBReal_eq_toReal_cB {μ : PMF ℕ} (B : Set ℕ) : cBReal μ B = (cB μ B).toReal

The real value of the constant c_B of Statements.Main is cBReal μ B = ∑_{j ∈ B} j μ_j (for critical μ, c_B is finite by cB_ne_top).

theorem PoissonDeclumping.RootDeclumping.cB_pos_iff {μ : PMF ℕ} (hc : IsCritical μ) (B : Set ℕ) : 0 < cB μ B ↔ 0 < cBReal μ B

theorem PoissonDeclumping.RootDeclumping.lem_root_declumping {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) (B : Set ℕ) (hB : 0 < cB μ B) : bB μ B = (PlaneTree.bienayme μ).real {T : PlaneTree | T.rootDegree ∈ B ∧ 1 ≤ T.rootDegree} ∧ 0 < bB μ B ∧ (∀ (n : ℕ), bB μ B * markProb μ G k n ≤ markProb μ (fun (j : ℕ) => PlaneTree.declumpedMark B (G j)) k n) ∧ ((∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) → Filter.Tendsto (fun (n : ℕ) => ↑n * markProb μ (fun (j : ℕ) => PlaneTree.declumpedMark B (G j)) k n - (cB μ B).toReal * (↑n * markProb μ G k n)) (admissibleSizes μ) (nhds 0)) ∧ (Filter.Tendsto (fun (n : ℕ) => ↑n * markProb μ G k n) (admissibleSizes μ) Filter.atTop → Filter.Tendsto (fun (n : ℕ) => ↑n * markProb μ (fun (j : ℕ) => PlaneTree.declumpedMark B (G j)) k n) (admissibleSizes μ) Filter.atTop)

Lemma lem:root_declumping, first assertion and parts (i), (ii) (source lines 2197–2229). Let μ be critical with μ_1 ≠ 1, (G_k) marks, (k_n) a sequence, and B ⊆ ℕ with c_B > 0 (the standing assumption c_B ∈ (0, ∞) of Section 5; finiteness is automatic). Then b_B = P(k_∅(𝒯) ∈ B, k_∅(𝒯) ≥ 1) > 0, π̂_n ≥ b_B π_n for every n, and, along admissible sizes: (i) if (n π_n) is bounded, then n π̂_n - c_B n π_n → 0; (ii) if n π_n → ∞, then n π̂_n → ∞.