Explicit discount Lipschitz modulus across every real reserve

Proved

AvramDividend.Classical.unbounded_scale_discount_family_piecewise_lipschitz_bound

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

all-reservesavram-classicaldiscountlipschitzpiecewise-modulusscale-function

For q-scale functions of an unbounded-variation spectrally negative Lévy process, variation between two nonnegative discount rates has an explicit convolution Lipschitz bound at positive reserves and vanishes exactly at zero and negative reserves. The resulting inequality applies on the whole real reserve line with a piecewise coefficient.

Preamble

import Definitions.Def_AvramDividend_Classical_ScaleFunction
import Theorems.Thm_AvramDividend_Classical_unbounded_scale_discount_family_lipschitz_bound
import Theorems.Thm_AvramDividend_Classical_unbounded_scale_zero_origin_nonnegative_discount
open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.unbounded_scale_discount_family_piecewise_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 : ℝ, ∀ a ∈ Icc (0 : ℝ) Q, ∀ b ∈ Icc (0 : ℝ) Q,
      |W b x - W a x| ≤ |b - a| *
        (if 0 < x then ∫ s in Ioc (0 : ℝ) x, W Q s * W Q (x - s) else 0) := by sorry

Source

Canonical proved positive-reserve convolution Lipschitz estimate, negative support, and zero-origin vanishing.

View graph