Finite-horizon truncation of an extended nonnegative stopping clock remains a stopping clock

Proved

AvramDividend.Classical.extendedStopping_truncate_finite_leEvents

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

first-passageroot-connectedstopping-timestrong-markovtruncation

For any possibly infinite stopping time tau and deterministic finite horizon n, the truncated clock min(tau,n), converted into a nonnegative real time, has stopping-time level events. This bridges infinite first-passage stopping times to the finite-clock strong-Markov factorisation needed for the barrier dividend identity.

Preamble

import Mathlib.Probability.Process.Stopping
import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy

open MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.extendedStopping_truncate_finite_leEvents
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {𝓕 : Filtration ℝ≥0 mΩ}
    (τ : Ω → ℝ≥0∞) (hτ : IsStoppingTime 𝓕 τ)
    (n : ℝ≥0) :
    ∀ s : ℝ≥0,
      MeasurableSet[𝓕 s]
        {ω : Ω | (min (τ ω) (n : ℝ≥0∞)).toNNReal ≤ s} := by
  sorry

Source

Root-connected Strong-Markov barrier split 79978d61-9d1f-4b20-b8a5-114797a8e380. Proves a reusable finite-stopping-clock localisation property from Mathlib IsStoppingTime.min_const.

View graph