neg — Mathlib

English

The pointwise supremum (or maximum) of two submartingales is a submartingale.

Русский

Пусть супремейк двух субмартингалов по точкам; он сам является субмартингалом.

LaTeX

$$$\mathrm{Submartingale}(f,\mathcal{F},\mu) \land \mathrm{Submartingale}(g,\mathcal{F},\mu) \Rightarrow \mathrm{Submartingale}(\,f \sqcup g\, ,\mathcal{F},\mu)$$$

Lean4

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

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