upcrossingsBefore_le — Mathlib

English

For hab: a < b, the map N ↦ upcrossingsBefore a b f N ω is monotone in N for every ω.

Русский

Для любого ω отображение N ↦ upcrossingsBefore a b f N ω неубывает по N, если a < b.

LaTeX

$$$\\text{Monotone}_{N}\\bigl(\\omega\\mapsto \\mathrm{upcrossingsBefore}(a,b,f,N,\\omega)\\bigr)\\;\\text{при } a

Lean4

theorem upcrossingsBefore_le (f : ℕ → Ω → ℝ) (ω : Ω) (hab : a < b) : upcrossingsBefore a b f N ω ≤ N :=
  by
  by_cases hN : N = 0
  · subst hN
    rw [upcrossingsBefore_zero]
  · refine csSup_le ⟨0, zero_lt_iff.2 hN⟩ fun n (hn : _ < N) => ?_
    by_contra hnN
    exact hn.ne (upperCrossingTime_eq_of_bound_le hab (not_le.1 hnN).le)

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