English
Given a stochastic process u, a target set s, and time bounds n ≤ m, the hitting time hits the set s at the first time j ∈ [n,m] such that u_j is in s; if no such time exists, the hitting time is m. Moreover, the hitting time is a stopping time when the process is adapted and discrete.
Русский
Для процесса u, множества s и временных границ n ≤ m, время попадания определяется как первое время j ∈ [n,m], когда u_j ∈ s; если такого времени не существует, время попадания равно m. Время попадания является временем остановки при адаптированности и дискретности процесса.
LaTeX
$$$\text{hitting}(u,s,n,m) = \begin{cases} j &\text{ минимально}, j\in [n,m],\ u_j\in s \\ m &\text{ если такого } j\ нет. \end{cases}$$$
Lean4
/-- Hitting time: given a stochastic process `u` and a set `s`, `hitting 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 adapted and discrete. -/
noncomputable def hitting [Preorder ι] [InfSet ι] (u : ι → Ω → β) (s : Set β) (n m : ι) : Ω → ι := fun x =>
if ∃ j ∈ Set.Icc n m, u j x ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i x ∈ s}) else m
