Regular variation

DefinitionSlowly varying function#✓fully proved

A function \(L : \mathbb{R} \to \mathbb{R}\) is slowly varying (at infinity) if \(L(x) > 0\) for all sufficiently large \(x\) and, for every real \(c > 0\), \(L(cx) / L(x) \to 1\) as \(x \to \infty\).

def IsSlowlyVarying (L : ℝ → ℝ) : Prop :=
  (∀ᶠ x in atTop, 0 < L x) ∧
  ∀ c : ℝ, 0 < c → Tendsto (fun x => L (c * x) / L x) atTop (𝓝 1)
Used by 16
Used byPositive multiples of slowly varying functions · Positive multiples of regularly varying functions · Regularly varying functions are eventually positive · Regularly varying function · Powers are regularly varying · Positive constants are slowly varying · The constant function one is slowly varying · The function \(1 + (1 + x)^{-1}\) is slowly varying · Products of slowly varying functions · Products of regularly varying functions · Slow variation is preserved by eventual equality · Regular variation is preserved by eventual equality · Functions with a positive limit are slowly varying · Ratio limit of a regularly varying function · Generalized inverse of a regularly varying function · Corrected regularly-varying tail integral

TheoremFunctions with a positive limit are slowly varying#✓fully proved

Let \(L : \mathbb{R} \to \mathbb{R}\) and \(a > 0\). If \(L(x) > 0\) for all sufficiently large \(x\) and \(L(x) \to a\) as \(x \to \infty\), then \(L\) is slowly varying.

Indeed, for every \(c > 0\) the ratio \(L(cx) / L(x)\) tends to \(a / a = 1\).

theorem IsSlowlyVarying.of_tendsto {L : ℝ → ℝ} {a : ℝ}
    (hpos : ∀ᶠ x in atTop, 0 < L x) (hlim : Tendsto L atTop (𝓝 a)) (ha : 0 < a) :
    IsSlowlyVarying L
Uses 1 · Used by 1
Statement usesSlowly varying function
Used byThe function \(1 + (1 + x)^{-1}\) is slowly varying

TheoremThe constant function one is slowly varying#✓fully proved

The constant function \(x \mapsto 1\) on \(\mathbb{R}\) is slowly varying.

theorem isSlowlyVarying_one : IsSlowlyVarying (fun _ => (1 : ℝ))
Uses 1 · Used by 1
Statement usesSlowly varying function
Used byPowers are regularly varying

TheoremPositive constants are slowly varying#✓fully proved

For every real \(c > 0\), the constant function \(x \mapsto c\) on \(\mathbb{R}\) is slowly varying.

theorem isSlowlyVarying_const {c : ℝ} (hc : 0 < c) : IsSlowlyVarying (fun _ => c)
Uses 1
Statement usesSlowly varying function

TheoremProducts of slowly varying functions#✓fully proved

If \(L_1, L_2 : \mathbb{R} \to \mathbb{R}\) are slowly varying, then so is their pointwise product \(x \mapsto L_1(x) L_2(x)\).

theorem IsSlowlyVarying.mul {L₁ L₂ : ℝ → ℝ}
    (h₁ : IsSlowlyVarying L₁) (h₂ : IsSlowlyVarying L₂) :
    IsSlowlyVarying (fun x => L₁ x * L₂ x)
Uses 1 · Used by 1
Statement usesSlowly varying function
Used byProducts of regularly varying functions

TheoremPositive multiples of slowly varying functions#✓fully proved

If \(L : \mathbb{R} \to \mathbb{R}\) is slowly varying and \(c > 0\), then \(x \mapsto c L(x)\) is slowly varying.

theorem IsSlowlyVarying.const_mul {L : ℝ → ℝ} (hL : IsSlowlyVarying L) {c : ℝ}
    (hc : 0 < c) : IsSlowlyVarying (fun x => c * L x)
Uses 1 · Used by 1
Statement usesSlowly varying function
Used byPositive multiples of regularly varying functions

TheoremThe function \(1 + (1 + x)^{-1}\) is slowly varying#✓fully proved

