Strict nonattainment of a level on a compact upper-semicontinuous prefix gives a uniform positive gap below the level

Proved

AvramDividend.Classical.usc_compact_prefix_sup_strictly_below_level

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

avram-classicalcompactnessfirst-passagegrid-approximationupper-semicontinuity

If a real-valued path R is upper semicontinuous on the compact interval [0,t] and stays strictly below x at every time in that interval, then its exact supremum over the entire prefix is strictly below x. The proof uses compactness to obtain a time attaining the maximum, so there is a uniform positive gap between x and the supremum. This lemma is a key deterministic ingredient for showing that rational-grid first hitting times of levels x−1/n converge to the continuous-time first hit of x, thereby connecting stopping-time grid constructions to genuine excursion first-passage times.

Preamble

import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy
import Mathlib.Topology.Semicontinuity.Basic
import Mathlib.Order.ConditionallyCompleteLattice.Basic

open AvramDividend.Classical Set Topology
open scoped NNReal

Formal statement

theorem AvramDividend.Classical.usc_compact_prefix_sup_strictly_below_level
    (R : ℝ≥0 → ℝ) (t : ℝ≥0) (x : ℝ)
    (husc : UpperSemicontinuousOn R (Icc 0 t))
    (hNoHit : ∀ s : ℝ≥0, s ≤ t → R s < x) :
    sSup (R '' Icc (0 : ℝ≥0) t) < x := by sorry

Source

Compactness and upper-semicontinuous maximum theorem, pinned Mathlib UpperSemicontinuousOn.exists_isMaxOn.

View graph