English
A stopping time with respect to a filtration f is a rule τ: Ω → ι such that for every i, the set {ω | τ(ω) ≤ i} is measurable w.r.t. the i-th level of the filtration.
Русский
Время останова относительно фильтрации f — это правило τ: Ω → ι, такое что для каждого i множество {ω | τ(ω) ≤ i} измеримо в σ-алгебре f_i.
LaTeX
$$$$ \forall i, \{\omega \mid τ(ω) \le i\} \in \mathcal F_i. $$$$
Lean4
/-- A stopping time with respect to some filtration `f` is a function
`τ` such that for all `i`, the preimage of `{j | j ≤ i}` along `τ` is measurable
with respect to `f i`.
Intuitively, the stopping time `τ` describes some stopping rule such that at time
`i`, we may determine it with the information we have at time `i`. -/
def IsStoppingTime [Preorder ι] (f : Filtration ι m) (τ : Ω → ι) :=
∀ i : ι, MeasurableSet[f i] <| {ω | τ ω ≤ i}