The function \(x \mapsto 1 + (1 + x)^{-1}\) on \(\mathbb{R}\) is slowly varying; it tends to the positive limit \(1\) at infinity.

theorem isSlowlyVarying_one_add_inv :
    IsSlowlyVarying (fun x : ℝ => 1 + (1 + x)⁻¹)
Uses 2
Statement usesSlowly varying function
Proof usesFunctions with a positive limit are slowly varying

TheoremSlow variation is preserved by eventual equality#✓fully proved

Let \(f, g : \mathbb{R} \to \mathbb{R}\). If \(f\) is slowly varying and \(f(x) = g(x)\) for all sufficiently large \(x\), then \(g\) is slowly varying.

theorem IsSlowlyVarying.of_eventuallyEq {f g : ℝ → ℝ}
    (hf : IsSlowlyVarying f) (hfg : f =ᶠ[atTop] g) : IsSlowlyVarying g
Uses 1
Statement usesSlowly varying function

DefinitionRegularly varying function#✓fully proved

A function \(f : \mathbb{R} \to \mathbb{R}\) is regularly varying with index \(\rho \in \mathbb{R}\) if there is a slowly varying function \(L : \mathbb{R} \to \mathbb{R}\) such that \(f(x) = x^{\rho} L(x)\) for all sufficiently large \(x\).

def IsRegularlyVarying (f : ℝ → ℝ) (ρ : ℝ) : Prop :=
  ∃ L : ℝ → ℝ, IsSlowlyVarying L ∧ ∀ᶠ x in atTop, f x = x ^ ρ * L x
Uses 1 · Used by 12
Statement usesSlowly varying function
Used byPositive multiples of regularly varying functions · Regularly varying functions are eventually positive · Positive multiples of powers are regularly varying · Powers are regularly varying · Products of regularly varying functions · Regular variation is preserved by eventual equality · Ratio limit of a regularly varying function · Generalized inverse of a regularly varying function · Upper tail is asymptotic to the combined tail · Lower tail is asymptotic to the combined tail · Corrected regularly-varying tail integral · Truncated second moment asymptotic for regularly varying tails

TheoremPowers are regularly varying#✓fully proved

For every real number \(\rho\), the function \(x \mapsto x^\rho\) on \(\mathbb{R}\) is regularly varying with index \(\rho\).

The slowly varying factor can be taken to be the constant function \(1\).

theorem isRegularlyVarying_rpow (ρ : ℝ) :
    IsRegularlyVarying (fun x : ℝ => x ^ ρ) ρ
Uses 3 · Used by 1
Statement usesRegularly varying function
Proof usesSlowly varying function · The constant function one is slowly varying
Used byPositive multiples of powers are regularly varying

TheoremProducts of regularly varying functions#✓fully proved

If \(f : \mathbb{R} \to \mathbb{R}\) is regularly varying with index \(\rho\) and \(g : \mathbb{R} \to \mathbb{R}\) is regularly varying with index \(\sigma\), then the pointwise product \(fg\) is regularly varying with index \(\rho + \sigma\).

theorem IsRegularlyVarying.mul {f g : ℝ → ℝ} {ρ σ : ℝ}
    (hf : IsRegularlyVarying f ρ) (hg : IsRegularlyVarying g σ) :
    IsRegularlyVarying (f * g) (ρ + σ)
Uses 3
Statement usesRegularly varying function
Proof usesSlowly varying function · Products of slowly varying functions

TheoremPositive multiples of regularly varying functions#✓fully proved

If \(f : \mathbb{R} \to \mathbb{R}\) is regularly varying with index \(\rho\) and \(c > 0\), then \(x \mapsto c f(x)\) is regularly varying with index \(\rho\).

theorem IsRegularlyVarying.const_mul {f : ℝ → ℝ} {ρ : ℝ}
    (hf : IsRegularlyVarying f ρ) {c : ℝ} (hc : 0 < c) :
    IsRegularlyVarying (fun x => c * f x) ρ
