Asymptotics of the root leaf-height tail

Lemma lem:ell_asymp of the paper (source lines 2937–3005) and the identification of the constants C_μ, D_μ as limits (source lines 562–586, inventory U03), for the analytic sequence π_0 = 1, π_{k+1} = g(π_k) of PoissonDeclumping.LeafHeight.Recursion.

• If μ_1 > 0: π_k / μ_1^k is nondecreasing and bounded, so it converges to C_μ = lim π_k / μ_1^k ≥ 1, and π_k ∼ C_μ μ_1^k.
• If μ_1 = 0, let κ = min{j ≥ 2 : μ_j > 0} and a = μ_κ. With β = log a / (κ - 1), v_k = (log π_k + β) / κ^k is nondecreasing and u_k = v_k + π_k / (a (κ - 1) κ^k) is nonincreasing; both converge to log D_μ < 0, and 0 ≤ κ^k log D_μ - (log π_k + β) ≤ π_k / (a (κ - 1)) → 0. Hence π_k ∼ μ_κ^{-1/(κ-1)} D_μ^{κ^k} (an asymptotic equivalent, not just a logarithmic estimate), and D_μ = lim π_k^{1/κ^k} ∈ (0, 1).

The proof follows the paper's route; in the second case the paper bounds the tail error using the superexponential bound π_k ≤ A ξ^{κ^k}, while we use the monotone sandwich v_k ≤ log D_μ ≤ u_k, which only needs π_k ↓ 0.

