Inversion of a regularly varying integer tail

Let ν be a probability measure on ℤ and T(x) = ν.real {z | x < z}. If T is regularly varying of index -θ, θ > 0, then the tail quantile q_n = tailQuantile ν n satisfies q_n → ∞, n T(q_n) → 1; the multiplier quantile q^c_n = inf {x ≥ 0 | T x ≤ c / n} satisfies n T(q^c_n) → c and q^c_n / q_n → c ^ (-1/θ); and q_{⌊λ n⌋} / q_n → λ ^ (1/θ). Ported from BGWLeaves/StableAnalysis/QuantileInversion.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

structure BGW.StableTrees.Attraction.QuantileInversion.TailData (T : ℝ → ℝ) (θ : ℝ) : Prop

The properties of the tail function T used for the inversion.

• nonneg (x : ℝ) : 0 ≤ T x
• anti : Antitone T
• rc (x : ℝ) : ContinuousWithinAt T (Set.Ici x) x
• tendsto_nat : Filter.Tendsto (fun (n : ℕ) => T ↑n) Filter.atTop (nhds 0)
• theta_pos : 0 < θ
• rv : MonotoneDensity.IsRegVaryAtTop T (-θ)

noncomputable def BGW.StableTrees.Attraction.QuantileInversion.levelQuantile (T : ℝ → ℝ) (a : ℝ) : ℝ

Left-continuous inverse of T at level a.

Equations

• BGW.StableTrees.Attraction.QuantileInversion.levelQuantile T a = sInf {x : ℝ | 0 ≤ x ∧ T x ≤ a}

theorem BGW.StableTrees.Attraction.QuantileInversion.TailData.pos {T : ℝ → ℝ} {θ : ℝ} (h : TailData T θ) (x : ℝ) : 0 < T x

theorem BGW.StableTrees.Attraction.QuantileInversion.TailData.set_nonempty {T : ℝ → ℝ} {θ : ℝ} (h : TailData T θ) {a : ℝ} (ha : 0 < a) : {x : ℝ | 0 ≤ x ∧ T x ≤ a}.Nonempty

theorem BGW.StableTrees.Attraction.QuantileInversion.TailData.level_nonneg {T : ℝ → ℝ} {θ : ℝ} (h : TailData T θ) {a : ℝ} (ha : 0 < a) : 0 ≤ levelQuantile T a

theorem BGW.StableTrees.Attraction.QuantileInversion.TailData.tail_level_le {T : ℝ → ℝ} {θ : ℝ} (h : TailData T θ) {a : ℝ} (ha : 0 < a) : T (levelQuantile T a) ≤ a

theorem BGW.StableTrees.Attraction.QuantileInversion.lt_tail_of_lt_level {T : ℝ → ℝ} {a x : ℝ} (hx : 0 ≤ x) (hxQ : x < levelQuantile T a) : a < T x

theorem BGW.StableTrees.Attraction.QuantileInversion.TailData.level_tendsto_atTop {T : ℝ → ℝ} {θ : ℝ} (h : TailData T θ) : Filter.Tendsto (levelQuantile T) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

theorem BGW.StableTrees.Attraction.QuantileInversion.rpow_neg_lt_of_lt {x y θ : ℝ} (hx : 0 < x) (hxy : x < y) (hθ : 0 < θ) : y ^ (-θ) < x ^ (-θ)

theorem BGW.StableTrees.Attraction.QuantileInversion.TailData.level_ratio_tendsto {T : ℝ → ℝ} {θ : ℝ} (h : TailData T θ) : Filter.Tendsto (fun (a : ℝ) => T (levelQuantile T a) / a) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

theorem BGW.StableTrees.Attraction.QuantileInversion.TailData.ratio_tendsto {T : ℝ → ℝ} {θ : ℝ} (h : TailData T θ) {r s : ℕ → ℝ} (hs : Filter.Tendsto s Filter.atTop Filter.atTop) {c : ℝ} (hc : 0 < c) (hrs : Filter.Tendsto (fun (n : ℕ) => T (r n) / T (s n)) Filter.atTop (nhds c)) : Filter.Tendsto (fun (n : ℕ) => r n / s n) Filter.atTop (nhds (c ^ (-1 / θ)))

