Consequences of the root leaf-height asymptotics

• Remark after Lemma lem:ell_asymp (source lines 3007–3025, inventory R7.2): the exact root leaf-height probabilities ℓ_k = π_k - π_{k+1} satisfy π_{k+1}/π_k → μ_1, ℓ_k ∼ (1 - μ_1) C_μ μ_1^k if μ_1 > 0, and ℓ_k ∼ π_k ∼ μ_κ^{-1/(κ-1)} D_μ^{κ^k} if μ_1 = 0.
• Inventory U13 (source lines 3473–3491): if μ_1 = 0 and n π_{k_n} is bounded then n π_{k_n + 1} → 0, i.e. n |π_{k_n} - ℓ_{k_n}| → 0.
• Inventory U09 (source lines 3031–3042, 3274–3296): c = E[k_∅ 1{k_∅ ≥ κ+1}] = 1 - κ μ_κ ≥ 0; c = 0 forces μ_1 = 0, supp μ ⊆ {0, κ} and μ_κ = 1/κ; then π_k = μ_κ^{(κ^k - 1)/(κ - 1)}, D_μ = μ_κ^{1/(κ-1)}, log(1/D_μ) = log(1/μ_κ)/(κ - 1), and the centerings k_n^{**} and t_n^{**} agree.

Consecutive ratios and ℓ_k (Remark R7.2)

theorem PoissonDeclumping.LeafHeight.piSeq_succ_bounds {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : mass μ 1 * piSeq μ k ≤ piSeq μ (k + 1) ∧ piSeq μ (k + 1) ≤ mass μ 1 * piSeq μ k + piSeq μ k ^ 2

μ_1 π_k ≤ π_{k+1} ≤ μ_1 π_k + π_k^2.

theorem PoissonDeclumping.LeafHeight.tendsto_piSeq_succ_div {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : Filter.Tendsto (fun (k : ℕ) => piSeq μ (k + 1) / piSeq μ k) Filter.atTop (nhds (mass μ 1))

π_{k+1} / π_k → μ_1 (in both cases of the remark).

theorem PoissonDeclumping.LeafHeight.tendsto_ellSeq_div_piSeq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : Filter.Tendsto (fun (k : ℕ) => ellSeq μ k / piSeq μ k) Filter.atTop (nhds (1 - mass μ 1))

ℓ_k / π_k → 1 - μ_1.

theorem PoissonDeclumping.LeafHeight.ellSeq_isEquivalent_mul_piSeq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : Asymptotics.IsEquivalent Filter.atTop (ellSeq μ) fun (k : ℕ) => (1 - mass μ 1) * piSeq μ k

ℓ_k ∼ (1 - μ_1) π_k.

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

Remark R7.2, case μ_1 > 0: ℓ_k ∼ (1 - μ_1) C_μ μ_1^k.

theorem PoissonDeclumping.LeafHeight.piSeq_succ_le_sq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) (k : ℕ) : piSeq μ (k + 1) ≤ piSeq μ k ^ 2

If μ_1 = 0, then π_{k+1} ≤ π_k^2.

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

Remark R7.2, case μ_1 = 0: π_{k+1} / π_k → 0.

theorem PoissonDeclumping.LeafHeight.ellSeq_isEquivalent_piSeq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : Asymptotics.IsEquivalent Filter.atTop (ellSeq μ) (piSeq μ)

Remark R7.2, case μ_1 = 0: ℓ_k ∼ π_k.

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

Remark R7.2, case μ_1 = 0: ℓ_k ∼ μ_κ^{-1/(κ-1)} D_μ^{κ^k}.

Interchangeability of the Poisson parameters (U13)

theorem PoissonDeclumping.LeafHeight.tendsto_mul_piSeq_succ_of_bounded {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) {ι : Type u_1} {l : Filter ι} {n : ι → ℝ} {k : ι → ℕ} (hn : Filter.Tendsto n l Filter.atTop) (hbd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (i : ι) => n i * piSeq μ (k i)) : Filter.Tendsto (fun (i : ι) => n i * piSeq μ (k i + 1)) l (nhds 0)

U13, general form: if μ_1 = 0, n_i → ∞ and n_i π_{k_i} is bounded above, then n_i π_{k_i + 1} → 0.

theorem PoissonDeclumping.LeafHeight.tendsto_natCast_mul_piSeq_succ {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) {k : ℕ → ℕ} (hbd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => ↑n * piSeq μ (k n)) : Filter.Tendsto (fun (n : ℕ) => ↑n * piSeq μ (k n + 1)) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => ↑n * |piSeq μ (k n) - ellSeq μ (k n)|) Filter.atTop (nhds 0)

U13 as used in the source: if μ_1 = 0 and (n π_{k_n})_n is bounded, then n π_{k_n+1} → 0 and n |π_{k_n} - ℓ_{k_n}| → 0.

theorem PoissonDeclumping.LeafHeight.mass_zero_mul_piSeq_le_ellSeq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : mass μ 0 * piSeq μ k ≤ ellSeq μ k

μ_0 π_k ≤ ℓ_k, so boundedness of n ℓ_{k_n} and of n π_{k_n} are equivalent.

theorem PoissonDeclumping.LeafHeight.tendsto_natCast_mul_piSeq_succ_of_ell {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) {k : ℕ → ℕ} (hbd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => ↑n * ellSeq μ (k n)) : Filter.Tendsto (fun (n : ℕ) => ↑n * piSeq μ (k n + 1)) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => ↑n * |piSeq μ (k n) - ellSeq μ (k n)|) Filter.atTop (nhds 0)

U13 with the bounded-mean hypothesis stated for n ℓ_{k_n} instead of n π_{k_n}.

