Below-cap barrier dividends have no Stieltjes mass at or before time zero

Proved

AvramDividend.Classical.barrierStrategy_dividendMeasure_zero_nonpositive

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

avram-classicalbarrier-strategydividend-measurestrong-markovsupport

For a spectrally negative Lévy process and initial reserve between zero and its nonnegative dividend barrier, the barrier dividend Stieltjes measure has zero mass on all real times up to and including zero. The admissible strategy is monotone, the barrier regulator is right-continuous, and the generic right-limit-fixed Stieltjes support theorem applies.

Preamble

import Mathlib.Data.NNReal.Defs
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_isDividendStrategy_nonnegative_barrier
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_right_continuous_below_barrier
import Theorems.Thm_AvramDividend_Classical_rightLim_comp_toNNReal_of_rightContinuous
import Theorems.Thm_AvramDividend_Classical_dividendMeasure_Iic_zero_of_monotone_rightLim

open MeasureTheory Set
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.barrierStrategy_dividendMeasure_zero_nonpositive
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (x a : ℝ) (hx0 : 0 ≤ x) (hxa : x ≤ a) (ω : Ω) :
    dividendMeasure (barrierStrategy X x a) ω
      (Set.Iic (0 : ℝ)) = 0 := by
  sorry

Source

Removes hμneg from Proved map-shift helper 3093890e-4ed7-4198-8491-5f41d268763c in the W-free strong-Markov child 79978d61-9d1f-4b20-b8a5-114797a8e380. Uses proved right continuity 1d8e9ea2, dividend strategy 501af29f, real-time right-limit conversion 95b3270f, and our pending generic support publication 2a38c903-6fe0-4d5f-802b-b179a2bcb5.

View graph