add_martingale — Mathlib

English

If f is a submartingale and g is a martingale with respect to the same filtration, then f+g is a submartingale.

Русский

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

LaTeX

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

Lean4

theorem add_martingale [Preorder E] [AddLeftMono E] (hf : Supermartingale f ℱ μ) (hg : Martingale g ℱ μ) :
    Supermartingale (f + g) ℱ μ :=
  hf.add hg.supermartingale

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