The constant c = 1 - κ μ_κ (U09)

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

c = 1 - κ μ_κ (source line 3031).

Equations

• PoissonDeclumping.LeafHeight.cConst μ = 1 - ↑(PoissonDeclumping.LeafHeight.kappa μ) * PoissonDeclumping.LeafHeight.mass μ (PoissonDeclumping.LeafHeight.kappa μ)

theorem PoissonDeclumping.LeafHeight.hasSum_cConst {μ : PMF ℕ} (hc : IsCritical μ) : HasSum (fun (j : ℕ) => if kappa μ + 1 ≤ j then ↑j * mass μ j else 0) (cConst μ)

c = E[k_∅ 1{k_∅ ≥ κ + 1}] = ∑_{j ≥ κ + 1} j μ_j (source line 3031).

theorem PoissonDeclumping.LeafHeight.cConst_nonneg {μ : PMF ℕ} (hc : IsCritical μ) : 0 ≤ cConst μ

U09: c ≥ 0.

theorem PoissonDeclumping.LeafHeight.cConst_pos_of_pos {μ : PMF ℕ} (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) : 0 < cConst μ

If μ_1 > 0 then κ = 1 and c = 1 - μ_1 > 0 (source line 3299).

theorem PoissonDeclumping.LeafHeight.mass_eq_zero_of_cConst_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (hc0 : cConst μ = 0) {j : ℕ} (hj0 : j ≠ 0) (hjk : j ≠ kappa μ) : mass μ j = 0

U09: if c = 0 then μ_j = 0 for every j ∉ {0, κ}.

theorem PoissonDeclumping.LeafHeight.support_subset_of_cConst_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (hc0 : cConst μ = 0) : μ.support ⊆ {0, kappa μ}

U09: if c = 0 then the support of μ is contained in {0, κ}.

theorem PoissonDeclumping.LeafHeight.mass_kappa_of_cConst_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hc0 : cConst μ = 0) : mass μ (kappa μ) = 1 / ↑(kappa μ)

U09: if c = 0 then μ_κ = 1/κ.

theorem PoissonDeclumping.LeafHeight.cConst_eq_zero_iff {μ : PMF ℕ} (hc : IsCritical μ) : cConst μ = 0 ↔ μ.support ⊆ {0, kappa μ}

U09: c = 0 exactly when μ is supported on {0, κ} (source lines 3040–3041).

theorem PoissonDeclumping.LeafHeight.two_le_kappa_of_cConst_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hc0 : cConst μ = 0) : 2 ≤ kappa μ ∧ μ 1 = 0

U09: if c = 0 then κ ≥ 2 and μ_1 = 0 (the case c = 0 is a case of μ_1 = 0).

theorem PoissonDeclumping.LeafHeight.g_eq_of_cConst_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hc0 : cConst μ = 0) (x : ℝ) : g μ x = mass μ (kappa μ) * x ^ kappa μ

In the two-point case c = 0: g(x) = μ_κ x^κ.

theorem PoissonDeclumping.LeafHeight.piSeq_eq_pow_of_cConst_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hc0 : cConst μ = 0) (k : ℕ) : piSeq μ k = mass μ (kappa μ) ^ ∑ i ∈ Finset.range k, kappa μ ^ i

In the two-point case c = 0: π_k = μ_κ^{1 + κ + ⋯ + κ^{k-1}}.

theorem PoissonDeclumping.LeafHeight.piSeq_eq_rpow_of_cConst_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hc0 : cConst μ = 0) (k : ℕ) : piSeq μ k = mass μ (kappa μ) ^ ((↑(kappa μ) ^ k - 1) / (↑(kappa μ) - 1)) ∧ piSeq μ k = mass μ (kappa μ) ^ (-1 / (↑(kappa μ) - 1)) * (mass μ (kappa μ) ^ (1 / (↑(kappa μ) - 1))) ^ kappa μ ^ k

In the two-point case c = 0 (source lines 3283–3287): π_k = μ_κ^{(κ^k - 1)/(κ - 1)} = μ_κ^{-1/(κ-1)} (μ_κ^{1/(κ-1)})^{κ^k}.

theorem PoissonDeclumping.LeafHeight.leafD_of_cConst_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hc0 : cConst μ = 0) : leafD μ = mass μ (kappa μ) ^ (1 / (↑(kappa μ) - 1))

In the two-point case c = 0: D_μ = μ_κ^{1/(κ-1)} (source line 3288).

theorem PoissonDeclumping.LeafHeight.log_inv_leafD_of_cConst_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hc0 : cConst μ = 0) : Real.log (1 / leafD μ) = Real.log (1 / mass μ (kappa μ)) / (↑(kappa μ) - 1)

In the two-point case c = 0: log(1/D_μ) = log(1/μ_κ)/(κ - 1) (source line 3290).

theorem PoissonDeclumping.LeafHeight.centering_eq_of_cConst_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hc0 : cConst μ = 0) (n : ℕ) : Real.logb (↑(kappa μ)) (Real.log ↑n) - Real.logb (↑(kappa μ)) (Real.log (1 / leafD μ)) = Real.logb (↑(kappa μ)) (Real.log ↑n) - Real.logb (↑(kappa μ)) (Real.log (1 / mass μ (kappa μ)) / (↑(kappa μ) - 1))

In the two-point case c = 0, the centering k_n^{**} = log_κ log n - log_κ log(1/D_μ) of Theorem thm:max_lh(ii) equals the centering t_n^{**} = log_r log n - log_r (log(1/μ_r)/(r - 1)) of Theorem thm:max_string(ii) with r = κ (source lines 3291–3293).