Uses 3 · Used by 1
Statement usesRegularly varying function
Proof usesSlowly varying function · Positive multiples of slowly varying functions
Used byPositive multiples of powers are regularly varying

TheoremPositive multiples of powers are regularly varying#✓fully proved

For real numbers \(c > 0\) and \(\rho\), the function \(x \mapsto c x^\rho\) on \(\mathbb{R}\) is regularly varying with index \(\rho\).

theorem isRegularlyVarying_const_mul_rpow {c ρ : ℝ} (hc : 0 < c) :
    IsRegularlyVarying (fun x : ℝ => c * x ^ ρ) ρ
Uses 3
Statement usesRegularly varying function
Proof usesPositive multiples of regularly varying functions · Powers are regularly varying

TheoremRegular variation is preserved by eventual equality#✓fully proved

Let \(f, g : \mathbb{R} \to \mathbb{R}\) and \(\rho \in \mathbb{R}\). If \(f\) is regularly varying with index \(\rho\) and \(f(x) = g(x)\) for all sufficiently large \(x\), then \(g\) is regularly varying with index \(\rho\).

theorem IsRegularlyVarying.of_eventuallyEq {f g : ℝ → ℝ} {ρ : ℝ}
    (hf : IsRegularlyVarying f ρ) (hfg : f =ᶠ[atTop] g) :
    IsRegularlyVarying g ρ
Uses 2
Statement usesRegularly varying function
Proof usesSlowly varying function

TheoremRegularly varying functions are eventually positive#✓fully proved

If \(f : \mathbb{R} \to \mathbb{R}\) is regularly varying with some index \(\rho\), then \(f(x) > 0\) for all sufficiently large \(x\).

theorem IsRegularlyVarying.eventually_pos {f : ℝ → ℝ} {ρ : ℝ}
    (hf : IsRegularlyVarying f ρ) : ∀ᶠ x in atTop, 0 < f x
Uses 2 · Used by 4
Statement usesRegularly varying function
Proof usesSlowly varying function
Used byUpper tail is asymptotic to the combined tail · Lower tail is asymptotic to the combined tail · Corrected regularly-varying tail integral · Truncated second moment asymptotic for regularly varying tails

DefinitionRight tail of a measure#✓fully proved

For a measure \(\mu\) on \(\mathbb{R}\) and \(x \in \mathbb{R}\), the right tail of \(\mu\) at \(x\) is the real number \(\mu((x, \infty))\) when \(\mu((x, \infty)) < \infty\), and \(0\) when \(\mu((x, \infty)) = \infty\).

For a finite measure \(\mu\) it is the mass of the open half-line \((x, \infty)\).

def rightTail (μ : Measure ℝ) (x : ℝ) : ℝ := (μ (Set.Ioi x)).toReal
Used by 17
Used byCombined tail of a measure · The combined tail is antitone · The combined tail of a probability measure is at most two · Tail balance · Tail balance zero from a vanishing right tail · The left tail is at most the combined tail · Dirac masses have no tail balance · Eventually vanishing combined tail rules out tail balance · The right tail of a finite measure is antitone · The right tail is at most the combined tail · The right tail of a probability measure is at most one · The combined tail of a finite measure vanishes at infinity · The right tail of a finite measure vanishes at infinity · Layer-cake formula for the first moment · Upper tail is asymptotic to the combined tail · Strict absolute tail equals the combined tail · Corrected regularly-varying tail integral

DefinitionLeft tail of a measure#✓fully proved

For a measure \(\mu\) on \(\mathbb{R}\) and a real \(x\), the left tail of \(\mu\) at \(x\) is the real number \(\mu((-\infty, -x))\), where an infinite value is sent to \(0\).

For a finite measure it is the mass of the strict left tail \((-\infty, -x)\).

def leftTail (μ : Measure ℝ) (x : ℝ) : ℝ := (μ (Set.Iio (-x))).toReal
Used by 13
Used byCombined tail of a measure · The combined tail is antitone · The combined tail of a probability measure is at most two · Monotonicity of the left tail · The left tail is at most the combined tail · The left tail of a probability measure is at most one · Dirac masses have no tail balance · The right tail is at most the combined tail · The combined tail of a finite measure vanishes at infinity · The left tail of a finite measure vanishes at infinity · Upper tail is asymptotic to the combined tail · Strict absolute tail equals the combined tail · Corrected regularly-varying tail integral

