Theorems · Definition · probability

MeasureTheory.hittingBtwn

{Ω : Type u_1} → {β : Type u_2} → {ι : Type u_3} → [Preorder ι] → [InfSet ι] → (ι → Ω → β) → Set β → ι → ι → Ω → ι

Hitting time: given a stochastic process u and a set s, hittingBtwn u s n m is the first time u is in s after time n and before time m (if u does not hit s after time n and before m then the hitting time is simply m). The hitting time is a stopping time if the process is strongly adapted and discrete.

Defined in

Mathlib.Probability.Process.HittingTime

Cited by

39 results in Mathlib

Foundations

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

Assumes

PreorderInfSet