adapted_natural — Mathlib

English

If every component u_i is strongly measurable, then the natural filtration built from u is adapted to u.

Русский

Если все элементы u_i сильно измеримы, то естественная фильтрация, порождаемая u, адаптирована к u.

LaTeX

$$$\\mathrm{Adapted}(\\mathrm{Filtration.natural}(u, hum),\\, u)$$$

Lean4

theorem adapted_natural [MetrizableSpace β] [mβ : MeasurableSpace β] [BorelSpace β] {u : ι → Ω → β}
    (hum : ∀ i, StronglyMeasurable[m] (u i)) : Adapted (Filtration.natural u hum) u :=
  by
  intro i
  refine StronglyMeasurable.mono ?_ (le_iSup₂_of_le i (le_refl i) le_rfl)
  rw [stronglyMeasurable_iff_measurable_separable]
  exact ⟨measurable_iff_comap_le.2 le_rfl, (hum i).isSeparable_range⟩

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