Two-sided quantitative bounds for positive-discount scale deviations from zero discount

Proved

AvramDividend.Classical.unbounded_scale_discount_zero_reference_two_sided_bounds

by WillR · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

avram-classicaldiscountquantitative-boundscale-functionzero-discount

For unbounded variation, the variation in scale function from undiscounted q=0 to any positive discount q≤Q is bounded below by q times self-convolution of W0 and above by q times self-convolution of WQ, pointwise on every positive reserve.

Preamble

import Theorems.Thm_AvramDividend_Classical_unbounded_scale_discount_two_sided_linear_bounds
open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.unbounded_scale_discount_zero_reference_two_sided_bounds
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (hnbv : ¬ X.BoundedVariation)
    (q Q : ℝ) (hq : 0 < q) (hqQ : q ≤ Q)
    (W₀ Wq WQ : ℝ → ℝ)
    (hW₀ : IsScaleFunction X 0 W₀)
    (hWq : IsScaleFunction X q Wq)
    (hWQ : IsScaleFunction X Q WQ) :
    ∀ x : ℝ, 0 < x →
      q * (∫ s in Ioc (0 : ℝ) x, W₀ s * W₀ (x - s)) ≤
        Wq x - W₀ x ∧
      Wq x - W₀ x ≤ q *
        (∫ s in Ioc (0 : ℝ) x, WQ s * WQ (x - s)) := by sorry

Source

The already-Proved general two-sided discount secant estimate, specialised to a zero lower discount endpoint.

View graph