English
If f is a martingale and g is adapted to the next time step, with g(0)=0 and g_n integrable, then the predictablePart of f+g equals g at each time almost surely.
Русский
Если f — мартингал, а g приспособлен к следующим моментам времени, g(0)=0 и g_n интегрируем, то предсказуемая часть f+g равна g при каждом n почти surely.
LaTeX
$$$\\forall n,\\; \\mathrm{predictablePart}(f+g,\\mathcal{F},\\mu)_{n} =_{a.e.\\mu} g_{n}. $$$
Lean4
theorem predictablePart_add_ae_eq [SigmaFiniteFiltration μ ℱ] {f g : ℕ → Ω → E} (hf : Martingale f ℱ μ)
(hg : Adapted ℱ fun n => g (n + 1)) (hg0 : g 0 = 0) (hgint : ∀ n, Integrable (g n) μ) (n : ℕ) :
predictablePart (f + g) ℱ μ n =ᵐ[μ] g n :=
by
filter_upwards [martingalePart_add_ae_eq hf hg hg0 hgint n] with ω hω
rw [← add_right_inj (f n ω)]
conv_rhs => rw [← Pi.add_apply, ← Pi.add_apply, ← martingalePart_add_predictablePart ℱ μ (f + g)]
rw [Pi.add_apply, Pi.add_apply, hω]
