martingalePart_process_ae_eq — Mathlib

English

The predictable part and the martingale part sum to the process; the decomposition is unique in the sense that f = martingalePart + predictablePart.

Русский

Предсказуемая часть и мартинговая часть образуют разложение процесса; f = martingalePart + predictablePart.

LaTeX

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

Lean4

theorem martingalePart_process_ae_eq (ℱ : Filtration ℕ m0) (μ : Measure Ω) (s : ℕ → Set Ω) (n : ℕ) :
    martingalePart (process s) ℱ μ n =
      ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|ℱ k]) :=
  by
  simp only [martingalePart_eq_sum, process_zero, zero_add]
  refine Finset.sum_congr rfl fun k _ => ?_
  simp only [process, Finset.sum_range_succ_sub_sum]

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