Doubly exponential level intensities: centering, thresholds, two-point levels

Deterministic part of Theorem thm:max_string(ii) (source lines 486–501, proof 2851–2897, inventory P20) and of the case μ_1 = 0, c > 0 of Theorem thm:max_lh(ii) (source lines 542–558, proof 3328–3383, inventory P24).

Let r ≥ 2 be an integer, D ∈ (0, 1) and x_n = log_r log n - log_r log(1/D), so that r^{x_n} = log n / log(1/D) for n ≥ 2 (rpow_doubleLogCenter). Write m_n = ⌊x_n⌋, θ_n = {x_n}.

• Exact identity (natCast_mul_pow_pow_eq): n D^{r^k} = n^{1 - r^{k - x_n}} for n ≥ 2, every k ∈ ℕ. For k = m_n + j this is n^{1 - r^{j - θ_n}}.
• If p_k ∼ A D^{r^k} with A > 0 then for every fixed j ∈ ℤ, n p_{m_n + j} ∼ A n^{1 - r^{j - θ_n}} (isEquivalent_level; source lines 2855–2858 and 3336–3342; the levels m_n + j are eventually nonnegative).
• Thresholds, along any filter l ≤ atTop (a subsequence, e.g. admissible sizes or the indices with θ_n ≤ 1/2): if the integer level h_n satisfies h_n ≥ x_n + δ eventually then n p_{h_n} → 0; if x_n - K ≤ h_n ≤ x_n - δ eventually then n p_{h_n} → ∞ (tendsto_mul_zero_of_isEquivalent, tendsto_mul_atTop_of_isEquivalent). These are the inputs of eq:threshold_rary / eq:threshold_lh.
• Two-point levels: with a_n = twoPointLow x_n, J_n = {a_n, a_n + 1}, n p_{a_n} → ∞ and n p_{a_n + 2} → 0 along the whole sequence (twoPoint_thresholds); the source's split at θ_n = 1/2 is also provided (fract_le_half_thresholds, half_lt_fract_thresholds). Interior phase (δ ≤ min(θ_n, 1 - θ_n) eventually along l): n p_{m_n} → ∞, n p_{m_n + 1} → 0 along l (interior_thresholds).
• Level sizes: every level h_n ≤ x_n + K satisfies r^{h_n} = O(log n), hence r^{h_n} ≤ n^δ eventually for every δ > 0 (pow_level_le_rpow), the hypothesis of Lemmas lem:S_rary(i) and lem:S_lh(i).
• Complete r-ary specialization (D = μ_r^{1/(r-1)}, A = μ_r^{-1/(r-1)}): π_k = μ_r^{(r^k-1)/(r-1)} = A D^{r^k} exactly (rary_pi_eq), the centering is t_n^{**} = tStarStar r μ_r n (tStarStar_eq), and n π_k = μ_r^{-1/(r-1)} n^{1 - r^{k - t_n^{**}}} exactly for n ≥ 2 (rary_natCast_mul_eq).

theorem PoissonDeclumping.ExtremesAnalysis.log_one_div_pos {D : ℝ} (hD0 : 0 < D) (hD1 : D < 1) : 0 < Real.log (1 / D)

theorem PoissonDeclumping.ExtremesAnalysis.tendsto_doubleLogCenter {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) : Filter.Tendsto x Filter.atTop Filter.atTop

x_n → ∞.

