Truncated moments of regularly varying tails

TheoremAntitone bounded functions are interval integrable#✓fully proved

Antitone bounded functions are interval-integrable.

theorem intervalIntegrable_of_antitone_bdd {W : ℝ → ℝ} (hW : Antitone W)
    (hWnn : ∀ t, 0 ≤ W t) (hWbdd : ∃ B, ∀ t, W t ≤ B) {a b : ℝ} (hab : a ≤ b) :
    IntervalIntegrable W volume a b

Used by 1

Used byCorrected regularly-varying tail integral

TheoremLayer-cake formula for the first moment#✓fully proved

Layer-cake formula for the first moment on (0, a]: the integral of y over (0, a] equals the integral of the right tail minus the endpoint correction.

theorem layerCake_firstMoment {μ : Measure ℝ} [IsProbabilityMeasure μ] {a : ℝ} (ha : 0 ≤ a) :
    ∫ y in Set.Ioc 0 a, y ∂μ
      = ∫ t in (0:ℝ)..a, (rightTail μ t - rightTail μ a)

Uses 1 · Used by 1

Statement usesRight tail of a measure

Used byCorrected regularly-varying tail integral

TheoremCorrected regularly-varying tail integral#✓fully proved

For a probability measure μ on ℝ with regularly varying combined tail of index -α, 0 < α < 1, and tail balance p, the first-moment tail integral satisfies (∫ y in Ioc 0 (c * x), y ∂μ) / (x * combinedTail μ x) → p * α * c ^ (1 - α) / (1 - α).

theorem tailIntegral_tendsto {μ : Measure ℝ} [IsProbabilityMeasure μ] {α : ℝ}
    (hα : 0 < α) (hα1 : α < 1) {p : ℝ} (hTB : HasTailBalance μ p)
    (hRV : IsRegularlyVarying (combinedTail μ) (-α)) {c : ℝ} (hc : 0 < c) :
    Tendsto (fun x => (∫ y in Set.Ioc 0 (c * x), y ∂μ) / (x * combinedTail μ x))
      atTop (𝓝 (p * α * c ^ (1 - α) / (1 - α)))

Uses 13

Statement usesTail balance · Regularly varying function · Combined tail of a measure

Proof usesRegularly varying functions are eventually positive · Slowly varying function · The combined tail is antitone · The combined tail of a probability measure is at most two · Left tail of a measure · Right tail of a measure · The right tail of a finite measure is antitone · The right tail of a probability measure is at most one · Antitone bounded functions are interval integrable · Layer-cake formula for the first moment

DefinitionClosed upper tail of a measure#✓fully proved

The upper tail (μ {y | s ≤ |y|}).toReal.

noncomputable def tailGe (μ : Measure ℝ) (s : ℝ) : ℝ := (μ {y : ℝ | s ≤ |y|}).toReal

Used by 4

Used byLayer-cake formula for the truncated second moment · Non-strict absolute tail as combined tail plus endpoint atoms · Upper tail is asymptotic to the combined tail · Truncated second moment asymptotic for regularly varying tails

DefinitionStrict upper tail of a measure#✓fully proved

The lower tail (μ {y | s < |y|}).toReal.

noncomputable def tailGt (μ : Measure ℝ) (s : ℝ) : ℝ := (μ {y : ℝ | s < |y|}).toReal

Used by 5

Used byLayer-cake formula for the truncated second moment · Non-strict absolute tail as combined tail plus endpoint atoms · Strict absolute tail equals the combined tail · Lower tail is asymptotic to the combined tail · Truncated second moment asymptotic for regularly varying tails

TheoremStrict absolute tail equals the combined tail#✓fully proved

At nonnegative thresholds the strict absolute tail is the canonical combined tail.

theorem tailGt_eq_combinedTail (μ : Measure ℝ) [IsFiniteMeasure μ]
    {s : ℝ} (hs : 0 ≤ s) : tailGt μ s = combinedTail μ s

Uses 4 · Used by 2

Statement usesCombined tail of a measure · Strict upper tail of a measure

Proof usesLeft tail of a measure · Right tail of a measure

Used byNon-strict absolute tail as combined tail plus endpoint atoms · Lower tail is asymptotic to the combined tail

TheoremNon-strict absolute tail as combined tail plus endpoint atoms#✓fully proved

The non-strict absolute tail adds both endpoint atoms to the canonical strict tail.

