smul_nonpos — Mathlib

English

Let f be a submartingale. If c ≤ 0, then the scaled process c · f is a supermartingale.

Русский

Пусть f — субмартингал. Тогда для c ≤ 0 процесс c · f является супермартингалом.

LaTeX

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

Lean4

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

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