smul_nonpos — Mathlib

English

Let f be a (vector-valued) supermartingale with respect to a filtration and a measure μ. If c ≤ 0 is a real number, then the scaled process c · f is a submartingale with respect to the same filtration and measure.

Русский

Пусть f является (векторной) супермартингалом относительно той же фильтрации и меры μ. Тогда процесс c · f, где c ≤ 0, является субмартингалом.

LaTeX

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

Lean4

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

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