Monotone density theorem

If f ≥ 0 is antitone on (0, ∞) and U(x) = ∫₀ˣ f is regularly varying at infinity of index ρ, then x f(x) / U(x) → ρ. (The index ρ ∈ [0,1) of the application is not needed.) Ported from BGWLeaves/StableAnalysis/MonotoneDensity.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

def BGW.StableTrees.Attraction.MonotoneDensity.IsRegVaryAtTop (U : ℝ → ℝ) (ρ : ℝ) : Prop

U is regularly varying of index ρ at infinity.

Equations

• BGW.StableTrees.Attraction.MonotoneDensity.IsRegVaryAtTop U ρ = ∀ (c : ℝ), 0 < c → Filter.Tendsto (fun (x : ℝ) => U (c * x) / U x) Filter.atTop (nhds (c ^ ρ))

theorem BGW.StableTrees.Attraction.MonotoneDensity.monotone_density {f : ℝ → ℝ} (hnn : ∀ (x : ℝ), 0 < x → 0 ≤ f x) (hanti : AntitoneOn f (Set.Ioi 0)) {ρ : ℝ} (hU : IsRegVaryAtTop (fun (x : ℝ) => ∫ (t : ℝ) in 0..x, f t) ρ) : Filter.Tendsto (fun (x : ℝ) => x * f x / ∫ (t : ℝ) in 0..x, f t) Filter.atTop (nhds ρ)

theorem BGW.StableTrees.Attraction.MonotoneDensity.karamata_antitone {T : ℝ → ℝ} {θ : ℝ} (hT0 : ∀ (x : ℝ), 0 ≤ T x) (hanti : Antitone T) (hθ0 : 0 < θ) (hθ2 : θ < 2) (hT : IsRegVaryAtTop T (-θ)) : Filter.Tendsto (fun (x : ℝ) => (∫ (u : ℝ) in 0..x, u * T u) / (x ^ 2 * T x)) Filter.atTop (nhds (1 / (2 - θ)))

Karamata's theorem for an antitone nonnegative regularly varying function.

theorem BGW.StableTrees.Attraction.MonotoneDensity.layer_cake_trunc (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hneg : ν {z : ℤ | z < -1} = 0) {x : ℝ} (hx : 1 ≤ x) : 2 * ∫ (u : ℝ) in 0..x, u * ν.real {z : ℤ | u < ↑z} = truncSecondMoment ν x + x ^ 2 * ν.real {z : ℤ | x < ↑z} - ν.real {-1}

Layer-cake identity for the truncated second moment of a law on ℤ with ν {z < -1} = 0: 2 ∫₀ˣ u T(u) du = K(x) + x² T(x) - ν{-1} for x ≥ 1.

theorem BGW.StableTrees.Attraction.MonotoneDensity.truncSecondMoment_div_tendsto (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hneg : ν {z : ℤ | z < -1} = 0) {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : Filter.Tendsto (fun (x : ℝ) => truncSecondMoment ν x / (x ^ 2 * ν.real {z : ℤ | x < ↑z})) Filter.atTop (nhds (θ / (2 - θ)))

Truncated second moment under a regularly varying tail (1 < θ < 2; in fact the proof only uses 0 < θ < 2). If ν is a probability law on ℤ with ν {z < -1} = 0 whose right tail T(x) = ν {z > x} is regularly varying of index -θ, then K(x) ~ θ x² T(x) / (2 - θ).

theorem BGW.StableTrees.Attraction.MonotoneDensity.truncSecondMoment_isEquivalent (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hneg : ν {z : ℤ | z < -1} = 0) {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : Asymptotics.IsEquivalent Filter.atTop (truncSecondMoment ν) fun (x : ℝ) => θ / (2 - θ) * (x ^ 2 * ν.real {z : ℤ | x < ↑z})

Same statement in the form K(x) ~ θ x² T(x) / (2 - θ).