Regularly varying sequences #
Source lines 846–853: the normalizing sequence (a_n) is increasing and regularly varying of
index 1/α, i.e. a_n / n^{1/α} is slowly varying. This directory is a pure real-analysis
toolbox about a monotone sequence a : ℕ → ℝ, positive at every n ≥ 1, that is regularly
varying of an index ρ (for the paper ρ = 1/α ∈ [1/2, 1)).
The sequential form of regular variation used here is
a ⌊c n⌋ / a n → c ^ ρ for every c > 0.
The bridge from the paper's formulation (x ↦ a_{⌊x⌋} / x^ρ is slowly varying in the sense of
PoissonDeclumping.SlowlyVarying) is PoissonDeclumping.RegularlyVaryingSeq.of_slowlyVarying
in PoissonDeclumping.RegularVariation.Bridge.
A real sequence a is regularly varying of index ρ (sequential form):
a ⌊c n⌋₊ / a n → c ^ ρ as n → ∞, for every c > 0.
Equations
- PoissonDeclumping.RegularlyVaryingSeq ρ a = ∀ (c : ℝ), 0 < c → Filter.Tendsto (fun (n : ℕ) => a ⌊c * ↑n⌋₊ / a n) Filter.atTop (nhds (c ^ ρ))