Stopped value of a stochastic process #
In mathlib, given a stochastic process X : ι → Ω → E and τ : Ω → WithTop ι a stopping time,
we define stoppedValue X τ ω as X (τ ω) if τ ω ≠ ⊤, and an arbitrary value otherwise.
This is not well suited in a number of context where X converges almost surely at infinity,
and we would expect the stopped value to be equal to the limit random variable when τ ω = ⊤
(this is for example true if X is a uniformly integrable martingale).
This limit process is always defined in mathlib as 𝓕.limitProcess X P, with a default value
when it does not make sense. In this file we define 𝓕.stoppedValue' X τ P ω to be equal
to X (τ ω) if τ ω ≠ ⊤, and 𝓕.limitProcess X P ω otherwise.
Definition of the stopped value #
Given a stochastic process X and a stopping time τ 𝓕.stoppedValue' X τ P is the process
given by X (τ ω), where X ⊤ is given by 𝓕.limitProcess X P.
Equations
- MeasureTheory.Filtration.stoppedValue' X τ 𝓕 P ω = if h : τ ω = ⊤ then MeasureTheory.Filtration.limitProcess X 𝓕 P ω else X ((τ ω).untop h) ω