theorem PoissonDeclumping.ExtremesAnalysis.rpow_doubleLogCenter {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {n : ℕ} (hn : 2 ≤ n) : ↑r ^ x n = Real.log ↑n / Real.log (1 / D)

r^{x_n} = log n / log(1/D) for n ≥ 2 (source lines 2853 and 3335).

theorem PoissonDeclumping.ExtremesAnalysis.natCast_mul_pow_pow_eq {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {n : ℕ} (hn : 2 ≤ n) (k : ℕ) : ↑n * D ^ r ^ k = ↑n ^ (1 - ↑r ^ (↑k - x n))

Exact identity: n D^{r^k} = n^{1 - r^{k - x_n}} for n ≥ 2.

theorem PoissonDeclumping.ExtremesAnalysis.tendsto_mul_pow_pow_zero {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {l : Filter ℕ} (hl : l ≤ Filter.atTop) {h : ℕ → ℤ} {δ : ℝ} (hδ : 0 < δ) (hh : ∀ᶠ (n : ℕ) in l, x n + δ ≤ ↑(h n)) : Filter.Tendsto (fun (n : ℕ) => ↑n * D ^ r ^ (h n).toNat) l (nhds 0)

If h_n ≥ x_n + δ eventually along l, then n D^{r^{h_n}} → 0 along l.

theorem PoissonDeclumping.ExtremesAnalysis.tendsto_mul_pow_pow_atTop {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {l : Filter ℕ} (hl : l ≤ Filter.atTop) {h : ℕ → ℤ} {δ : ℝ} (hδ : 0 < δ) (hh : ∀ᶠ (n : ℕ) in l, ↑(h n) ≤ x n - δ) : Filter.Tendsto (fun (n : ℕ) => ↑n * D ^ r ^ (h n).toNat) l Filter.atTop

If h_n ≤ x_n - δ eventually along l, then n D^{r^{h_n}} → ∞ along l (no lower bound on h_n is needed for the exact intensity).

theorem PoissonDeclumping.ExtremesAnalysis.pow_level_le_rpow {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {h : ℕ → ℤ} {K : ℝ} (hh : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(h n) ≤ x n + K) (δ : ℝ) : 0 < δ → ∀ᶠ (n : ℕ) in Filter.atTop, ↑r ^ (h n).toNat ≤ ↑n ^ δ

Every level h_n ≤ x_n + K satisfies r^{h_n} ≤ n^δ eventually, for every δ > 0 (r^{h_n} = O(log n); source lines 2860, 2881, 2889 and 3344).

Transfer to p_k ∼ A D^{r^k}

theorem PoissonDeclumping.ExtremesAnalysis.isEquivalent_mul_comp {r : ℕ} {D : ℝ} {p : ℕ → ℝ} {A : ℝ} (hp : Asymptotics.IsEquivalent Filter.atTop p fun (k : ℕ) => A * D ^ r ^ k) {l : Filter ℕ} {k : ℕ → ℕ} (hk : Filter.Tendsto k l Filter.atTop) : Asymptotics.IsEquivalent l (fun (n : ℕ) => ↑n * p (k n)) fun (n : ℕ) => A * (↑n * D ^ r ^ k n)

If the natural levels k_n → ∞ along l, then n p_{k_n} ∼ A n D^{r^{k_n}} along l.

theorem PoissonDeclumping.ExtremesAnalysis.tendsto_mul_zero_of_isEquivalent {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {p : ℕ → ℝ} {A : ℝ} (hp : Asymptotics.IsEquivalent Filter.atTop p fun (k : ℕ) => A * D ^ r ^ k) {l : Filter ℕ} (hl : l ≤ Filter.atTop) {h : ℕ → ℤ} {δ : ℝ} (hδ : 0 < δ) (hh : ∀ᶠ (n : ℕ) in l, x n + δ ≤ ↑(h n)) : Filter.Tendsto (fun (n : ℕ) => ↑n * p (h n).toNat) l (nhds 0)

n p_{h_n} → 0 along l whenever h_n ≥ x_n + δ eventually along l.

theorem PoissonDeclumping.ExtremesAnalysis.tendsto_mul_atTop_of_isEquivalent {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {p : ℕ → ℝ} {A : ℝ} (hp : Asymptotics.IsEquivalent Filter.atTop p fun (k : ℕ) => A * D ^ r ^ k) (hA : 0 < A) {l : Filter ℕ} (hl : l ≤ Filter.atTop) {h : ℕ → ℤ} {δ K : ℝ} (hδ : 0 < δ) (hlow : ∀ᶠ (n : ℕ) in l, x n - K ≤ ↑(h n)) (hh : ∀ᶠ (n : ℕ) in l, ↑(h n) ≤ x n - δ) : Filter.Tendsto (fun (n : ℕ) => ↑n * p (h n).toNat) l Filter.atTop

n p_{h_n} → ∞ along l whenever x_n - K ≤ h_n ≤ x_n - δ eventually along l (A > 0).

theorem PoissonDeclumping.ExtremesAnalysis.isEquivalent_level {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {p : ℕ → ℝ} {A : ℝ} (hp : Asymptotics.IsEquivalent Filter.atTop p fun (k : ℕ) => A * D ^ r ^ k) (j : ℤ) : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑n * p (⌊x n⌋ + j).toNat) fun (n : ℕ) => A * ↑n ^ (1 - ↑r ^ (↑j - Int.fract (x n)))

Source lines 2855–2858 and 3336–3342: for every fixed j ∈ ℤ, n p_{m_n + j} ∼ A n^{1 - r^{j - θ_n}} with m_n = ⌊x_n⌋, θ_n = {x_n}.

The two-point and interior levels

theorem PoissonDeclumping.ExtremesAnalysis.twoPoint_thresholds {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {p : ℕ → ℝ} {A : ℝ} (hp : Asymptotics.IsEquivalent Filter.atTop p fun (k : ℕ) => A * D ^ r ^ k) (hA : 0 < A) {l : Filter ℕ} (hl : l ≤ Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => ↑n * p (twoPointLow (x n)).toNat) l Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => ↑n * p (twoPointLow (x n) + 2).toNat) l (nhds 0)

Two-point levels (source lines 2862–2880 and 3358–3374, without splitting): with a_n = twoPointLow x_n (so J_n = {a_n, a_n + 1}), n p_{a_n} → ∞ and n p_{a_n + 2} → 0 along any l ≤ atTop.

theorem PoissonDeclumping.ExtremesAnalysis.fract_le_half_thresholds {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {p : ℕ → ℝ} {A : ℝ} (hp : Asymptotics.IsEquivalent Filter.atTop p fun (k : ℕ) => A * D ^ r ^ k) (hA : 0 < A) {l : Filter ℕ} (hl : l ≤ Filter.atTop) (hθ : ∀ᶠ (n : ℕ) in l, Int.fract (x n) ≤ 1 / 2) : Filter.Tendsto (fun (n : ℕ) => ↑n * p (⌊x n⌋ - 1).toNat) l Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => ↑n * p (⌊x n⌋ + 1).toNat) l (nhds 0)

Source's split, indices with θ_n ≤ 1/2 (source lines 2862–2870, 3363–3366): n p_{m_n - 1} → ∞ and n p_{m_n + 1} → 0.

theorem PoissonDeclumping.ExtremesAnalysis.half_lt_fract_thresholds {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {p : ℕ → ℝ} {A : ℝ} (hp : Asymptotics.IsEquivalent Filter.atTop p fun (k : ℕ) => A * D ^ r ^ k) (hA : 0 < A) {l : Filter ℕ} (hl : l ≤ Filter.atTop) (hθ : ∀ᶠ (n : ℕ) in l, 1 / 2 < Int.fract (x n)) : Filter.Tendsto (fun (n : ℕ) => ↑n * p ⌊x n⌋.toNat) l Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => ↑n * p (⌊x n⌋ + 2).toNat) l (nhds 0)

Source's split, indices with θ_n > 1/2 (source lines 2872–2877, 3366–3368): n p_{m_n} → ∞ and n p_{m_n + 2} → 0.

theorem PoissonDeclumping.ExtremesAnalysis.interior_thresholds {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {p : ℕ → ℝ} {A : ℝ} (hp : Asymptotics.IsEquivalent Filter.atTop p fun (k : ℕ) => A * D ^ r ^ k) (hA : 0 < A) {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 * p ⌊x n⌋.toNat) l Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => ↑n * p (⌊x n⌋ + 1).toNat) l (nhds 0)

Interior phase (source lines 2882–2895, 3375–3381): if δ ≤ min(θ_n, 1 - θ_n) eventually along l, then n p_{m_n} → ∞ and n p_{m_n + 1} → 0 along l.

theorem PoissonDeclumping.ExtremesAnalysis.shifted_thresholds {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) {p : ℕ → ℝ} {A : ℝ} (hp : Asymptotics.IsEquivalent Filter.atTop p fun (k : ℕ) => A * D ^ r ^ k) (hA : 0 < A) {δ : ℝ} (hδ : 0 < δ) : (∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ↑r ^ ⌊x n - δ⌋.toNat ≤ ↑n ^ ε) ∧ (∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ↑r ^ ⌈x n + δ⌉.toNat ≤ ↑n ^ ε) ∧ Filter.Tendsto (fun (n : ℕ) => ↑n * p ⌊x n - δ⌋.toNat) Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => ↑n * p ⌈x n + δ⌉.toNat) Filter.atTop (nhds 0)

Shifted levels have global intensity limits and subpolynomial size. On phase-separated subsequences they agree with the floor and the next integer, respectively.

theorem PoissonDeclumping.ExtremesAnalysis.levels_le_rpow {r : ℕ} {D : ℝ} {x : ℕ → ℝ} (hr : 2 ≤ r) (hD0 : 0 < D) (hD1 : D < 1) (hx : ∀ (n : ℕ), x n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / D))) : (∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in Filter.atTop, ↑r ^ (twoPointLow (x n)).toNat ≤ ↑n ^ δ) ∧ (∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in Filter.atTop, ↑r ^ (twoPointLow (x n) + 2).toNat ≤ ↑n ^ δ) ∧ ∀ j ≤ 2, ∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in Filter.atTop, ↑r ^ (⌊x n⌋ + j).toNat ≤ ↑n ^ δ

Level sizes for all levels used: r^{a_n}, r^{a_n + 2}, r^{m_n + j} (j ≤ 2) are ≤ n^δ eventually, for every δ > 0.

Complete r-ary trees (Theorem thm:max_string(ii))

theorem PoissonDeclumping.ExtremesAnalysis.log_one_div_rpow_inv {r : ℕ} {μ : ℝ} (hμ0 : 0 < μ) : Real.log (1 / μ ^ (1 / (↑r - 1))) = Real.log (1 / μ) / (↑r - 1)

log(1/μ^{1/(r-1)}) = log(1/μ)/(r - 1).

theorem PoissonDeclumping.ExtremesAnalysis.tStarStar_eq {r : ℕ} {μ : ℝ} (hμ0 : 0 < μ) (n : ℕ) : tStarStar r μ n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / μ ^ (1 / (↑r - 1))))

The centering t_n^{**} is the doubly logarithmic centering with D = μ_r^{1/(r-1)}.

theorem PoissonDeclumping.ExtremesAnalysis.rary_pi_eq {r : ℕ} {μ : ℝ} (hr : 2 ≤ r) (hμ0 : 0 < μ) (k : ℕ) : μ ^ ((r ^ k - 1) / (r - 1)) = μ ^ (-1 / (↑r - 1)) * (μ ^ (1 / (↑r - 1))) ^ r ^ k

π_k = μ_r^{(r^k - 1)/(r - 1)} = μ_r^{-1/(r-1)} (μ_r^{1/(r-1)})^{r^k} (source line 2855, with the natural-number exponent of Patterns.Complete).

theorem PoissonDeclumping.ExtremesAnalysis.rary_natCast_mul_eq {r : ℕ} {μ : ℝ} (hr : 2 ≤ r) (hμ0 : 0 < μ) (hμ1 : μ < 1) {n : ℕ} (hn : 2 ≤ n) (k : ℕ) : ↑n * μ ^ ((r ^ k - 1) / (r - 1)) = μ ^ (-1 / (↑r - 1)) * ↑n ^ (1 - ↑r ^ (↑k - tStarStar r μ n))

Source lines 2853–2858, exact form: n π_k = μ_r^{-1/(r-1)} n^{1 - r^{k - t_n^{**}}} for n ≥ 2 and every level k; with k = m_n + j this is μ_r^{-1/(r-1)} n^{1 - r^{j - θ_n}}.

theorem PoissonDeclumping.ExtremesAnalysis.rary_natCast_mul_level_eq {r : ℕ} {μ : ℝ} (hr : 2 ≤ r) (hμ0 : 0 < μ) (hμ1 : μ < 1) {n : ℕ} (hn : 2 ≤ n) {j : ℤ} (hj : 0 ≤ ⌊tStarStar r μ n⌋ + j) : ↑n * μ ^ ((r ^ (⌊tStarStar r μ n⌋ + j).toNat - 1) / (r - 1)) = μ ^ (-1 / (↑r - 1)) * ↑n ^ (1 - ↑r ^ (↑j - Int.fract (tStarStar r μ n)))

The same identity at the level k = m_n + j ≥ 0, m_n = ⌊t_n^{**}⌋, θ_n = {t_n^{**}}.

theorem PoissonDeclumping.ExtremesAnalysis.rary_isEquivalent {r : ℕ} {μ : ℝ} (hr : 2 ≤ r) (hμ0 : 0 < μ) : Asymptotics.IsEquivalent Filter.atTop (fun (k : ℕ) => μ ^ ((r ^ k - 1) / (r - 1))) fun (k : ℕ) => μ ^ (-1 / (↑r - 1)) * (μ ^ (1 / (↑r - 1))) ^ r ^ k

π_k = μ_r^{(r^k - 1)/(r - 1)} is (trivially) asymptotically equivalent to its exact form A D^{r^k}; this feeds the generic threshold lemmas.

theorem PoissonDeclumping.ExtremesAnalysis.rary_isEquivalent_level {r : ℕ} {μ : ℝ} (hr : 2 ≤ r) (hμ0 : 0 < μ) (hμ1 : μ < 1) (j : ℤ) : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑n * μ ^ ((r ^ (⌊tStarStar r μ n⌋ + j).toNat - 1) / (r - 1))) fun (n : ℕ) => μ ^ (-1 / (↑r - 1)) * ↑n ^ (1 - ↑r ^ (↑j - Int.fract (tStarStar r μ n)))

Source lines 2855–2858 in the asymptotic form stated there: for every fixed j ∈ ℤ, n π_{m_n + j} ∼ μ_r^{-1/(r-1)} n^{1 - r^{j - θ_n}} (with π_k = μ_r^{(r^k-1)/(r-1)}).

theorem PoissonDeclumping.ExtremesAnalysis.rary_twoPoint_thresholds {r : ℕ} {μ : ℝ} (hr : 2 ≤ r) (hμ0 : 0 < μ) (hμ1 : μ < 1) {l : Filter ℕ} (hl : l ≤ Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => ↑n * μ ^ ((r ^ (twoPointLow (tStarStar r μ n)).toNat - 1) / (r - 1))) l Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => ↑n * μ ^ ((r ^ (twoPointLow (tStarStar r μ n) + 2).toNat - 1) / (r - 1))) l (nhds 0)

