smul_nonneg — Mathlib

English

Let f be a submartingale. For a nonnegative scalar c ≥ 0, the scaled process c · f is again a submartingale.

Русский

Пусть f — субмартингал. Для неотрицательного коэффициента c ≥ 0 процесс c · f снова является субмартингалом.

LaTeX

$$$0 \\le c \\Rightarrow \\text{Submartingale}(f, \\mathcal{F}, \\mu) \\Rightarrow \\text{Submartingale}(c \\cdot f, \\mathcal{F}, \\mu).$$$

Lean4

theorem smul_nonneg {f : ι → Ω → F} {c : ℝ} (hc : 0 ≤ c) (hf : Submartingale f ℱ μ) : Submartingale (c • f) ℱ μ :=
  by
  rw [← neg_neg (c • f), ← smul_neg]
  exact Supermartingale.neg (hf.neg.smul_nonneg hc)

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