DefinitionCombined tail of a measure#✓fully proved

For a measure \(\mu\) on \(\mathbb{R}\) and a real number \(x\), the combined tail of \(\mu\) at \(x\) is the real number \(\mu((x, \infty)) + \mu((-\infty, -x))\), where each of the two measures is converted from \([0, \infty]\) to a real number, an infinite value becoming \(0\).

For a finite measure and \(x \ge 0\) this equals \(\mu(\{y : |y| > x\})\). At negative thresholds the two intervals can overlap, so the combined tail is not the mass of the absolute tail.

def combinedTail (μ : Measure ℝ) (x : ℝ) : ℝ := rightTail μ x + leftTail μ x
Uses 2 · Used by 15
Statement usesLeft tail of a measure · Right tail of a measure
Used byThe combined tail is antitone · The combined tail of a probability measure is at most two · Tail balance · Tail balance zero from a vanishing right tail · The left tail is at most the combined tail · Dirac masses have no tail balance · Eventually vanishing combined tail rules out tail balance · The right tail is at most the combined tail · The combined tail of a finite measure vanishes at infinity · Non-strict absolute tail as combined tail plus endpoint atoms · Upper tail is asymptotic to the combined tail · Strict absolute tail equals the combined tail · Lower tail is asymptotic to the combined tail · Corrected regularly-varying tail integral · Truncated second moment asymptotic for regularly varying tails

TheoremThe right tail of a probability measure is at most one#✓fully proved

For every probability measure \(\mu\) on \(\mathbb{R}\) and every \(x \in \mathbb{R}\), the right tail of \(\mu\) at \(x\) is at most \(1\).

theorem rightTail_le_one (μ : Measure ℝ) [IsProbabilityMeasure μ] (x : ℝ) :
    rightTail μ x ≤ 1
Uses 1 · Used by 2
Statement usesRight tail of a measure
Used byThe combined tail of a probability measure is at most two · Corrected regularly-varying tail integral

TheoremThe left tail of a probability measure is at most one#✓fully proved

For every probability measure \(\mu\) on \(\mathbb{R}\) and every real \(x\), the left tail of \(\mu\) at \(x\) is at most \(1\).

theorem leftTail_le_one (μ : Measure ℝ) [IsProbabilityMeasure μ] (x : ℝ) :
    leftTail μ x ≤ 1
Uses 1 · Used by 1
Statement usesLeft tail of a measure
Used byThe combined tail of a probability measure is at most two

TheoremThe combined tail of a probability measure is at most two#✓fully proved

For every probability measure \(\mu\) on \(\mathbb{R}\) and every real number \(x\), the combined tail of \(\mu\) at \(x\) satisfies \(\mu((x, \infty)) + \mu((-\infty, -x)) \le 2\).

theorem combinedTail_le_two (μ : Measure ℝ) [IsProbabilityMeasure μ] (x : ℝ) :
    combinedTail μ x ≤ 2
Uses 5 · Used by 1
Statement usesCombined tail of a measure
Proof usesLeft tail of a measure · The left tail of a probability measure is at most one · Right tail of a measure · The right tail of a probability measure is at most one
Used byCorrected regularly-varying tail integral

TheoremThe right tail of a finite measure is antitone#✓fully proved

Let \(\mu\) be a finite measure on \(\mathbb{R}\). If \(x \le y\), then the right tail of \(\mu\) at \(y\) is at most the right tail of \(\mu\) at \(x\).

theorem rightTail_antitone (μ : Measure ℝ) [IsFiniteMeasure μ] :
    Antitone (rightTail μ)
Uses 1 · Used by 4
Statement usesRight tail of a measure
Used byThe combined tail is antitone · The right tail of a finite measure vanishes at infinity · Upper tail is asymptotic to the combined tail · Corrected regularly-varying tail integral

