English
Under suitable sigma-finite conditions and suitable hypotheses on g (vanishing at time 0 and integrability), the martingalePart of f+g is almost surely equal to f, time-by-time.
Русский
При подходящих условиях и гипотезах на g (g(0)=0 и интегрируемость), martingalePart(f+g) практически всегда равна f по времени n: для каждого n выполняется равенство почти surely.
LaTeX
$$$\\forall n,\\; \\mathrm{martingalePart}(f+g,\\mathcal{F},\\mu)_{n} =_{a.e.\\mu} f_{n}. $$$
Lean4
theorem martingalePart_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 : ℕ) :
martingalePart (f + g) ℱ μ n =ᵐ[μ] f n :=
by
set h := f - martingalePart (f + g) ℱ μ with hhdef
have hh : h = predictablePart (f + g) ℱ μ - g := by
rw [hhdef, sub_eq_sub_iff_add_eq_add, add_comm (predictablePart (f + g) ℱ μ), martingalePart_add_predictablePart]
have hhpred : Adapted ℱ fun n => h (n + 1) := by
rw [hh]
exact adapted_predictablePart.sub hg
have hhmgle : Martingale h ℱ μ :=
hf.sub
(martingale_martingalePart (hf.adapted.add <| Predictable.adapted hg <| hg0.symm ▸ stronglyMeasurable_zero)
fun n => (hf.integrable n).add <| hgint n)
refine (eventuallyEq_iff_sub.2 ?_).symm
filter_upwards [hhmgle.eq_zero_of_predictable hhpred n] with ω hω
unfold h at hω
rw [Pi.sub_apply] at hω
rw [hω, Pi.sub_apply, martingalePart]
simp [hg0]
