sub_submartingale — Mathlib

English

Under sigma-finite filtration, the submartingale inequality extends to integrals over measurable sets with i ≤ j.

Русский

При сигма-финитной фильтрации неравенство для субмартингала распространяется на интегралы по измеримым множествам при i ≤ j.

LaTeX

$$$[\SigmaFiniteFiltration \mu \mathcal{F}] \Rightarrow \mathrm{SetIntegralLe}(f,\mathcal{F},\mu)$$$

Lean4

theorem sub_submartingale [Preorder E] [AddLeftMono E] (hf : Supermartingale f ℱ μ) (hg : Submartingale g ℱ μ) :
    Supermartingale (f - g) ℱ μ := by rw [sub_eq_add_neg]; exact hf.add hg.neg

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