First genuine reflected running-maximum hit occurs before any finite terminal time at which the reflected process lies below that maximum

Proved

AvramDividend.Classical.reflectedSup_terminal_below_max_capped_first_hit_geometry

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

atomlessnessavram-classicalheight-attainmentrunning-maximumstopping-timeterminal-gap

For an actual spectrally negative Lévy reflected path and a deterministic finite horizon H, let x>0 be its exact supremum over [0,H]. If its terminal value R(H) is strictly less than x, then the true capped first closed-level-x hit T lies before H and satisfies R(T)=x; moreover every reflected path value through H is ≤x. This is the pathwise geometry needed to prove the substantive probability result P(max_{s≤H} R_s=x and R_H<x)=0 whenever the original Lévy process is downward regular. The proof uses compact USC maximum attainment before a lower endpoint, the accepted exact first-level entrance theorem, and the cap-removal infimum lemma.

Preamble

import Mathlib.Topology.Semicontinuity.Basic
import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Theorems.Thm_AvramDividend_Classical_usc_compact_sup_level_hit_before_lower_endpoint
import Theorems.Thm_AvramDividend_Classical_first_exact_level_hit_of_upperSemicontinuous
import Theorems.Thm_AvramDividend_Classical_reflectedSup_upperSemicontinuousOn_Icc
import Theorems.Thm_AvramDividend_Classical_reflectedSup_origin_eq_zero
import Theorems.Thm_AvramDividend_Classical_nnreal_sInf_union_cap_eq_of_early_member

open AvramDividend.Classical MeasureTheory Set Topology
open scoped NNReal

Formal statement

theorem AvramDividend.Classical.reflectedSup_terminal_below_max_capped_first_hit_geometry
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (ω : Ω)
    (H : ℝ≥0) (x : ℝ) (hx : 0 < x)
    (hMax : sSup ((fun u : ℝ≥0 => reflectedSup X u ω) '' Icc 0 H) = x)
    (hEnd : reflectedSup X H ω < x) :
    sInf ((Icc (0 : ℝ≥0) H ∩
      (fun u : ℝ≥0 => reflectedSup X u ω) ⁻¹' Ici x) ∪ {H}) < H ∧
    reflectedSup X (sInf ((Icc (0 : ℝ≥0) H ∩
      (fun u : ℝ≥0 => reflectedSup X u ω) ⁻¹' Ici x) ∪ {H})) ω = x ∧
    ∀ t : ℝ≥0, t ≤ H → reflectedSup X t ω ≤ x := by sorry

Source

Accepted first_exact_level_hit_of_upperSemicontinuous, reflectedSup_upperSemicontinuousOn_Icc, nnreal_sInf_union_cap_eq_of_early_member and usc_compact_sup_level_hit_before_lower_endpoint.

View graph