Theorem thm:max_string(ii), deterministic inputs: two-point levels (along any l ≤ atTop, in particular admissible sizes), with π_k = μ_r^{(r^k-1)/(r-1)} and t_n^{**}.

theorem PoissonDeclumping.ExtremesAnalysis.rary_interior_thresholds {r : ℕ} {μ : ℝ} (hr : 2 ≤ r) (hμ0 : 0 < μ) (hμ1 : μ < 1) {l : Filter ℕ} (hl : l ≤ Filter.atTop) {δ : ℝ} (hδ : 0 < δ) (hθ : ∀ᶠ (n : ℕ) in l, δ ≤ min (Int.fract (tStarStar r μ n)) (1 - Int.fract (tStarStar r μ n))) : Filter.Tendsto (fun (n : ℕ) => ↑n * μ ^ ((r ^ ⌊tStarStar r μ n⌋.toNat - 1) / (r - 1))) l Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => ↑n * μ ^ ((r ^ (⌊tStarStar r μ n⌋ + 1).toNat - 1) / (r - 1))) l (nhds 0)

Theorem thm:max_string(ii), deterministic inputs: interior phase.

theorem PoissonDeclumping.ExtremesAnalysis.rary_levels_le_rpow {r : ℕ} {μ : ℝ} (hr : 2 ≤ r) (hμ0 : 0 < μ) (hμ1 : μ < 1) : (∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in Filter.atTop, ↑r ^ (twoPointLow (tStarStar r μ n)).toNat ≤ ↑n ^ δ) ∧ (∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in Filter.atTop, ↑r ^ (twoPointLow (tStarStar r μ n) + 2).toNat ≤ ↑n ^ δ) ∧ ∀ j ≤ 2, ∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in Filter.atTop, ↑r ^ (⌊tStarStar r μ n⌋ + j).toNat ≤ ↑n ^ δ

Theorem thm:max_string(ii), level sizes: r^{a_n}, r^{a_n+2}, r^{m_n + j} (j ≤ 2) are n^{o(1)}.