Running-supremum dividend measure vanishes before its first positive record

Proved

AvramDividend.Classical.runningSup_dividendMeasure_zero_through_first_positive_record

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

avram-dividenddividend-measurefirst-positive-recordinitial-cellpathwise-upper

The running supremum makes no dividend payments on the interval from time zero through its first positive upcrossing, provided the initial reserve used for its equivalent barrier strategy is nonnegative. This eliminates the initial unrecorded interval from the countable first-record grid decomposition of the stopped dividend reward.

Preamble

import Mathlib.MeasureTheory.Measure.Restrict
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_dividendMeasure_zero_until_firstUpcrossing
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_self_eq_runningSup

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

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

Source

Direct specialisation of Proved barrierStrategy_dividendMeasure_zero_until_firstUpcrossing at x=a, rewriting barrierStrategy X a a by Proved barrierStrategy_self_eq_runningSup. Supports root c6c3b1d0-2c2f-41ce-a5a0-2771efcc3a69.

View graph