add — Mathlib

English

If f and g are submartingales, then f+g is a submartingale.

Русский

Если f и g — субмартингалы, то сумма f+g — субмартингал.

LaTeX

$$$\mathrm{Submartingale}(f,\mathcal{F},\mu) \rightarrow \mathrm{Submartingale}(f+g,\mathcal{F},\mu)$$$

Lean4

theorem add [Preorder E] [AddLeftMono E] (hf : Submartingale f ℱ μ) (hg : Submartingale g ℱ μ) :
    Submartingale (f + g) ℱ μ :=
  by
  refine ⟨hf.1.add hg.1, fun i j hij => ?_, fun i => (hf.2.2 i).add (hg.2.2 i)⟩
  refine EventuallyLE.trans ?_ (condExp_add (hf.integrable j) (hg.integrable j) _).symm.le
  filter_upwards [hf.2.1 i j hij, hg.2.1 i j hij]
  intros
  refine add_le_add ?_ ?_ <;> assumption

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