Running supremum stays below a level before an extended first-upcrossing clock

Proved

AvramDividend.Classical.runningSup_pre_extended_upcrossing_clock_le

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

avram-dividendfirst-passageinfinite-clockpathwise-upper

For any finite observation time strictly before the extended-real first strict upward-crossing clock of level b, the running supremum of the Lévy path is at most b. In particular this includes the case where the first crossing is infinite. This supplies the missing terminal-cell bound when the next record level is never reached.

Preamble

import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Theorems.Thm_AvramDividend_Classical_runningSup_eq_rawSup_nonneg

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal Classical

Formal statement

theorem AvramDividend.Classical.runningSup_pre_extended_upcrossing_clock_le
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (ω : Ω) (b : ℝ)
    (t : ℝ≥0)
    (ht : (t : ℝ≥0∞) <
      (⨅ (r : ℝ≥0) (_ : b < X.X r ω), (r : ℝ≥0∞))) :
    runningSup X t ω ≤ b := by sorry

Source

Direct order argument from the raw-supremum characterization, with the first-passage clock defined as an infimum.

View graph