English
The lower crossing time is the first time before N that f drops below a after an upper-crossing time, i.e., it is the hitting time to the lower set after the upper crossing step.
Русский
Нижнее время пересечения — первое попадание ниже a до N после верхнего пересечения, т.е. попадание в нижнее множество после нижнего шага.
LaTeX
$$$ lowerCrossingTime(a,b,f,N,n) = hitting\\, f\\; (\\{x \\le a\\}) \\; (upperCrossingTime(a,b,f,N,n)) \\; N $$$
Lean4
/-- `lowerCrossingTime a b f N n` is the first time before time `N`, `f` reaches
below `a` after `f` reached above `b` for the `n`-th time. -/
noncomputable def lowerCrossingTime [Preorder ι] [OrderBot ι] [InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ) (N : ι) (n : ℕ) :
Ω → ι := fun ω => hitting f (Set.Iic a) (upperCrossingTime a b f N n ω) N ω
