Theorems · Definition · probability

MeasureTheory.hittingAfter

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

Hitting time: given a stochastic process u and a set s, hittingAfter u s n is the first time u is in s after time n (if u does not hit s after time n then the hitting time is ⊤).

Defined in

Mathlib.Probability.Process.HittingTime

Cited by

19 results in Mathlib

Foundations

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

Assumes

PreorderInfSet