adapted — Mathlib

English

Another formulation: under discrete index, Adapted implies ProgMeasurable.

Русский

Еще одно формулирование: при дискретном индексе Adapted => ProgMeasurable.

LaTeX

$$$\\mathrm{Adapted}(f,u) \\Rightarrow \\mathrm{ProgMeasurable}(f,u)$$$

Lean4

theorem adapted {f : Filtration ℕ m} {u : ℕ → Ω → β} (hu : Adapted f fun n => u (n + 1))
    (hu0 : StronglyMeasurable[f 0] (u 0)) : Adapted f u := fun n =>
  match n with
  | 0 => hu0
  | n + 1 => (hu n).mono (f.mono n.le_succ)

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