Barrier strategy pays no Stieltjes dividend at any real time through first upward passage

Proved

AvramDividend.Classical.barrierStrategy_dividendMeasure_zero_preUpcrossing_Iic

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

avram-classicalbarrier-strategyfirst-upcrossingstieltjesstrong-markov

For initial reserve at or below barrier a, if first upcrossing of the barrier gap occurs at a finite time u, the entire original Stieltjes dividend measure of (-∞,u] is zero. Combine no negative-time payments, no initial atom, and the proved zero payment on [0,u]. This is the exact hμzero required by the translated weighted-payoff integral lemma.

Preamble

import Mathlib.MeasureTheory.Measure.MeasureSpace
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_dividendMeasure_zero_nonpositive
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_dividendMeasure_zero_through_firstUpcrossing
import Theorems.Thm_AvramDividend_Classical_measure_Iic_zero_of_zero_nonpositive_and_initial_window

open MeasureTheory Set
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.barrierStrategy_dividendMeasure_zero_preUpcrossing_Iic
    {Ω : 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.Iic (u : ℝ)) = 0 := by
  sorry

Source

Canonical W-free strong-Markov child 79978d61-9d1f-4b20-b8a5-114797a8e380. Direct composition of barrierStrategy_dividendMeasure_zero_nonpositive (publication pending) with Proved barrierStrategy_dividendMeasure_zero_through_firstUpcrossing 4396ddd6 and measure_Iic_zero_of_zero_nonpositive_and_initial_window 48bc6398.

View graph