measurable_upcrossings — Mathlib

English

The total upcrossings function a < b and f is measurable: the map ω ↦ upcrossings(a, b, f)(ω) is measurable.

Русский

Общая функция upcrossings(a, b, f) измерима: отображение ω↦upcrossings(a,b,f)(ω) измеримо.

LaTeX

$$Measurable\left( upcrossings(a,b,f) \right)$$

Lean4

theorem measurable_upcrossings (hf : Adapted ℱ f) (hab : a < b) : Measurable (upcrossings a b f) :=
  .iSup fun _ => measurable_from_top.comp (hf.measurable_upcrossingsBefore hab)

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