upcrossingStrat_adapted — Mathlib

English

The function upcrossingStrat is adapted with respect to the filtration, i.e., measurable w.r.t. each stage.

Русский

Функция upcrossingStrat адаптирована к фильтрации, то есть измерима относительно каждого этапа.

LaTeX

$$$\text{Adapted}(\mathcal{F}, \text{upcrossingStrat}(a,b,f,N))$$$

Lean4

theorem upcrossingStrat_adapted (hf : Adapted ℱ f) : Adapted ℱ (upcrossingStrat a b f N) :=
  by
  intro n
  change
    StronglyMeasurable[ℱ n] fun ω =>
      ∑ k ∈ Finset.range N,
        ({n | lowerCrossingTime a b f N k ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (k + 1) ω}).indicator 1 n
  refine
    Finset.stronglyMeasurable_fun_sum _ fun i _ =>
      stronglyMeasurable_const.indicator ((hf.isStoppingTime_lowerCrossingTime n).inter ?_)
  simp_rw [← not_le]
  exact (hf.isStoppingTime_upperCrossingTime n).compl

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