sub_supermartingale — Mathlib

English

If hf is a Submartingale, then the integrals of each component are finite, i.e., integrable on μ.

Русский

Если hf — субмартингал, то интегралы по каждой компоненте конечны, то есть интегрируемы по μ.

LaTeX

$$$\mathrm{Submartingale}(f,\mathcal{F},\mu) \Rightarrow \forall i, \mathrm{Integrable}(f(i),\mu)$$$

Lean4

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

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