Actual reflected Lévy local-time regulator is continuous at every positive time

Proved

AvramDividend.Classical.runningSup_continuousAt_positive

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

avram-classicalcontinuityexcursion-inverselocal-timerunning-supremum

The genuine running supremum S of a spectrally negative Lévy path is continuous at every strictly positive time. Combine the already proved actual left continuity on Iio t and actual right continuity on Ici t. Restrict right continuity to Ioi t, then use the pinned Mathlib characterisation continuousAt_iff_continuous_left'_right'. This is a necessary strong regularity prerequisite for constructing the local-time inverse and the Itô excursion decomposition rather than merely postulating an excursion measure.

Preamble

import Mathlib.Topology.Order.LeftRight
import Theorems.Thm_AvramDividend_Classical_runningSup_left_continuous_actual
import Theorems.Thm_AvramDividend_Classical_runningSup_right_continuous_actual

open AvramDividend.Classical MeasureTheory Set Topology
open scoped NNReal

Formal statement

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

Source

Proved runningSup_left_continuous_actual and runningSup_right_continuous_actual; Mathlib.Topology.Order.LeftRight.

View graph