add — Mathlib

English

If f and g are martingales with respect to the same filtration, their sum f + g is a martingale.

Русский

Если f и g — мартингалы относительно одной и той же фильтрации, то их сумма f+g — мартингал.

LaTeX

$$$\\text{Martingale}(f, \\mathcal{F}, \\mu) \\land \\text{Martingale}(g, \\mathcal{F}, \\mu) \\Rightarrow \\text{Martingale}(f+g, \\mathcal{F}, \\mu)$$$

Lean4

theorem add (hf : Martingale f ℱ μ) (hg : Martingale g ℱ μ) : Martingale (f + g) ℱ μ :=
  by
  refine ⟨hf.adapted.add hg.adapted, fun i j hij => ?_⟩
  exact (condExp_add (hf.integrable j) (hg.integrable j) _).trans ((hf.2 i j hij).add (hg.2 i j hij))

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