upcrossings_eq_top_of_frequently_lt

English

If a<b and the process frequently stays below a and above b, then the upcrossings count is infinite.

Русский

Если a<b и процесс часто бывает ниже a и выше b, то число upcrossings стремится к бесконечности.

LaTeX

$$$\\text{If } a

Lean4

/-- A stochastic process that frequently visits below `a` and above `b` has infinite upcrossings. -/ theorem upcrossings_eq_top_of_frequently_lt (hab : a < b) (h₁ : ∃ᶠ n in atTop, f n ω < a) (h₂ : ∃ᶠ n in atTop, b < f n ω) : upcrossings a b f ω = ∞ := by_contradiction fun h => not_frequently_of_upcrossings_lt_top hab h ⟨h₁, h₂⟩

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