No barrier-dividend Stieltjes mass before or at the first upper passage

Proved

AvramDividend.Classical.barrierStrategy_dividendMeasure_zero_until_firstUpcrossing

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

avram-classicalbarrier-dividendroot-connectedstieltjesstrong-markov

When a barrier strategy starts below the barrier, the cumulative dividend process is zero at time zero and at the first finite strict upper passage. Monotonicity and right-continuity imply that its Stieltjes dividend measure gives zero mass to the interval from time zero through that upper passage.

Preamble

import Mathlib.Data.NNReal.Defs
import Theorems.Thm_AvramDividend_Classical_dividendMeasure_Ioc_eq_path_increment_of_mono_rightLim
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_monotone_of_le
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_right_continuous_of_le
import Theorems.Thm_AvramDividend_Classical_rightLim_comp_toNNReal_of_rightContinuous
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_zero_at_firstUpcrossing
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_isDividendStrategy_nonnegative_barrier

open MeasureTheory Filter Set Topology
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.barrierStrategy_dividendMeasure_zero_until_firstUpcrossing
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (x a : ℝ) (hx0 : 0 ≤ x) (hxa : x ≤ a)
    (ω : Ω) (u : ℝ≥0)
    (hu : (u : ℝ≥0∞) =
      (⨅ (s : ℝ≥0) (_ : a - x < X.X s ω), (s : ℝ≥0∞))) :
    (dividendMeasure (barrierStrategy X x a) ω)
      (Set.Ioc (0 : ℝ) (u : ℝ)) = 0 := by
  sorry

Source

Root-connected pathwise bridge for the strong-Markov dividend-value splitting theorem 79978d61-9d1f-4b20-b8a5-114797a8e380. Uses established zero-at-upcrossing and the exact Stieltjes interval formula; no scale-function premises.

View graph