upcrossings — Mathlib

English

For a, b real with a < b and a process f, the total number of upcrossings is the supremum over N of the finite-time upcrossingsBefore counts, i.e.,

Русский

Для действительных a < b и процесса f, общее число восходящих пересечений определяется как верхняя грань по N числа upcrossingsBefore.

LaTeX

$$$\mathrm{upcrossings}(a,b,f)(\omega)=\sup_{N\in\mathbb{N}} \bigl( upcrossingsBefore(a,b,f,N)(\omega) \bigr)$$$

Lean4

/-- The number of upcrossings of a realization of a stochastic process (`upcrossings` takes value
in `ℝ≥0∞` and so is allowed to be `∞`). -/
noncomputable def upcrossings [Preorder ι] [OrderBot ι] [InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ) (ω : Ω) : ℝ≥0∞ :=
  ⨆ N, (upcrossingsBefore a b f N ω : ℝ≥0∞)

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