theorem tailGe_eq_combinedTail_add_atoms (μ : Measure ℝ) [IsFiniteMeasure μ]
    {s : ℝ} (hs : 0 < s) :
    tailGe μ s = combinedTail μ s + (μ {s}).toReal + (μ {-s}).toReal

Uses 4 · Used by 1

Statement usesCombined tail of a measure · Closed upper tail of a measure

Proof usesStrict upper tail of a measure · Strict absolute tail equals the combined tail

Used byUpper tail is asymptotic to the combined tail

TheoremUpper tail is asymptotic to the combined tail#✓fully proved

The upper tail is asymptotically the combined tail.

theorem tailGe_ratio_tendsto {μ : Measure ℝ} [IsProbabilityMeasure μ] {α : ℝ}
    (hα : 0 < α) (hRV : IsRegularlyVarying (combinedTail μ) (-α)) :
    Tendsto (fun x => tailGe μ x / combinedTail μ x) atTop (𝓝 1)

Uses 10 · Used by 1

Statement usesRegularly varying function · Combined tail of a measure · Closed upper tail of a measure

Proof usesRegularly varying functions are eventually positive · Ratio limit of a regularly varying function · Left tail of a measure · Monotonicity of the left tail · Right tail of a measure · The right tail of a finite measure is antitone · Non-strict absolute tail as combined tail plus endpoint atoms

Used byTruncated second moment asymptotic for regularly varying tails

TheoremLower tail is asymptotic to the combined tail#✓fully proved

The lower tail is asymptotically the combined tail.

theorem tailGt_ratio_tendsto {μ : Measure ℝ} [IsProbabilityMeasure μ] {α : ℝ}
    (hRV : IsRegularlyVarying (combinedTail μ) (-α)) :
    Tendsto (fun x => tailGt μ x / combinedTail μ x) atTop (𝓝 1)

Uses 5 · Used by 1

Statement usesRegularly varying function · Combined tail of a measure · Strict upper tail of a measure

Proof usesRegularly varying functions are eventually positive · Strict absolute tail equals the combined tail

Used byTruncated second moment asymptotic for regularly varying tails

TheoremLayer-cake formula for the truncated second moment#✓fully proved

Layer-cake formula for the truncated second moment, in terms of the upper tail tailGe. The term x ^ 2 * tailGt μ x removes the contribution from points with |y| > x, which lie outside the closed truncation interval.

theorem layerCake {μ : Measure ℝ} [IsProbabilityMeasure μ] {x : ℝ} (hx : 0 ≤ x) :
    ∫ y in Set.Icc (-x) x, y ^ 2 ∂μ
      = 2 * (∫ t in (0:ℝ)..x, t * tailGe μ t) - x ^ 2 * tailGt μ x

Uses 2 · Used by 1

Statement usesClosed upper tail of a measure · Strict upper tail of a measure

Used byTruncated second moment asymptotic for regularly varying tails

TheoremTruncated second moment asymptotic for regularly varying tails#✓fully proved

The corrected truncated-second-moment asymptotic: for a probability measure on ℝ with regularly varying combined tail of index -α, 0 < α < 2, the ratio (∫ y in Icc (-x) x, y ^ 2 ∂μ) / (x ^ 2 * combinedTail μ x) tends to α / (2 - α).

Correction: v1/Atlas/TheoryOfProbability/code/RegularVariation.lean states this with the constant 2 / (2 - α), which is wrong; the Pareto tail gives α / (2 - α) (see the test file).

theorem truncatedMoment_tendsto {μ : Measure ℝ} [IsProbabilityMeasure μ] {α : ℝ}
    (hα : 0 < α) (hα2 : α < 2)
    (hRV : IsRegularlyVarying (combinedTail μ) (-α)) :
    Tendsto (fun x => (∫ y in Set.Icc (-x) x, y ^ 2 ∂μ) / (x ^ 2 * combinedTail μ x))
      atTop (𝓝 (α / (2 - α)))

Uses 10

Statement usesRegularly varying function · Combined tail of a measure

Proof usesRegularly varying functions are eventually positive · Ratio limit of a regularly varying function · Karamata's integral theorem · Layer-cake formula for the truncated second moment · Closed upper tail of a measure · Upper tail is asymptotic to the combined tail · Strict upper tail of a measure · Lower tail is asymptotic to the combined tail

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.