theorem PoissonDeclumping.LeafHeight.sum_piSeq_le {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : ∑ j ∈ Finset.range k, piSeq μ j ≤ (mass μ 0)⁻¹

∑_{j < k} π_j ≤ 1/μ_0 (geometric domination).

theorem PoissonDeclumping.LeafHeight.mass_one_lt_one {μ : PMF ℕ} (h1 : μ 1 ≠ 1) : mass μ 1 < 1

Case μ_1 > 0

noncomputable def PoissonDeclumping.LeafHeight.leafC (μ : PMF ℕ) : ℝ

C_μ = lim_{k → ∞} π_k / μ_1^k (source lines 576–579).

Equations

• PoissonDeclumping.LeafHeight.leafC μ = Filter.atTop.limUnder fun (k : ℕ) => PoissonDeclumping.LeafHeight.piSeq μ k / PoissonDeclumping.LeafHeight.mass μ 1 ^ k

theorem PoissonDeclumping.LeafHeight.g_bounds_of_pos {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : mass μ 1 * x ≤ g μ x ∧ g μ x ≤ mass μ 1 * x + x ^ 2

For μ_1 > 0: μ_1 x ≤ g(x) ≤ μ_1 x + x^2 on [0, 1].

theorem PoissonDeclumping.LeafHeight.ratio_le_ratio_succ {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) (k : ℕ) : piSeq μ k / mass μ 1 ^ k ≤ piSeq μ (k + 1) / mass μ 1 ^ (k + 1)

theorem PoissonDeclumping.LeafHeight.monotone_ratio {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) : Monotone fun (k : ℕ) => piSeq μ k / mass μ 1 ^ k

theorem PoissonDeclumping.LeafHeight.ratio_succ_le {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) (k : ℕ) : piSeq μ (k + 1) / mass μ 1 ^ (k + 1) ≤ piSeq μ k / mass μ 1 ^ k * (1 + piSeq μ k / mass μ 1)

theorem PoissonDeclumping.LeafHeight.ratio_le_exp {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) (k : ℕ) : piSeq μ k / mass μ 1 ^ k ≤ Real.exp ((∑ j ∈ Finset.range k, piSeq μ j) / mass μ 1)

theorem PoissonDeclumping.LeafHeight.bddAbove_ratio {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) : BddAbove (Set.range fun (k : ℕ) => piSeq μ k / mass μ 1 ^ k)

theorem PoissonDeclumping.LeafHeight.tendsto_ratio_leafC {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) : Filter.Tendsto (fun (k : ℕ) => piSeq μ k / mass μ 1 ^ k) Filter.atTop (nhds (leafC μ))

π_k / μ_1^k → C_μ (source lines 576–579 and the proof of Lemma lem:ell_asymp(i)).

theorem PoissonDeclumping.LeafHeight.one_le_leafC {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) : 1 ≤ leafC μ

theorem PoissonDeclumping.LeafHeight.leafC_pos {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) : 0 < leafC μ

theorem PoissonDeclumping.LeafHeight.piSeq_isEquivalent_leafC {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) : Asymptotics.IsEquivalent Filter.atTop (piSeq μ) fun (k : ℕ) => leafC μ * mass μ 1 ^ k

Lemma lem:ell_asymp(i), with the explicit constant: π_k ∼ C_μ μ_1^k.

theorem PoissonDeclumping.LeafHeight.lem_ell_asymp_i {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) : ∃ (C : ℝ), 0 < C ∧ Asymptotics.IsEquivalent Filter.atTop (piSeq μ) fun (k : ℕ) => C * mass μ 1 ^ k

Lemma lem:ell_asymp(i): if μ_1 > 0 there is C_μ > 0 with π_k ∼ C_μ μ_1^k.

Case μ_1 = 0

noncomputable def PoissonDeclumping.LeafHeight.betaC (μ : PMF ℕ) : ℝ

β = log μ_κ / (κ - 1), so that μ_κ^{-1/(κ-1)} = exp (-β).

Equations

• PoissonDeclumping.LeafHeight.betaC μ = Real.log (PoissonDeclumping.LeafHeight.mass μ (PoissonDeclumping.LeafHeight.kappa μ)) / (↑(PoissonDeclumping.LeafHeight.kappa μ) - 1)

noncomputable def PoissonDeclumping.LeafHeight.vSeq (μ : PMF ℕ) (k : ℕ) : ℝ

v_k = (log π_k + β) / κ^k (κ^{-k} log y_k in the paper, with y_k = μ_κ^{1/(κ-1)} π_k).

Equations

• PoissonDeclumping.LeafHeight.vSeq μ k = (Real.log (PoissonDeclumping.LeafHeight.piSeq μ k) + PoissonDeclumping.LeafHeight.betaC μ) / ↑(PoissonDeclumping.LeafHeight.kappa μ) ^ k

noncomputable def PoissonDeclumping.LeafHeight.errSeq (μ : PMF ℕ) (k : ℕ) : ℝ

The error log π_{k+1} - κ log π_k - log μ_κ (log (1 + ε(π_k)) in the paper).

Equations

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

noncomputable def PoissonDeclumping.LeafHeight.uSeq (μ : PMF ℕ) (k : ℕ) : ℝ

The upper companion u_k = v_k + π_k / (μ_κ (κ - 1) κ^k) of v_k.

Equations

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

noncomputable def PoissonDeclumping.LeafHeight.logD (μ : PMF ℕ) : ℝ

log D_μ = lim v_k = sup_k v_k.

Equations

• PoissonDeclumping.LeafHeight.logD μ = ⨆ (k : ℕ), PoissonDeclumping.LeafHeight.vSeq μ k

noncomputable def PoissonDeclumping.LeafHeight.leafD (μ : PMF ℕ) : ℝ

D_μ = lim_{k → ∞} π_k^{1/κ^k} (source lines 576–579), as used in Lemma lem:ell_asymp(ii) (where μ_1 = 0).

Equations

• PoissonDeclumping.LeafHeight.leafD μ = Filter.atTop.limUnder fun (k : ℕ) => PoissonDeclumping.LeafHeight.piSeq μ k ^ (1 / ↑(PoissonDeclumping.LeafHeight.kappa μ) ^ k)

theorem PoissonDeclumping.LeafHeight.vSeq_succ {μ : PMF ℕ} (h2 : 2 ≤ kappa μ) (k : ℕ) : vSeq μ (k + 1) = vSeq μ k + errSeq μ k / ↑(kappa μ) ^ (k + 1)

theorem PoissonDeclumping.LeafHeight.errSeq_bounds {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : 0 ≤ errSeq μ k ∧ errSeq μ k ≤ piSeq μ k / mass μ (kappa μ)

theorem PoissonDeclumping.LeafHeight.monotone_vSeq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : Monotone (vSeq μ)

theorem PoissonDeclumping.LeafHeight.vSeq_le_uSeq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) (k : ℕ) : vSeq μ k ≤ uSeq μ k

theorem PoissonDeclumping.LeafHeight.uSeq_succ_le {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) (k : ℕ) : uSeq μ (k + 1) ≤ uSeq μ k

theorem PoissonDeclumping.LeafHeight.antitone_uSeq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : Antitone (uSeq μ)

theorem PoissonDeclumping.LeafHeight.bddAbove_vSeq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : BddAbove (Set.range (vSeq μ))

theorem PoissonDeclumping.LeafHeight.tendsto_vSeq_logD {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : Filter.Tendsto (vSeq μ) Filter.atTop (nhds (logD μ))

theorem PoissonDeclumping.LeafHeight.vSeq_le_logD {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) (k : ℕ) : vSeq μ k ≤ logD μ

theorem PoissonDeclumping.LeafHeight.logD_le_uSeq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) (k : ℕ) : logD μ ≤ uSeq μ k

theorem PoissonDeclumping.LeafHeight.logD_error_bounds {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) (k : ℕ) : 0 ≤ ↑(kappa μ) ^ k * logD μ - (Real.log (piSeq μ k) + betaC μ) ∧ ↑(kappa μ) ^ k * logD μ - (Real.log (piSeq μ k) + betaC μ) ≤ piSeq μ k / (mass μ (kappa μ) * (↑(kappa μ) - 1))

The tail error estimate after multiplying by κ^k: 0 ≤ κ^k log D_μ - (log π_k + β) ≤ π_k / (μ_κ (κ - 1)).

theorem PoissonDeclumping.LeafHeight.tendsto_logD_error {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : Filter.Tendsto (fun (k : ℕ) => ↑(kappa μ) ^ k * logD μ - (Real.log (piSeq μ k) + betaC μ)) Filter.atTop (nhds 0)

κ^k log D_μ - log π_k - β → 0: the error of the paper's final display, multiplied by κ^k, tends to zero.

theorem PoissonDeclumping.LeafHeight.logD_neg {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : logD μ < 0

theorem PoissonDeclumping.LeafHeight.tendsto_piSeq_rpow {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : Filter.Tendsto (fun (k : ℕ) => piSeq μ k ^ (1 / ↑(kappa μ) ^ k)) Filter.atTop (nhds (Real.exp (logD μ)))

theorem PoissonDeclumping.LeafHeight.leafD_eq_exp_logD {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : leafD μ = Real.exp (logD μ)

D_μ = exp (log D_μ), i.e. the limit lim π_k^{1/κ^k} exists (inventory U03).

theorem PoissonDeclumping.LeafHeight.tendsto_piSeq_rpow_leafD {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : Filter.Tendsto (fun (k : ℕ) => piSeq μ k ^ (1 / ↑(kappa μ) ^ k)) Filter.atTop (nhds (leafD μ))

π_k^{1/κ^k} → D_μ (source lines 576–579).

theorem PoissonDeclumping.LeafHeight.leafD_pos {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : 0 < leafD μ

theorem PoissonDeclumping.LeafHeight.leafD_lt_one {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : leafD μ < 1

theorem PoissonDeclumping.LeafHeight.tendsto_piSeq_div_leafD {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : Filter.Tendsto (fun (k : ℕ) => piSeq μ k / (mass μ (kappa μ) ^ (-1 / (↑(kappa μ) - 1)) * leafD μ ^ kappa μ ^ k)) Filter.atTop (nhds 1)

π_k / (μ_κ^{-1/(κ-1)} D_μ^{κ^k}) → 1.

theorem PoissonDeclumping.LeafHeight.piSeq_isEquivalent_leafD {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : Asymptotics.IsEquivalent Filter.atTop (piSeq μ) fun (k : ℕ) => mass μ (kappa μ) ^ (-1 / (↑(kappa μ) - 1)) * leafD μ ^ kappa μ ^ k

Lemma lem:ell_asymp(ii), with the explicit constant: π_k ∼ μ_κ^{-1/(κ-1)} D_μ^{κ^k}.

theorem PoissonDeclumping.LeafHeight.lem_ell_asymp_ii {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : ∃ (D : ℝ), 0 < D ∧ D < 1 ∧ Asymptotics.IsEquivalent Filter.atTop (piSeq μ) fun (k : ℕ) => mass μ (kappa μ) ^ (-1 / (↑(kappa μ) - 1)) * D ^ kappa μ ^ k

Lemma lem:ell_asymp(ii): if μ_1 = 0 there is D_μ ∈ (0, 1) with π_k ∼ μ_κ^{-1/(κ-1)} D_μ^{κ^k}, where κ = min{j ≥ 2 : μ_j > 0} (kappa_eq_sInf_two).