Theorems · Definition · probability

MeasureTheory.IsStoppingTime

{Ω : Type u_1} →
  {ι : Type u_3} → {m : MeasurableSpace Ω} → [inst : Preorder ι] → MeasureTheory.Filtration ι m → (Ω → WithTop ι) → Prop

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.

Defined in

Mathlib.Probability.Process.Stopping

Cited by

122 results in Mathlib

Foundations

Depth 17 from the axioms, rests on 156 definitions · uses propext, Quot.sound

Assumes

Preorder