neg — Mathlib

English

If f is a submartingale, then the negated process −f is a supermartingale.

Русский

Если f — субмартингал, то отрицание процесса −f является суперmartингалом.

LaTeX

$$$\mathrm{Submartingale}(f,\mathcal{F},\mu) \Rightarrow \mathrm{Supermartingale}(-f,\mathcal{F},\mu)$$$

Lean4

theorem neg [Preorder E] [AddLeftMono E] (hf : Supermartingale f ℱ μ) : Submartingale (-f) ℱ μ :=
  by
  refine ⟨hf.1.neg, fun i j hij => ?_, fun i => (hf.2.2 i).neg⟩
  refine EventuallyLE.trans ?_ (condExp_neg ..).symm.le
  filter_upwards [hf.2.1 i j hij] with _ _
  simpa

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