lowerCrossingTimeAux — Mathlib

English

The lower crossing time auxiliary is defined as the first time the path f crosses below a level a after a time c and before N, i.e., hitting of the level set {x ≤ a} between c and N.

Русский

Нижнее переходное время-резервуар — это первое пересечение траектории f ниже уровня a после времени c и до N, то есть попадание в множество {x ≤ a} между c и N.

LaTeX

$$$ lowerCrossingTimeAux(a,f,c,N) = hitting\\; f \\; (\\{x \\le a\\}) \\; c \\; N $$$

Lean4

/-- `lowerCrossingTimeAux a f c N` is the first time `f` reached below `a` after time `c` before
time `N`. -/
noncomputable def lowerCrossingTimeAux [Preorder ι] [InfSet ι] (a : ℝ) (f : ι → Ω → ℝ) (c N : ι) : Ω → ι :=
  hitting f (Set.Iic a) c N

Похожие утверждения