Global unit Lipschitz bound for the unbounded-variation zero-barrier candidate

Proved

AvramDividend.Classical.unbounded_variation_zero_barrier_candidate_lipschitz

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

avram-dividendgenerator-integrabilitylipschitzunbounded-variationzero-barrier

For a spectrally negative Lévy process of unbounded variation under positive discount, the zero-barrier dividend candidate x↦barrierValue W 0 x is globally Lipschitz with constant one. The proved identity with max(x,0) and the pinned Mathlib LipschitzWith.max_const lemma establish the result, which controls jumps and supports generator-domain integrability without extra smoothness conditions.

Preamble

import Theorems.Thm_AvramDividend_Classical_unbounded_variation_zero_barrier_candidate_eq_posPart
import Mathlib.Topology.MetricSpace.Lipschitz

open AvramDividend.Classical MeasureTheory
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.unbounded_variation_zero_barrier_candidate_lipschitz
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (q : ℝ) (hq : 0 < q)
    (W : ℝ → ℝ) (hW : IsScaleFunction X q W)
    (hnbv : ¬ X.BoundedVariation) :
    LipschitzWith (1 : ℝ≥0) (barrierValue W 0) := by sorry

Source

Proved zero-barrier candidate equals positive-part identity; pinned Mathlib LipschitzWith.id and LipschitzWith.max_const.

View graph