English
If a real-valued process has increments bounded in absolute value by R, then the martingalePart has increments bounded by 2R almost surely.
Русский
Если процесс имеет приращения по модулю ограниченные на R, то мартингальная часть имеет приращения не более чем 2R почти surely.
LaTeX
$$$\\forall i, |\\mathrm{martingalePart}(f,\\mathcal{F},\\mu)(i+1,\\omega) - \\mathrm{martingalePart}(f,\\mathcal{F},\\mu)(i,\\omega)| \\le 2R.$$$
Lean4
theorem martingalePart_bdd_difference {R : ℝ≥0} {f : ℕ → Ω → ℝ} (ℱ : Filtration ℕ m0)
(hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) :
∀ᵐ ω ∂μ, ∀ i, |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R) :=
by
filter_upwards [hbdd, predictablePart_bdd_difference ℱ hbdd] with ω hω₁ hω₂ i
simp only [two_mul, martingalePart, Pi.sub_apply]
have :
|f (i + 1) ω - predictablePart f ℱ μ (i + 1) ω - (f i ω - predictablePart f ℱ μ i ω)| =
|f (i + 1) ω - f i ω - (predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω)| :=
by
ring_nf -- `ring` suggests `ring_nf` despite proving the goal
rw [this]
exact (abs_sub _ _).trans (add_le_add (hω₁ i) (hω₂ i))
