theorem ProbabilityTheory.regularlyVarying_generalized_inverse (f : ℝ → ℝ) (α : ℝ) (hα : 0 < α) (hf : IsRegularlyVarying f (-α)) (hdecr : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (y : ℝ), x ≤ y → f y ≤ f x) : ∃ (a : ℕ → ℝ), (∀ (n : ℕ), 0 < a n) ∧ Filter.Tendsto (fun (n : ℕ) => ↑n * f (a n)) Filter.atTop (nhds 1)

For a regularly varying function f of index -α with α > 0 that is eventually non-increasing, there exists a sequence a : ℕ → ℝ of positive reals (a "generalized inverse") such that n · f (a n) → 1 as n → ∞. This is a standard tool in the analysis of domains of attraction for stable laws.

theorem ProbabilityTheory.regularlyVarying_truncated_moment (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (α : ℝ) (hα₁ : 0 < α) (hα₂ : α < 2) (hRV : IsRegularlyVarying (combinedTail μ) (-α)) : Filter.Tendsto (fun (x : ℝ) => (∫ (y : ℝ) in Set.Icc (-x) x, y ^ 2 ∂μ) / (x ^ 2 * combinedTail μ x)) Filter.atTop (nhds (2 / (2 - α)))

Asymptotic for the truncated second moment of a distribution with regularly varying tails of index -α, 0 < α < 2. The ratio of ∫_{[-x, x]} y² dμ to x² · P(|X| > x) tends to 2 / (2 - α) as x → ∞. This is a key estimate in the proof of the convergence to stable laws.

theorem ProbabilityTheory.regularlyVarying_tail_integral (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (α : ℝ) (hα₁ : 0 < α) (hα₂ : α < 2) (hα_ne_1 : α ≠ 1) (p : ℝ) (hTB : HasTailBalance μ p) (hRV : IsRegularlyVarying (combinedTail μ) (-α)) (c : ℝ) (hc : 0 < c) : Filter.Tendsto (fun (x : ℝ) => (∫ (y : ℝ) in Set.Ioc 0 (c * x), y ∂μ) / (x * combinedTail μ x)) Filter.atTop (nhds (p * α * c ^ (1 - α) / (1 - α)))

Asymptotic for the integral ∫_{(0, c·x]} y dμ of a distribution with regularly varying tails of index -α, balanced with parameter p, normalized by x · P(|X| > x). The limit equals p · α · c^{1-α} / (1 - α), used in establishing domains of attraction to stable laws when α ≠ 1.