Unary centering: the lattice-modulated Gumbel exponent

Deterministic part of Theorem thm:max_string(i) (source lines 480–485, proof 2815–2850, inventory P20) and of Theorem thm:max_lh(i) (source lines 537–541, proof 3298–3326, inventory P24).

Fix q = μ_1 ∈ (0, 1), c > 0 (the declumping constant c_B = 1 - μ_1) and C > 0, and let x_n = (log n + log (c C)) / log (1/q). For t ∈ ℝ the paper's level is h_n = m_n + 1 = ⌊x_n + t⌋ + 1 ∈ ℤ (which may be ≤ 0 for finitely many n; the mark index is h_n.toNat, and TwoPoint.natCast_le_iff_not_toNat_le identifies {H ≤ ⌊x_n + t⌋} with {h_n.toNat ≤ H}ᶜ for every n). Put Λ_n = q^{t + 1 - {x_n + t}} ∈ (q^{t+1}, q^t].

• Exact identity (natCast_mul_mul_zpow_floor_add_one): n c C q^{⌊x_n + t⌋ + 1} = Λ_n for n ≥ 1 (integer power). With C = 1, c = 1 - μ_1 and x_n = t_n^* this is the display of source line 2821 (tStar_identity).
• If p_k / q^k → C (π_k ∼ C_μ μ_1^k, Lemma lem:ell_asymp(i)), then c n p_{h_n} - Λ_n → 0 (source lines 3305–3309), hence exp(-c n p_{h_n}) - exp(-Λ_n) → 0 (source lines 3320–3326); also n p_{h_n} is bounded (π_{h_n} = O(1/n), needed by Corollary cor:declump_zero) and h_n = n^{o(1)} (needed by Lemmas lem:S_rary(i), lem:S_lh(i); the source writes h_n = O(log n)).

O(log n) sequences are n^{o(1)}

theorem PoissonDeclumping.ExtremesAnalysis.eventually_log_le_mul_rpow {δ ε : ℝ} (hδ : 0 < δ) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, Real.log ↑n ≤ ε * ↑n ^ δ

log n ≤ ε n^δ eventually, for every ε, δ > 0.

theorem PoissonDeclumping.ExtremesAnalysis.eventually_le_rpow_of_le_log {l : Filter ℕ} (hl : l ≤ Filter.atTop) {f : ℕ → ℝ} {A B : ℝ} (hA : 0 ≤ A) (hf : ∀ᶠ (n : ℕ) in l, f n ≤ A * Real.log ↑n + B) (δ : ℝ) : 0 < δ → ∀ᶠ (n : ℕ) in l, f n ≤ ↑n ^ δ

If f_n ≤ A log n + B eventually along l ≤ atTop (with A ≥ 0), then f_n ≤ n^δ eventually along l, for every δ > 0 (the form n^{o(1)} of the hypotheses of Lemmas lem:S_rary(i) and lem:S_lh(i)).

The unary centering

theorem PoissonDeclumping.ExtremesAnalysis.tendsto_unaryCenter {q : ℝ} {x : ℕ → ℝ} (hq0 : 0 < q) (hq1 : q < 1) {a : ℝ} (hx : ∀ (n : ℕ), x n = (Real.log ↑n + a) / Real.log (1 / q)) : Filter.Tendsto x Filter.atTop Filter.atTop

x_n → ∞.

theorem PoissonDeclumping.ExtremesAnalysis.rpow_unaryCenter {q c : ℝ} {x : ℕ → ℝ} (hq0 : 0 < q) (hq1 : q < 1) (hc : 0 < c) (hx : ∀ (n : ℕ), x n = (Real.log ↑n + Real.log c) / Real.log (1 / q)) {n : ℕ} (hn : 0 < n) : q ^ x n = (↑n * c)⁻¹

q^{x_n} = (n c)⁻¹ for n ≥ 1.

