Strict monotonicity of unbounded-variation q-scale families in the discount

Proved

AvramDividend.Classical.unbounded_scale_discount_family_strictMonoOn

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

avram-classicaldiscountscale-functionsensitivitystrict-monotonicity

For an unbounded-variation spectrally negative Lévy process with a valid q-scale function W q for every nonnegative q, the function mapping q to W q x is strictly increasing for each x>0.

Preamble

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

Formal statement

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

Source

Direct functional application of the verified strict pairwise q-discount monotonicity theorem.

View graph