sub_martingale — Mathlib

English

If a process f is adapted and integrable, then for i ≤ j and measurable s with respect to ℱ_i, the integrated inequality holds between f_i and f_j over s.

Русский

Если процесс адаптирован и интегрируем, то при i ≤ j и измеримом s относительно ℱ_i выполняется неравенство на интеграле по s между f_i и f_j.

LaTeX

$$$\mathrm{Adapted}(\mathcal{F}, f) \land \forall i,\mathrm{Integrable}(f(i),\mu) \land \forall i\le j, \forall s, \mathrm{MeasurableSet}_{\mathcal{F}_i}(s) \Rightarrow \int_s f_i \le \int_s f_j$$$

Lean4

theorem sub_martingale [Preorder E] [AddLeftMono E] (hf : Supermartingale f ℱ μ) (hg : Martingale g ℱ μ) :
    Supermartingale (f - g) ℱ μ :=
  hf.sub_submartingale hg.submartingale

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