theorem PoissonDeclumping.ExtremesAnalysis.natCast_mul_mul_zpow_floor_add_one {q c : ℝ} {x : ℕ → ℝ} (hq0 : 0 < q) (hq1 : q < 1) (hc : 0 < c) (hx : ∀ (n : ℕ), x n = (Real.log ↑n + Real.log c) / Real.log (1 / q)) {n : ℕ} (hn : 0 < n) (t : ℝ) : ↑n * c * q ^ (⌊x n + t⌋ + 1) = q ^ (t + 1 - Int.fract (x n + t))

Exact unary identity: n c q^{⌊x_n + t⌋ + 1} = q^{t + 1 - {x_n + t}} for n ≥ 1 (integer power on the left; the level ⌊x_n + t⌋ + 1 may be nonpositive).

theorem PoissonDeclumping.ExtremesAnalysis.tStar_identity {q : ℝ} (hq0 : 0 < q) (hq1 : q < 1) {n : ℕ} (hn : 0 < n) (t : ℝ) : ↑n * (1 - q) * q ^ (⌊tStar q n + t⌋ + 1) = q ^ (t + 1 - Int.fract (tStar q n + t))

Theorem thm:max_string(i), source line 2821: with t_n^* = tStar μ_1 n, n (1 - μ_1) μ_1^{⌊t_n^* + t⌋ + 1} = μ_1^{t + 1 - {t_n^* + t}} exactly, for n ≥ 1.

theorem PoissonDeclumping.ExtremesAnalysis.rpow_lattice_bounds {q : ℝ} (hq0 : 0 < q) (hq1 : q < 1) (t y : ℝ) : 0 < q ^ (t + 1 - Int.fract y) ∧ q ^ (t + 1 - Int.fract y) ≤ q ^ t

The lattice exponent Λ = q^{t + 1 - {y}} lies in (0, q^t].

