adapted_martingalePart — Mathlib

English

If f is adapted to the filtration F, then the martingalePart of f with respect to F and μ is also adapted to F. In other words, each time-projected value of martingalePart is measurable with respect to the corresponding filtration σ-algebra.

Русский

Если f адаптирован к фильтрации F, то и мартингальная часть f по отношению к F и μ является адаптированной к F: для каждого времени элемент martingalePart(f, F, μ)_n измерим относительно фильтрации F_n.

LaTeX

$$$\\forall n,\\; (\\mathrm{martingalePart}(f,\\mathcal{F},\\mu))_{n}$ тесно измерим относительно $\\mathcal{F}_{n}$.$$

Lean4

theorem adapted_martingalePart (hf : Adapted ℱ f) : Adapted ℱ (martingalePart f ℱ μ) :=
  Adapted.sub hf adapted_predictablePart'

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