adapted_predictablePart' — Mathlib

English

The martingale part plus the predictable part recovers the original process exactly for each n and ω.

Русский

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

LaTeX

$$$$\mathrm{martingalePart}(f, \mathcal{F}, \mu)(n,\omega) + \mathrm{predictablePart}(f, \mathcal{F}, \mu)(n, \omega) = f(n,\omega).$$$$

Lean4

theorem adapted_predictablePart' : Adapted ℱ fun n => predictablePart f ℱ μ n := fun _ =>
  Finset.stronglyMeasurable_sum _ fun _ hin => stronglyMeasurable_condExp.mono (ℱ.mono (Finset.mem_range_le hin))

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