theorem PoissonDeclumping.ExtremesAnalysis.eventually_unaryLevel {q : ℝ} {x : ℕ → ℝ} (hq0 : 0 < q) (hq1 : q < 1) {a : ℝ} (hx : ∀ (n : ℕ), x n = (Real.log ↑n + a) / Real.log (1 / q)) (t : ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ ⌊x n + t⌋ + 1 ∧ ↑(⌊x n + t⌋ + 1).toNat = ↑(⌊x n + t⌋ + 1)

The unary levels ⌊x_n + t⌋ + 1 are eventually nonnegative, so their natural indices have the same value.

theorem PoissonDeclumping.ExtremesAnalysis.tendsto_unaryLevel {q : ℝ} {x : ℕ → ℝ} (hq0 : 0 < q) (hq1 : q < 1) {a : ℝ} (hx : ∀ (n : ℕ), x n = (Real.log ↑n + a) / Real.log (1 / q)) (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => (⌊x n + t⌋ + 1).toNat) Filter.atTop Filter.atTop

The natural unary levels tend to infinity.

theorem PoissonDeclumping.ExtremesAnalysis.unaryLevel_le_rpow {q : ℝ} {x : ℕ → ℝ} (hq0 : 0 < q) (hq1 : q < 1) {a : ℝ} (hx : ∀ (n : ℕ), x n = (Real.log ↑n + a) / Real.log (1 / q)) (t δ : ℝ) : 0 < δ → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(⌊x n + t⌋ + 1).toNat ≤ ↑n ^ δ

The unary levels are O(log n), hence n^{o(1)} (hypothesis of Lemmas lem:S_rary(i) with r = 1 and lem:S_lh(i) with κ = 1).

theorem PoissonDeclumping.ExtremesAnalysis.tendsto_mul_sub_lattice {q c : ℝ} {x : ℕ → ℝ} (hq0 : 0 < q) (hq1 : q < 1) (hc : 0 < c) {C : ℝ} (hC : 0 < C) {p : ℕ → ℝ} (hp : Filter.Tendsto (fun (k : ℕ) => p k / q ^ k) Filter.atTop (nhds C)) (hx : ∀ (n : ℕ), x n = (Real.log ↑n + Real.log (c * C)) / Real.log (1 / q)) (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => c * (↑n * p (⌊x n + t⌋ + 1).toNat) - q ^ (t + 1 - Int.fract (x n + t))) Filter.atTop (nhds 0)

If p_k / q^k → C with C > 0 and x_n = (log n + log (c C)) / log (1/q), then c n p_{⌊x_n + t⌋ + 1} - q^{t + 1 - {x_n + t}} → 0 (source lines 3305–3309, and line 2821 with p_k = q^k).

theorem PoissonDeclumping.ExtremesAnalysis.norm_exp_neg_sub_exp_neg_le (a : ℝ) {b : ℝ} (hb : 0 ≤ b) : ‖Real.exp (-a) - Real.exp (-b)‖ ≤ ‖Real.exp (-(a - b)) - 1‖

|e^{-a} - e^{-b}| ≤ |e^{-(a-b)} - 1| for b ≥ 0.

theorem PoissonDeclumping.ExtremesAnalysis.tendsto_exp_sub_lattice {q c : ℝ} {x : ℕ → ℝ} (hq0 : 0 < q) (hq1 : q < 1) (hc : 0 < c) {C : ℝ} (hC : 0 < C) {p : ℕ → ℝ} (hp : Filter.Tendsto (fun (k : ℕ) => p k / q ^ k) Filter.atTop (nhds C)) (hx : ∀ (n : ℕ), x n = (Real.log ↑n + Real.log (c * C)) / Real.log (1 / q)) (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => Real.exp (-(c * (↑n * p (⌊x n + t⌋ + 1).toNat))) - Real.exp (-q ^ (t + 1 - Int.fract (x n + t)))) Filter.atTop (nhds 0)

exp(-c n p_{⌊x_n + t⌋ + 1}) - exp(-q^{t + 1 - {x_n + t}}) → 0: combined with Corollary cor:declump_zero this is the lattice Gumbel limit (source lines 2840–2850, 3320–3326).

theorem PoissonDeclumping.ExtremesAnalysis.exists_eventually_mul_le {q c : ℝ} {x : ℕ → ℝ} (hq0 : 0 < q) (hq1 : q < 1) (hc : 0 < c) {C : ℝ} (hC : 0 < C) {p : ℕ → ℝ} (hp : Filter.Tendsto (fun (k : ℕ) => p k / q ^ k) Filter.atTop (nhds C)) (hx : ∀ (n : ℕ), x n = (Real.log ↑n + Real.log (c * C)) / Real.log (1 / q)) (t : ℝ) : ∃ (K : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ↑n * p (⌊x n + t⌋ + 1).toNat ≤ K

Bounded mean: n p_{⌊x_n + t⌋ + 1} is eventually bounded, i.e. π_{h_n} = O(1/n) (hypothesis of Corollary cor:declump_zero, source lines 2836 and 3318).

Specialization to Theorem thm:max_string(i)

theorem PoissonDeclumping.ExtremesAnalysis.tStar_tendsto_exp_sub {q : ℝ} (hq0 : 0 < q) (hq1 : q < 1) (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => Real.exp (-((1 - q) * (↑n * q ^ (⌊tStar q n + t⌋ + 1).toNat))) - Real.exp (-q ^ (t + 1 - Int.fract (tStar q n + t)))) Filter.atTop (nhds 0)

Theorem thm:max_string(i): with π_k = μ_1^k, c_B = 1 - μ_1 and t_n^* = tStar μ_1 n, exp(-c_B n π_{⌊t_n^* + t⌋ + 1}) - exp(-μ_1^{t + 1 - {t_n^* + t}}) → 0.

theorem PoissonDeclumping.ExtremesAnalysis.tStar_exists_eventually_mul_le {q : ℝ} (hq0 : 0 < q) (hq1 : q < 1) (t : ℝ) : ∃ (K : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ↑n * q ^ (⌊tStar q n + t⌋ + 1).toNat ≤ K

Theorem thm:max_string(i): n μ_1^{⌊t_n^* + t⌋ + 1} is eventually bounded.