upcrossingsBefore — Mathlib

English

The number of upcrossings before time N is defined as the supremum of indices n with upperCrossingTime a b f N n ω < N.

Русский

Число восходящих до времени N определяется как супремум индексов n, для которых upperCrossingTime a b f N n ω < N.

LaTeX

$$$\\text{upcrossingsBefore}(a,b,f,N,\\omega) := \\sup\\{n : \\mathrm{upperCrossingTime}(a,b,f,N,n,\\omega) < N\\}.$$$

Lean4

/-- The number of upcrossings (strictly) before time `N`. -/
noncomputable def upcrossingsBefore [Preorder ι] [OrderBot ι] [InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ) (N : ι) (ω : Ω) :
    ℕ :=
  sSup {n | upperCrossingTime a b f N n ω < N}

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