add_martingale — Mathlib

English

If f is a Submartingale, then multiplying by a nonnegative scalar c preserves the submartingale property.

Русский

Если f — субмартингал, умножение на неотрицательную константу c сохраняет субмартингальность.

LaTeX

$$$c \ge 0 \Rightarrow \mathrm{Submartingale}(f,\mathcal{F},\mu) \Rightarrow \mathrm{Submartingale}(c\cdot f,\mathcal{F},\mu)$$$

Lean4

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

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