The genuine spectrally negative Lévy running-supremum local-time regulator is continuous at time zero

Proved

AvramDividend.Classical.runningSup_continuousAt_origin

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

avram-classicalcontinuityexcursion-inverselocal-timeorigin

At the bottom time 0 of ℝ≥0, right-continuity is full continuity because Ici 0 is the universal time domain. The already proved runningSup_right_continuous_actual theorem consequently yields continuity of the genuine running maximum at its origin, completing the endpoint requirement for a globally continuous local-time regulator and the inverse local-time construction.

Preamble

import Mathlib.Topology.ContinuousOn
import Mathlib.Data.NNReal.Basic
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_origin
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (ω : Ω) :
    ContinuousAt (fun s : ℝ≥0 => runningSup X s ω) 0 := by sorry

Source

Proved runningSup_right_continuous_actual and pinned Mathlib continuousWithinAt_univ.

View graph