adapted_predictablePart — Mathlib

English

The adaptedness of predictablePart f ℱ μ n holds uniformly: for each n, predictablePart f ℱ μ n is adapted to the filtration up to n.

Русский

Адаптированность предсказуемой части сохраняется: для каждого n предсказуемая часть описывается адаптированно к фильтрации до n.

LaTeX

$$$$\mathrm{Adapted}(\mathcal{F}, \mathrm{predictablePart}(f, \mathcal{F}, \mu))(n).$$$$

Lean4

theorem adapted_predictablePart : Adapted ℱ fun n => predictablePart f ℱ μ (n + 1) := fun _ =>
  Finset.stronglyMeasurable_sum _ fun _ hin =>
    stronglyMeasurable_condExp.mono (ℱ.mono (Finset.mem_range_succ_iff.mp hin))

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