measurable_upcrossingsBefore — Mathlib

English

Let f be adapted to the filtration ℱ and a < b. Then for every natural number N, the map ω ↦ upcrossingsBefore(a, b, f, N)(ω) is measurable.

Русский

Пусть f адаптирован к фильтрации ℱ и a < b. Тогда для каждого натурального N функция ω ↦ upcrossingsBefore(a, b, f, N)(ω) измерима.

LaTeX

$$$\operatorname{Measurable}\bigl( upcrossingsBefore(a,b,f,N) \bigr)$$$

Lean4

theorem measurable_upcrossingsBefore (hf : Adapted ℱ f) (hab : a < b) : Measurable (upcrossingsBefore a b f N) :=
  by
  have :
    upcrossingsBefore a b f N = fun ω =>
      ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i :=
    by
    ext ω
    exact upcrossingsBefore_eq_sum hab
  rw [this]
  exact
    Finset.measurable_fun_sum _ fun i _ =>
      Measurable.indicator measurable_const <| ℱ.le N _ (hf.isStoppingTime_upperCrossingTime.measurableSet_lt_of_pred N)

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