Unbounded-variation zero-barrier scale candidate equals available reserves

Proved

AvramDividend.Classical.unbounded_variation_zero_barrier_candidate_eq_reserve

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

avram-dividendboundary-valuescale-functionunbounded-variationzero-barrier

For any positive discount and spectrally negative Lévy process of unbounded variation, the zero-scale-origin identity and the affine zero-barrier formula imply the barrier candidate value is exactly the initial reserve at every nonnegative initial capital. This completes the positive-reserve extension of the zero-barrier candidate boundary condition, independent of the stochastic dividend-value identity.

Preamble

import Theorems.Thm_AvramDividend_Classical_chat04_scale_zero_origin_of_unbounded_variation
import Theorems.Thm_AvramDividend_Classical_barrierValue_zero_of_scale_zero
import Theorems.Thm_AvramDividend_Classical_barrierValue_zero_affine_nonnegative

open AvramDividend.Classical MeasureTheory
open scoped NNReal ENNReal

Formal statement

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

Source

Existing Proved zero-origin scale theorem, barrierValue_zero_of_scale_zero and barrierValue_zero_affine_nonnegative.

View graph