adapted — Mathlib

English

If a process u is progressively measurable, then it is adapted to the filtration f.

Русский

Если процесс u прогрессивно измерим, то он адаптирован к фильтрации f.

LaTeX

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

Lean4

protected theorem adapted (h : ProgMeasurable f u) : Adapted f u :=
  by
  intro i
  have : u i = (fun p : Set.Iic i × Ω => u p.1 p.2) ∘ fun x => (⟨i, Set.mem_Iic.mpr le_rfl⟩, x) := rfl
  rw [this]
  exact (h i).comp_measurable measurable_prodMk_left

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