Level intensities for the leaf-height and the complete r-ary heights #
Specializations of ExtremesAnalysis.Unary and ExtremesAnalysis.Rary to the actual tails
(Theorems thm:max_string and thm:max_lh, inventory P20, P24, U03):
π_k = P(λ_∅(𝒯) ≥ k)for the Bienaymé tree, written(PlaneTree.bienayme μ).real {T | k ≤ T.rootLeafHeight}(themarkProbof the marksG_k = 1{λ_∅ ≥ k}), withπ_k / μ_1^k → C_μ = leafC μifμ_1 > 0andπ_k ∼ μ_κ^{-1/(κ-1)} D_μ^{κ^k},D_μ = leafD μ, ifμ_1 = 0(lem_ell_asymp_i_tree,lem_ell_asymp_ii_tree).μ_1 > 0(Theoremthm:max_lh(i), source lines 3298–3326): withk_n^* = (log n + log((1 - μ_1) C_μ)) / log(1/μ_1)andc_B = 1 - μ_1,exp(-c_B n π_{⌊k_n^* + t⌋ + 1}) - exp(-μ_1^{t + 1 - {k_n^* + t}}) → 0,n π_{h_n}bounded,h_n = n^{o(1)}(lh_unary_inputs).μ_1 = 0(Theoremthm:max_lh(ii) withc > 0, source lines 3328–3383): withk_n^{**} = log_κ log n - log_κ log(1/D_μ):n π_{m_n + j} ∼ μ_κ^{-1/(κ-1)} n^{1 - κ^{j - θ_n}}(lh_isEquivalent_level), the two-point and interior thresholds (lh_twoPoint_thresholds,lh_interior_thresholds) and the level sizes (lh_levels_le_rpow). The positivityc > 0is not used by these analytic statements (it is used by Lemmalem:C_lh).c = 0(source lines 3274–3296):k_n^{**} = t_n^{**}withr = κ,μ_r = μ_κ(lh_center_eq_tStarStar), so the two-point law case is Theoremthm:max_string(ii).- For a critical law and
r ≥ 2:μ_r < 1(toReal_lt_one_of_two_le), the side condition of ther-ary lemmas.
theorem
PoissonDeclumping.ExtremesAnalysis.toReal_lt_one_of_two_le
{μ : PMF ℕ}
(hc : IsCritical μ)
{r : ℕ}
(hr : 2 ≤ r)
:
For a critical law, μ_r ≤ 1/r < 1 whenever r ≥ 2.
μ_1 > 0 #
theorem
PoissonDeclumping.ExtremesAnalysis.lh_unary_inputs
{μ : PMF ℕ}
(hc : IsCritical μ)
(h1 : μ 1 ≠ 1)
(hpos : 0 < μ 1)
{x : ℕ → ℝ}
(hx : ∀ (n : ℕ), x n = (Real.log ↑n + Real.log ((1 - (μ 1).toReal) * LeafHeight.leafC μ)) / Real.log (1 / (μ 1).toReal))
(t : ℝ)
:
Filter.Tendsto
(fun (n : ℕ) =>
Real.exp
(-((1 - (μ 1).toReal) * (↑n * (PlaneTree.bienayme μ).real {T : PlaneTree | (⌊x n + t⌋ + 1).toNat ≤ T.rootLeafHeight}))) - Real.exp (-(μ 1).toReal ^ (t + 1 - Int.fract (x n + t))))
Filter.atTop (nhds 0) ∧ (∃ (K : ℝ),
∀ᶠ (n : ℕ) in Filter.atTop, ↑n * (PlaneTree.bienayme μ).real {T : PlaneTree | (⌊x n + t⌋ + 1).toNat ≤ T.rootLeafHeight} ≤ K) ∧ ∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(⌊x n + t⌋ + 1).toNat ≤ ↑n ^ δ
Theorem thm:max_lh(i), deterministic inputs, with C = C_μ = leafC μ, c_B = 1 - μ_1 and
the level h_n = ⌊k_n^* + t⌋ + 1:
exp(-c_B n π_{h_n}) - exp(-μ_1^{t + 1 - {k_n^* + t}}) → 0, n π_{h_n} is eventually bounded,
and h_n ≤ n^δ eventually for every δ > 0.
μ_1 = 0 #
theorem
PoissonDeclumping.ExtremesAnalysis.lh_isEquivalent_level
{μ : PMF ℕ}
(hc : IsCritical μ)
(h1 : μ 1 ≠ 1)
(h0 : μ 1 = 0)
{x : ℕ → ℝ}
(hx :
∀ (n : ℕ),
x n = Real.logb (↑(LeafHeight.kappa μ)) (Real.log ↑n) - Real.logb (↑(LeafHeight.kappa μ)) (Real.log (1 / LeafHeight.leafD μ)))
(j : ℤ)
:
Asymptotics.IsEquivalent Filter.atTop
(fun (n : ℕ) => ↑n * (PlaneTree.bienayme μ).real {T : PlaneTree | (⌊x n⌋ + j).toNat ≤ T.rootLeafHeight})
fun (n : ℕ) =>
(μ (LeafHeight.kappa μ)).toReal ^ (-1 / (↑(LeafHeight.kappa μ) - 1)) * ↑n ^ (1 - ↑(LeafHeight.kappa μ) ^ (↑j - Int.fract (x n)))
Source lines 3336–3342: for every fixed j ∈ ℤ,
n π_{m_n + j} ∼ μ_κ^{-1/(κ-1)} n^{1 - κ^{j - θ_n}}, m_n = ⌊k_n^{**}⌋, θ_n = {k_n^{**}}.
theorem
PoissonDeclumping.ExtremesAnalysis.lh_twoPoint_thresholds
{μ : PMF ℕ}
(hc : IsCritical μ)
(h1 : μ 1 ≠ 1)
(h0 : μ 1 = 0)
{x : ℕ → ℝ}
(hx :
∀ (n : ℕ),
x n = Real.logb (↑(LeafHeight.kappa μ)) (Real.log ↑n) - Real.logb (↑(LeafHeight.kappa μ)) (Real.log (1 / LeafHeight.leafD μ)))
{l : Filter ℕ}
(hl : l ≤ Filter.atTop)
:
Filter.Tendsto
(fun (n : ℕ) => ↑n * (PlaneTree.bienayme μ).real {T : PlaneTree | (twoPointLow (x n)).toNat ≤ T.rootLeafHeight}) l
Filter.atTop ∧ Filter.Tendsto
(fun (n : ℕ) => ↑n * (PlaneTree.bienayme μ).real {T : PlaneTree | (twoPointLow (x n) + 2).toNat ≤ T.rootLeafHeight})
l (nhds 0)
Two-point levels for the leaf-height (source lines 3358–3374), along any l ≤ atTop: with
a_n = twoPointLow k_n^{**}, n π_{a_n} → ∞ and n π_{a_n + 2} → 0.
theorem
PoissonDeclumping.ExtremesAnalysis.lh_interior_thresholds
{μ : PMF ℕ}
(hc : IsCritical μ)
(h1 : μ 1 ≠ 1)
(h0 : μ 1 = 0)
{x : ℕ → ℝ}
(hx :
∀ (n : ℕ),
x n = Real.logb (↑(LeafHeight.kappa μ)) (Real.log ↑n) - Real.logb (↑(LeafHeight.kappa μ)) (Real.log (1 / LeafHeight.leafD μ)))
{l : Filter ℕ}
(hl : l ≤ Filter.atTop)
{δ : ℝ}
(hδ : 0 < δ)
(hθ : ∀ᶠ (n : ℕ) in l, δ ≤ min (Int.fract (x n)) (1 - Int.fract (x n)))
:
Filter.Tendsto (fun (n : ℕ) => ↑n * (PlaneTree.bienayme μ).real {T : PlaneTree | ⌊x n⌋.toNat ≤ T.rootLeafHeight}) l
Filter.atTop ∧ Filter.Tendsto
(fun (n : ℕ) => ↑n * (PlaneTree.bienayme μ).real {T : PlaneTree | (⌊x n⌋ + 1).toNat ≤ T.rootLeafHeight}) l (nhds 0)
Interior phase for the leaf-height (source lines 3375–3381): if
δ ≤ min(θ_n, 1 - θ_n) eventually along l ≤ atTop, then n π_{m_n} → ∞ and
n π_{m_n + 1} → 0 along l.
theorem
PoissonDeclumping.ExtremesAnalysis.lh_levels_le_rpow
{μ : PMF ℕ}
(hc : IsCritical μ)
(h1 : μ 1 ≠ 1)
(h0 : μ 1 = 0)
{x : ℕ → ℝ}
(hx :
∀ (n : ℕ),
x n = Real.logb (↑(LeafHeight.kappa μ)) (Real.log ↑n) - Real.logb (↑(LeafHeight.kappa μ)) (Real.log (1 / LeafHeight.leafD μ)))
:
(∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(LeafHeight.kappa μ) ^ (twoPointLow (x n)).toNat ≤ ↑n ^ δ) ∧ (∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(LeafHeight.kappa μ) ^ (twoPointLow (x n) + 2).toNat ≤ ↑n ^ δ) ∧ ∀ j ≤ 2, ∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(LeafHeight.kappa μ) ^ (⌊x n⌋ + j).toNat ≤ ↑n ^ δ
Level sizes for the leaf-height (κ^{h_n} = O(log n), hypothesis of Lemma lem:S_lh(i)):
κ^{a_n}, κ^{a_n+2}, κ^{m_n + j} (j ≤ 2) are ≤ n^δ eventually, for every δ > 0.
c = 0: reduction to complete κ-ary trees #
theorem
PoissonDeclumping.ExtremesAnalysis.lh_center_eq_tStarStar
{μ : PMF ℕ}
(hc : IsCritical μ)
(h1 : μ 1 ≠ 1)
(hc0 : LeafHeight.cConst μ = 0)
(n : ℕ)
:
Real.logb (↑(LeafHeight.kappa μ)) (Real.log ↑n) - Real.logb (↑(LeafHeight.kappa μ)) (Real.log (1 / LeafHeight.leafD μ)) = tStarStar (LeafHeight.kappa μ) (μ (LeafHeight.kappa μ)).toReal n
If c = 1 - κ μ_κ = 0 (source lines 3274–3296): k_n^{**} = t_n^{**} with r = κ.