English
If f and g are both supermartingales with respect to the same filtration, then their sum f+g is also a supermartingale.
Русский
Если оба процесса f и g являются суперmartингалами относительно одной и той же фильтрации, то их сумма f+g тоже является суперmartingale.
LaTeX
$$$\mathrm{Supermartingale}(f,\mathcal{F},\mu) \land \mathrm{Supermartingale}(g,\mathcal{F},\mu) \Rightarrow \mathrm{Supermartingale}(f+g,\mathcal{F},\mu)$$$
Lean4
theorem add [Preorder E] [AddLeftMono E] (hf : Supermartingale f ℱ μ) (hg : Supermartingale g ℱ μ) :
Supermartingale (f + g) ℱ μ :=
by
refine ⟨hf.1.add hg.1, fun i j hij => ?_, fun i => (hf.2.2 i).add (hg.2.2 i)⟩
refine (condExp_add (hf.integrable j) (hg.integrable j) _).le.trans ?_
filter_upwards [hf.2.1 i j hij, hg.2.1 i j hij]
intros
refine add_le_add ?_ ?_ <;> assumption
