Theorems · Definition · probability

MeasureTheory.stoppedValue

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

Given a map u : ι → Ω → E, its stopped value with respect to the stopping time τ is the map x ↦ u (τ ω) ω.

Defined in

Mathlib.Probability.Process.Stopping

Cited by

51 results in Mathlib

Foundations

Depth 8 from the axioms · uses Classical.choice

Assumes

Nonempty