TheoremMonotonicity of the left tail#✓fully proved

For every finite measure \(\mu\) on \(\mathbb{R}\), the left tail of \(\mu\) is antitone in the threshold: if \(a \le b\), then \(\mu((-\infty, -b)) \le \mu((-\infty, -a))\).

theorem leftTail_antitone (μ : Measure ℝ) [IsFiniteMeasure μ] :
    Antitone (leftTail μ)
Uses 1 · Used by 3
Statement usesLeft tail of a measure
Used byThe combined tail is antitone · The left tail of a finite measure vanishes at infinity · Upper tail is asymptotic to the combined tail

TheoremThe combined tail is antitone#✓fully proved

Let \(\mu\) be a finite measure on \(\mathbb{R}\) and write \(T(x) = \mu((x, \infty)) + \mu((-\infty, -x))\) for its combined tail at a real number \(x\). Then \(T\) is antitone: \(T(b) \le T(a)\) whenever \(a \le b\).

theorem combinedTail_antitone (μ : Measure ℝ) [IsFiniteMeasure μ] :
    Antitone (combinedTail μ)
Uses 5 · Used by 1
Statement usesCombined tail of a measure
Proof usesLeft tail of a measure · Monotonicity of the left tail · Right tail of a measure · The right tail of a finite measure is antitone
Used byCorrected regularly-varying tail integral

TheoremThe right tail is at most the combined tail#✓fully proved

For every measure \(\mu\) on \(\mathbb{R}\) and every \(x \in \mathbb{R}\), the right tail of \(\mu\) at \(x\) is at most the combined tail of \(\mu\) at \(x\).

theorem rightTail_le_combinedTail (μ : Measure ℝ) (x : ℝ) :
    rightTail μ x ≤ combinedTail μ x
Uses 3
Statement usesCombined tail of a measure · Right tail of a measure
Proof usesLeft tail of a measure

TheoremThe left tail is at most the combined tail#✓fully proved

For every measure \(\mu\) on \(\mathbb{R}\) and every real \(x\), the left tail of \(\mu\) at \(x\) is at most the combined tail of \(\mu\) at \(x\).

theorem leftTail_le_combinedTail (μ : Measure ℝ) (x : ℝ) :
    leftTail μ x ≤ combinedTail μ x
Uses 3
Statement usesCombined tail of a measure · Left tail of a measure
Proof usesRight tail of a measure

TheoremThe right tail of a finite measure vanishes at infinity#✓fully proved

For every finite measure \(\mu\) on \(\mathbb{R}\), the right tail \(\mu((x, \infty))\), taken as a real number, tends to \(0\) as \(x \to \infty\).

theorem tendsto_rightTail_atTop (μ : Measure ℝ) [IsFiniteMeasure μ] :
    Tendsto (rightTail μ) atTop (𝓝 0)
Uses 2 · Used by 1
Statement usesRight tail of a measure
Proof usesThe right tail of a finite measure is antitone
Used byThe combined tail of a finite measure vanishes at infinity

TheoremThe left tail of a finite measure vanishes at infinity#✓fully proved

For every finite measure \(\mu\) on \(\mathbb{R}\), the left tail \(\mu((-\infty, -x))\), taken as a real number, tends to \(0\) as \(x \to \infty\).

theorem tendsto_leftTail_atTop (μ : Measure ℝ) [IsFiniteMeasure μ] :
    Tendsto (leftTail μ) atTop (𝓝 0)
Uses 2 · Used by 1
Statement usesLeft tail of a measure
Proof usesMonotonicity of the left tail
Used byThe combined tail of a finite measure vanishes at infinity

TheoremThe combined tail of a finite measure vanishes at infinity#✓fully proved

For every finite measure \(\mu\) on \(\mathbb{R}\), the combined tail \(\mu((x, \infty)) + \mu((-\infty, -x))\), with both masses taken as real numbers, tends to \(0\) as \(x \to \infty\).

theorem tendsto_combinedTail_atTop (μ : Measure ℝ) [IsFiniteMeasure μ] :
    Tendsto (combinedTail μ) atTop (𝓝 0)
Uses 5
Statement usesCombined tail of a measure
Proof usesLeft tail of a measure · Right tail of a measure · The left tail of a finite measure vanishes at infinity · The right tail of a finite measure vanishes at infinity

DefinitionTail balance#✓fully proved

Let \(\mu\) be a finite measure on \(\mathbb{R}\) and \(p\) a real number. Write \(R(x) = \mu((x, \infty))\) for the right tail and \(T(x) = \mu((x, \infty)) + \mu((-\infty, -x))\) for the combined tail of \(\mu\). The measure \(\mu\) has tail balance \(p\) when \(0 \le p \le 1\), \(T(x) > 0\) for all sufficiently large \(x\), and \(R(x) / T(x) \to p\) as \(x \to \infty\).

For the law of a random variable \(X\) this says \(P(X > x) / P(|X| > x) \to p\). Eventual positivity of \(T\) rules out an eventual \(0 / 0\).

def HasTailBalance (μ : Measure ℝ) [IsFiniteMeasure μ] (p : ℝ) : Prop :=
  0 ≤ p ∧ p ≤ 1 ∧
  (∀ᶠ x in atTop, 0 < combinedTail μ x) ∧
  Tendsto (fun x => rightTail μ x / combinedTail μ x) atTop (𝓝 p)
Uses 2 · Used by 4
Statement usesCombined tail of a measure · Right tail of a measure
Used byTail balance zero from a vanishing right tail · Dirac masses have no tail balance · Eventually vanishing combined tail rules out tail balance · Corrected regularly-varying tail integral

TheoremTail balance zero from a vanishing right tail#✓fully proved

Let \(\mu\) be a finite measure on \(\mathbb{R}\). If \(\mu((x, \infty)) = 0\) for all sufficiently large \(x\) and the combined tail \(\mu((x, \infty)) + \mu((-\infty, -x))\) is positive for all sufficiently large \(x\), then \(\mu\) has tail balance \(0\).

theorem hasTailBalance_zero_of_eventually_rightTail_eq_zero (μ : Measure ℝ) [IsFiniteMeasure μ]
    (h : ∀ᶠ x in atTop, rightTail μ x = 0)
    (hdenom : ∀ᶠ x in atTop, 0 < combinedTail μ x) : HasTailBalance μ 0
Uses 3
Statement usesTail balance · Combined tail of a measure · Right tail of a measure

TheoremEventually vanishing combined tail rules out tail balance#✓fully proved

Let \(\mu\) be a finite measure on \(\mathbb{R}\) and let \(p \in \mathbb{R}\). If the combined tail of \(\mu\) at \(x\) equals \(0\) for all sufficiently large \(x\), then \(\mu\) does not have tail balance \(p\).

theorem not_hasTailBalance_of_eventually_combinedTail_eq_zero (μ : Measure ℝ) [IsFiniteMeasure μ]
    (p : ℝ)
    (hzero : ∀ᶠ x in atTop, combinedTail μ x = 0) : ¬ HasTailBalance μ p
Uses 3 · Used by 1
Statement usesTail balance · Combined tail of a measure
Proof usesRight tail of a measure
Used byDirac masses have no tail balance

TheoremDirac masses have no tail balance#✓fully proved

For every \(a \in \mathbb{R}\) and every \(p \in \mathbb{R}\), the Dirac measure \(\delta_a\) at \(a\) does not have tail balance \(p\).

The combined tail of \(\delta_a\) vanishes at every threshold \(x \ge |a|\), so the eventual positivity required by tail balance fails.

theorem not_hasTailBalance_dirac (a p : ℝ) : ¬ HasTailBalance (Measure.dirac a) p
Uses 5
Statement usesTail balance
Proof usesCombined tail of a measure · Left tail of a measure · Eventually vanishing combined tail rules out tail balance · Right tail of a measure

TheoremGeneralized inverse of a regularly varying function#✓fully proved

