Finite-valued stopping-time filtration condition implies Mathlib IsStoppingTime
ProvedAvramDividend.Classical.isStoppingTime_withTop_of_le_eventsavram-classicalfiltrationstopping-timestrong-markovtype-bridge
The stopped-history convention used in the Lévy mission, that each event {τ≤s} belongs to filtration F_s, directly entails Mathlib's IsStoppingTime for the canonical WithTop coercion of finite nonnegative stopping times. This is needed to apply the proved bounded stopping-grid convergence result to the strong-Markov barrier stopping times.
Preamble
import Mathlib.Probability.Process.Stopping open MeasureTheory open scoped NNReal ENNReal
Formal statement
theorem AvramDividend.Classical.isStoppingTime_withTop_of_le_events
{Ω : Type*} [mΩ : MeasurableSpace Ω]
{𝓕 : Filtration ℝ≥0 mΩ}
(τ : Ω → ℝ≥0)
(hτ : ∀ s : ℝ≥0,
MeasurableSet[𝓕 s] {ω : Ω | τ ω ≤ s}) :
IsStoppingTime 𝓕 (fun ω => (τ ω : WithTop ℝ≥0)) := by
sorrySource
Exact type/interface bridge for open strong-Markov shifted-path independence 61930a38-11f1-449e-bbb6-67d59c6d5ca8 and dividend-value barrier splitting child 79978d61-9d1f-4b20-b8a5-114797a8e380. Connects hτ to IsStoppingTime without W.