Theorems · Definition · probability

MeasureTheory.stoppedProcess

{Ω : Type u_1} →
  {β : Type u_2} → {ι : Type u_3} → [Nonempty ι] → [LinearOrder ι] → (ι → Ω → β) → (Ω → WithTop ι) → ι → Ω → β

Given a map u : ι → Ω → E, the stopped process with respect to τ is u i ω if i ≤ τ ω, and u (τ ω) ω otherwise. Intuitively, the stopped process stops evolving once the stopping time has occurred.

Defined in

Mathlib.Probability.Process.Stopping

Cited by

51 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonemptyLinearOrder