Uniform ratio bounds and Potter bounds for regularly varying sequences

Source lines 846–853, equation eq: potter_bound. Fix a monotone sequence a : ℕ → ℝ with 0 < a n for n ≥ 1, regularly varying of index ρ ≥ 0 in the sequential sense RegularlyVaryingSeq ρ a.

• RegularlyVaryingSeq.eventually_ratio_bounds: uniformly for n ≤ m ≤ 2n, a m / a n = (1 + o(1)) (m/n)^ρ (uniform convergence on the compact [1,2], obtained from monotonicity and a finite grid, as for the uniform convergence theorem).
• RegularlyVaryingSeq.potter_aux: the two-sided Potter bounds for B ≤ x ≤ y, proved by iterated doubling.
• RegularlyVaryingSeq.potter: the paper's form for a itself: a y / a x ≤ A max ((y/x)^(ρ+δ), (y/x)^(ρ-δ)) for x, y ≥ B.
• RegularlyVaryingSeq.potter_slowlyVarying: the paper's eq: potter_bound for the slowly varying part ℓ(n) = a n / n ^ ρ.
• RegularlyVaryingSeq.exists_potter_global: a version valid for all 1 ≤ x ≤ y, with a constant C in place of A.

The source cites Bingham–Goldie–Teugels, Theorem 1.5.6, for Potter bounds of slowly varying functions; here they are proved directly for monotone sequences, without any measurability or continuity assumption beyond monotonicity.

theorem PoissonDeclumping.RegularlyVaryingSeq.eventually_bounds {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) {c ε : ℝ} (hc : 0 < c) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, (1 - ε) * c ^ ρ < a ⌊c * ↑n⌋₊ / a n ∧ a ⌊c * ↑n⌋₊ / a n < (1 + ε) * c ^ ρ

Eventual two-sided bound at a fixed c > 0.

theorem PoissonDeclumping.RegularlyVaryingSeq.eventually_ratio_bounds {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 ≤ ρ) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ), n ≤ m → m ≤ 2 * n → a m ≤ (1 + ε) * (↑m / ↑n) ^ ρ * a n ∧ (1 - ε) * (↑m / ↑n) ^ ρ * a n ≤ a m

Uniform convergence on [1,2]: for every ε > 0, eventually in n, for all m with n ≤ m ≤ 2n, (1-ε)(m/n)^ρ a n ≤ a m ≤ (1+ε)(m/n)^ρ a n.

theorem PoissonDeclumping.RegularlyVaryingSeq.potter_aux {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 ≤ ρ) {A δ : ℝ} (hA : 1 < A) (hδ : 0 < δ) : ∃ (B : ℕ), 1 ≤ B ∧ ∀ (x y : ℕ), B ≤ x → x ≤ y → a y ≤ A * (↑y / ↑x) ^ (ρ + δ) * a x ∧ (↑y / ↑x) ^ (ρ - δ) * a x ≤ A * a y

Two-sided Potter bounds for a itself, for B ≤ x ≤ y: a y ≤ A (y/x)^(ρ+δ) a x and (y/x)^(ρ-δ) a x ≤ A a y.

theorem PoissonDeclumping.RegularlyVaryingSeq.potter {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 ≤ ρ) {A δ : ℝ} (hA : 1 < A) (hδ : 0 < δ) : ∃ (B : ℕ), 1 ≤ B ∧ ∀ (x y : ℕ), B ≤ x → B ≤ y → a y / a x ≤ A * max ((↑y / ↑x) ^ (ρ + δ)) ((↑y / ↑x) ^ (ρ - δ))

Potter bounds for the regularly varying sequence a itself (source eq. eq: potter_bound, transferred from the slowly varying part to a): for every A > 1 and δ > 0 there is B such that for all x, y ≥ B, a y / a x ≤ A * max ((y/x)^(ρ+δ)) ((y/x)^(ρ-δ)).

theorem PoissonDeclumping.RegularlyVaryingSeq.potter_slowlyVarying {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 ≤ ρ) {A δ : ℝ} (hA : 1 < A) (hδ : 0 < δ) : ∃ (B : ℕ), 1 ≤ B ∧ ∀ (x y : ℕ), B ≤ x → B ≤ y → a y / ↑y ^ ρ / (a x / ↑x ^ ρ) ≤ A * max ((↑y / ↑x) ^ δ) ((↑y / ↑x) ^ (-δ))

Potter bounds (source eq. eq: potter_bound) for the slowly varying part ℓ(n) = a n / n ^ ρ of the sequence: for every A > 1 and δ > 0 there is B such that for all x, y ≥ B, ℓ(y) / ℓ(x) ≤ A * max ((y/x)^δ) ((y/x)^(-δ)).

theorem PoissonDeclumping.RegularlyVaryingSeq.exists_potter_global {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 ≤ ρ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x y : ℕ), 1 ≤ x → x ≤ y → a y ≤ C * (↑y / ↑x) ^ (ρ + δ) * a x ∧ (↑y / ↑x) ^ (ρ - δ) * a x ≤ C * a y

Global Potter bounds: for every δ > 0 there is C > 0 such that for all 1 ≤ x ≤ y, a y ≤ C (y/x)^(ρ+δ) a x and (y/x)^(ρ-δ) a x ≤ C a y.