Actual spectrally negative Lévy running-supremum regulator is right-continuous at every time

Proved

AvramDividend.Classical.runningSup_right_continuous_actual

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

avram-classicalexcursion-theorylocal-timeright-continuityrunning-supremum

The actual running supremum of a canonical spectrally negative Lévy process is right-continuous at every nonnegative time, using its monotonicity, exact supremum representation, domination and underlying Lévy right-continuity. Together with proved left continuity this establishes the continuity of the regulator and supports constructing inverse local time and excursion intervals.

Preamble

import Definitions.Def_AvramDividend_Classical_Reflection
import Theorems.Thm_AvramDividend_Classical_runningSup_monotone_and_path_le
import Theorems.Thm_AvramDividend_Classical_runningSup_eq_rawSup_nonneg
import Theorems.Thm_AvramDividend_Classical_runningSup_right_continuous_of_right_continuous

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

Formal statement

theorem AvramDividend.Classical.runningSup_right_continuous_actual
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (ω : Ω) (t : ℝ≥0) :
    ContinuousWithinAt (fun s : ℝ≥0 => runningSup X s ω) (Ici t) t := by sorry

Source

Proved runningSup_monotone_and_path_le, runningSup_eq_rawSup_nonneg, runningSup_right_continuous_of_right_continuous.

View graph