martingalePart_add_predictablePart

English

For a finite measure μ, the predictablePart of the process equals the sum over k of conditional increments: predictor sum over k.

Русский

Для конечной меры предсказуемая часть равна сумме по k условных приращений.

LaTeX

$$$$\mathrm{predictablePart}(f, \mathcal{F}, \mu)(n) = \sum_{k=0}^{n-1} \mu[ f(k+1) - f(k) \mid \mathcal{F}_k].$$$$

Lean4

theorem martingalePart_add_predictablePart (ℱ : Filtration ℕ m0) (μ : Measure Ω) (f : ℕ → Ω → E) :
    martingalePart f ℱ μ + predictablePart f ℱ μ = f :=
  sub_add_cancel _ _

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