Uniqueness of the unbounded-variation q-scale function at a fixed nonnegative discount

Proved

AvramDividend.Classical.unbounded_scale_unique_nonnegative_discount

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

avram-classicallaplacescale-functionunbounded-variationuniqueness

For a spectrally negative Lévy process of unbounded variation, any two q-scale functions with the same nonnegative discount coincide at every positive reserve. The proof uses the eventual positive Lévy-exponent tail to obtain common Laplace transforms, followed by uniqueness of the Laplace transform among continuous functions.

Preamble

import Definitions.Def_AvramDividend_Classical_ScaleFunction
import Theorems.Thm_AvramDividend_Classical_unbounded_psi_two_discounts_common_tail
import Theorems.Thm_AvramDividend_Classical_continuousOn_Ioi_eq_of_laplace_eq_signed
open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.unbounded_scale_unique_nonnegative_discount
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (hnbv : ¬ X.BoundedVariation)
    (q : ℝ) (hq : 0 ≤ q)
    (W₁ W₂ : ℝ → ℝ)
    (hW₁ : IsScaleFunction X q W₁)
    (hW₂ : IsScaleFunction X q W₂) :
    ∀ x : ℝ, 0 < x → W₁ x = W₂ x := by sorry

Source

IsScaleFunction Laplace identity and the previously proved signed Laplace transform uniqueness theorem.

View graph