pos — Mathlib

English

If c ≥ 0 and f is a Submartingale with respect to μ, then the scalar multiple c·f is a Submartingale.

Русский

Если c ≥ 0 и f — субмартингал, то произведение c·f — субмартингал.

LaTeX

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

Lean4

protected theorem pos {f : ι → Ω → ℝ} (hf : Submartingale f ℱ μ) : Submartingale (f⁺) ℱ μ :=
  hf.sup (martingale_zero _ _ _).submartingale

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