English
The upper crossing time is defined recursively as the first time before N that the process hits above level b after the lower crossing step, producing a nested hitting time definition.
Русский
Верхнее время пересечения задаётся рекурсивно как первое попадание выше уровня b до N после нижнего шага, образуя вложенное определение времени попадания.
LaTeX
$$$ upperCrossingTime(a,b,f,N) = hitting\\, f\\; (\\{t \\ge b\\}) \\; (lowerCrossingTimeAux(a,f,\\text{upperCrossingTime}(a,b,f,N)) ) $$$
Lean4
/-- `upperCrossingTime a b f N n` is the first time before time `N`, `f` reaches
above `b` after `f` reached below `a` for the `n - 1`-th time. -/
noncomputable def upperCrossingTime [Preorder ι] [OrderBot ι] [InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ) (N : ι) : ℕ → Ω → ι
| 0 => ⊥
| n + 1 => fun ω => hitting f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω
