predictablePart_process_ae_eq — Mathlib

English

For any ℕ-indexed process f taking values in a normed space, the predictable part is well-defined as the sum of conditional expectations of increments with respect to the filtration.

Русский

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

LaTeX

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

Lean4

theorem predictablePart_process_ae_eq (ℱ : Filtration ℕ m0) (μ : Measure Ω) (s : ℕ → Set Ω) (n : ℕ) :
    predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator (1 : Ω → ℝ)|ℱ k] :=
  by
  have := martingalePart_process_ae_eq ℱ μ s n
  simp_rw [martingalePart, process, Finset.sum_sub_distrib] at this
  exact sub_right_injective this

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