Entire reflected-running-supremum dividend measure vanishes at all nonpositive times
ProvedAvramDividend.Classical.runningSup_dividendMeasure_zero_nonpositiveavram-classicalnonpositive-supportrunning-supremumstieltjesstrong-markov
The actual Lebesgue–Stieltjes dividend measure of a spectrally negative Lévy running supremum vanishes on the complete nonpositive real-time half-line. Combine proved zero mass of every negative-to-zero interval and countable exhaustion. This supplies the support boundary condition for factorising future running-supremum dividend rewards at an upper stopping time.
Preamble
import Theorems.Thm_AvramDividend_Classical_measure_Iic_zero_of_all_negative_to_zero_Ioc_zero import Theorems.Thm_AvramDividend_Classical_runningSup_dividendMeasure_Ioc_nonpos_eq_zero open MeasureTheory Set open scoped NNReal ENNReal open AvramDividend.Classical
Formal statement
theorem AvramDividend.Classical.runningSup_dividendMeasure_zero_nonpositive
{Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
{𝓕 : Filtration ℝ≥0 mΩ}
(X : SpectrallyNegativeLevy P 𝓕) (ω : Ω) :
dividendMeasure (runningSup X) ω (Set.Iic (0 : ℝ)) = 0 := by
sorrySource
W-free strong-Markov barrier child 79978d61-9d1f-4b20-b8a5-114797a8e380. Direct import of proved runningSup_dividendMeasure_Ioc_nonpos_eq_zero 55945b02-bdc5-4c2b-a26e-c147b0481f0b and measure_Iic_zero_of_all_negative_to_zero_Ioc_zero 30103409-586a-4404-b4a1-510990034747.