Uniform Lipschitz bound of q-scale functions on compact discount intervals

Proved

AvramDividend.Classical.unbounded_scale_discount_family_lipschitz_bound

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

avram-classicalcontinuitydiscountlipschitzscale-functionsensitivity

Let W_q be any scale-function family for an unbounded-variation spectrally negative Lévy process, indexed by all nonnegative discounts up to Q. For every fixed positive reserve, its dependence on q satisfies a two-sided global Lipschitz bound on [0,Q], with constant given by the Q-scale self-convolution. In particular the family is continuous with respect to discount.

Preamble

import Mathlib.Tactic.Linarith
import Theorems.Thm_AvramDividend_Classical_unbounded_scale_discount_uniform_secant_bound
open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.unbounded_scale_discount_family_lipschitz_bound
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (hnbv : ¬ X.BoundedVariation)
    (Q : ℝ) (hQ : 0 ≤ Q)
    (W : ℝ → ℝ → ℝ)
    (hW : ∀ q ∈ Icc (0 : ℝ) Q, IsScaleFunction X q (W q))
    (x : ℝ) (hx : 0 < x) :
    ∀ a ∈ Icc (0 : ℝ) Q, ∀ b ∈ Icc (0 : ℝ) Q,
      |W b x - W a x| ≤ |b - a| *
        ∫ s in Ioc (0 : ℝ) x, W Q s * W Q (x - s) := by sorry

Source

A two-sided orientation of the proved uniform q-discount secant bound.

View graph