For a regularly varying function f of index -α with α > 0 that is eventually non-increasing, there exists a sequence a : ℕ → ℝ of positive reals such that n · f (a n) → 1 as n → ∞.

theorem regularlyVarying_generalized_inverse (f : ℝ → ℝ) (α : ℝ)
    (hα : 0 < α)
    (hf : IsRegularlyVarying f (-α))
    (hdecr : ∀ᶠ x in atTop, ∀ y, x ≤ y → f y ≤ f x) :
    ∃ a : ℕ → ℝ, (∀ n, 0 < a n) ∧
      Tendsto (fun n => ↑n * f (a n)) atTop (𝓝 1)
Uses 2
Statement usesRegularly varying function
Proof usesSlowly varying function

TheoremRatio limit of a regularly varying function#✓fully proved

A regularly varying function has the expected ratio limit.

theorem IsRegularlyVarying.ratio_tendsto {T : ℝ → ℝ} {ρ : ℝ}
    (hT : IsRegularlyVarying T ρ) {c : ℝ} (hc : 0 < c) :
    Tendsto (fun x => T (c * x) / T x) atTop (𝓝 (c ^ ρ))
Uses 2 · Used by 2
Statement usesRegularly varying function
Proof usesSlowly varying function
Used byUpper tail is asymptotic to the combined tail · Truncated second moment asymptotic for regularly varying tails

TheoremPotter's bound#✓fully proved

Potter's bound for antitone functions with a ratio limit. If W is antitone, bounded, eventually positive and W (c * x) / W x → c ^ ρ for every c > 0, then for every δ > 0 there are C > 0 and Y such that W (x * u) / W x ≤ C * u ^ (ρ - δ) for all x ≥ Y and u ∈ (0, 1]. The proof chains the ratio limit at the dyadic scales 1/2 and 2.

theorem potter_upper {W : ℝ → ℝ} {ρ : ℝ}
    (hW : Antitone W) (hWnn : ∀ t, 0 ≤ W t) (hWb : ∃ B, ∀ t, W t ≤ B)
    (hpos : ∀ᶠ x in atTop, 0 < W x)
    (hratio : ∀ c : ℝ, 0 < c → Tendsto (fun x => W (c * x) / W x) atTop (𝓝 (c ^ ρ)))
    (hρ : ρ < 0) {δ : ℝ} (hδ : 0 < δ) :
    ∃ C : ℝ, ∃ Y : ℝ, 0 < C ∧ 0 < Y ∧ ∀ x ≥ Y, ∀ u ∈ Set.Ioc 0 1,
      W (x * u) / W x ≤ C * u ^ (ρ - δ)
Used by 1
Used byKaramata's integral theorem

TheoremKaramata's integral theorem#✓fully proved

Karamata's integral theorem for antitone functions with a ratio limit. If W is antitone, nonnegative, bounded, eventually positive and W (c * x) / W x → c ^ ρ for every c > 0, then for β ≥ 0 and β + 1 + ρ > 0, (∫ t in (0)..x, t ^ β * W t) / (x ^ (β + 1) * W x) → 1 / (β + 1 + ρ). The proof substitutes t = x * u and applies dominated convergence with Potter's bound as the dominator.

theorem karamata_integral {W : ℝ → ℝ} {ρ β : ℝ}
    (hW : Antitone W) (hWnn : ∀ t, 0 ≤ W t) (hWb : ∃ B, ∀ t, W t ≤ B)
    (hpos : ∀ᶠ x in atTop, 0 < W x)
    (hratio : ∀ c : ℝ, 0 < c → Tendsto (fun x => W (c * x) / W x) atTop (𝓝 (c ^ ρ)))
    (hρ : ρ < 0) (hβ : 0 ≤ β) (hβρ : 0 < β + 1 + ρ) :
    Tendsto (fun x => (∫ t in (0:ℝ)..x, t ^ β * W t) / (x ^ (β + 1) * W x))
      atTop (𝓝 (1 / (β + 1 + ρ)))
Uses 1 · Used by 1
Proof usesPotter's bound
Used byTruncated second moment asymptotic for regularly varying tails
37 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.