integrable — Mathlib

English

Let f be an E-valued process indexed by ι which is a supermartingale with respect to the filtration ℱ and measure μ. Then for every index i, the random variable f(i) is μ-integrable.

Русский

Пусть f — процесс, принимающий значения в E, индексируемый по ι, являющийся суперmartingale относительно фильтрации ℱ и меры μ. Тогда для каждого i множество f(i) интегрируемо по μ.

LaTeX

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

Lean4

protected theorem integrable [LE E] (hf : Supermartingale f ℱ μ) (i : ι) : Integrable (f i) μ :=
  hf.2.2 i

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