If T(r n) / T(s n) → c > 0 and s n → ∞, then r n / s n → c ^ (-1/θ).

theorem BGW.StableTrees.Attraction.QuantileInversion.TailData.level_seq {T : ℝ → ℝ} {θ : ℝ} (h : TailData T θ) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop (nhds 0)) (hpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < a n) : Filter.Tendsto (fun (n : ℕ) => levelQuantile T (a n)) Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => T (levelQuantile T (a n)) / a n) Filter.atTop (nhds 1)

theorem BGW.StableTrees.Attraction.QuantileInversion.TailData.level_mul_tail {T : ℝ → ℝ} {θ : ℝ} (h : TailData T θ) {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (n : ℕ) => ↑n * T (levelQuantile T (c / ↑n))) Filter.atTop (nhds c)

theorem BGW.StableTrees.Attraction.QuantileInversion.TailData.level_ratio_one {T : ℝ → ℝ} {θ : ℝ} (h : TailData T θ) {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (n : ℕ) => T (levelQuantile T (c / ↑n)) / T (levelQuantile T (1 / ↑n))) Filter.atTop (nhds c)

theorem BGW.StableTrees.Attraction.QuantileInversion.tailData_of_regVary (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ : 0 < θ) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : TailData (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) θ

noncomputable def BGW.StableTrees.Attraction.QuantileInversion.multQuantile (ν : MeasureTheory.Measure ℤ) (c : ℝ) (n : ℕ) : ℝ

Multiplier quantile inf {x ≥ 0 | P[W > x] ≤ c / n}.

Equations

• BGW.StableTrees.Attraction.QuantileInversion.multQuantile ν c n = sInf {x : ℝ | 0 ≤ x ∧ ν.real {z : ℤ | x < ↑z} ≤ c / ↑n}

theorem BGW.StableTrees.Attraction.QuantileInversion.tailQuantile_eq (ν : MeasureTheory.Measure ℤ) (n : ℕ) : tailQuantile ν n = levelQuantile (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (1 / ↑n)

theorem BGW.StableTrees.Attraction.QuantileInversion.multQuantile_eq (ν : MeasureTheory.Measure ℤ) (c : ℝ) (n : ℕ) : multQuantile ν c n = levelQuantile (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (c / ↑n)

theorem BGW.StableTrees.Attraction.QuantileInversion.tailQuantile_tendsto_atTop {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ : 0 < θ) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : Filter.Tendsto (fun (n : ℕ) => tailQuantile ν n) Filter.atTop Filter.atTop

(a) The tail quantile tends to infinity.

theorem BGW.StableTrees.Attraction.QuantileInversion.tailQuantile_mul_tail {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ : 0 < θ) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : Filter.Tendsto (fun (n : ℕ) => ↑n * ν.real {z : ℤ | tailQuantile ν n < ↑z}) Filter.atTop (nhds 1)

(b) n * T(q_n) → 1.

theorem BGW.StableTrees.Attraction.QuantileInversion.multQuantile_tendsto_atTop {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ : 0 < θ) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (n : ℕ) => multQuantile ν c n) Filter.atTop Filter.atTop

(c) The multiplier quantile tends to infinity.

theorem BGW.StableTrees.Attraction.QuantileInversion.multQuantile_mul_tail {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ : 0 < θ) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (n : ℕ) => ↑n * ν.real {z : ℤ | multQuantile ν c n < ↑z}) Filter.atTop (nhds c)

(c) n * T(q^c_n) → c.

theorem BGW.StableTrees.Attraction.QuantileInversion.multQuantile_div_tailQuantile {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ : 0 < θ) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (n : ℕ) => multQuantile ν c n / tailQuantile ν n) Filter.atTop (nhds (c ^ (-1 / θ)))

(c) q^c_n / q_n → c ^ (-1/θ).

theorem BGW.StableTrees.Attraction.QuantileInversion.tailQuantile_floor_div_tailQuantile {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ : 0 < θ) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) {l : ℝ} (hl : 0 < l) : Filter.Tendsto (fun (n : ℕ) => tailQuantile ν ⌊l * ↑n⌋₊ / tailQuantile ν n) Filter.atTop (nhds (l ^ (1 / θ)))

(d) q_{⌊λ n⌋} / q_n → λ ^ (1/θ).