English
Let f be an E-valued process adapted to a filtration F. The martingale part of f with respect to F and a measure μ is given by the base value f0 plus the sum of the increments minus their conditional expectations given the filtration. In particular, for every n, the martingale part up to time n equals f(0) plus the sum of i from 0 to n−1 of [f(i+1) − f(i) − Eμ[f(i+1) − f(i) | F_i]].
Русский
Пусть f — процесс, принимающий значения в E, адаптированный к фильтрации F. Мартингальная часть f по отношению к F и мере μ задаётся как начальное значение f(0) плюс сумма приращений минус их условного математического ожидания по фильтрации. Конкретно, для каждого n мартингальная часть до времени n равна f(0) плюс сумма по i от 0 до n−1 из [f(i+1) − f(i) − Eμ[f(i+1) − f(i) | F_i]].
LaTeX
$$$\\displaystyle \\mathrm{martingalePart}(f,\\mathcal{F},\\mu)_{n} \;=\; f(0) \;+\; \\sum_{i=0}^{n-1} \\Big( f(i+1) - f(i) - \\mathbb{E}_{\\mu}[f(i+1)-f(i) \\mid \\mathcal{F}_{i}] \\Big).$$$
Lean4
theorem martingalePart_eq_sum :
martingalePart f ℱ μ = fun n => f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|ℱ i]) :=
by
unfold martingalePart predictablePart
ext1 n
rw [Finset.eq_sum_range_sub f n, ← add_sub, ← Finset.sum_sub_distrib]
