Capped countable-grid excursion drawdown first passage is an actual stopping time with right-continuous filtration

Proved

AvramDividend.Classical.reflectedSup_countable_capped_grid_isStoppingTime

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

avram-classicalcountable-gridexcursion-heightreflected-levystopping-time

Let X be an actual spectrally negative Lévy process with reflected drawdown R and an explicitly right-continuous filtration. For any sequence of deterministic observation times bounded above by a finite horizon H and any level x, the first observed time at which the reflected drawdown reaches level x, or the cap H if none does, is an honest stopping time. This is obtained by instantiating the accepted general adapted countable-grid stopping-time lemma with the separately accepted actual reflected-process adaptedness theorem. It supplies a directly usable stochastic first-passage approximation for reflected Lévy excursions while making no unsupported claim about the full continuous-time excursion first-height debut.

Preamble

import Theorems.Thm_AvramDividend_Classical_reflectedSup_adapted
import Theorems.Thm_AvramDividend_Classical_countable_capped_grid_superlevel_isStoppingTime

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.reflectedSup_countable_capped_grid_isStoppingTime
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ} [𝓕.IsRightContinuous]
    (X : SpectrallyNegativeLevy P 𝓕)
    (clock : ℕ → ℝ≥0) (H : ℝ≥0)
    (hclock : ∀ n : ℕ, clock n ≤ H) (x : ℝ) :
    IsStoppingTime 𝓕 (fun ω : Ω =>
      ⨅ n : ℕ, if x ≤ reflectedSup X (clock n) ω
        then (clock n : WithTop ℝ≥0) else (H : WithTop ℝ≥0)) := by sorry

Source

Pinned Mathlib countable-inf stopping times under right-continuous filtration and the accepted Prove2Me actual reflectedSup_adapted theorem.

View graph