integrable

Mathlib.Probability.Martingale.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Submartingale.integrable

English

For a Submartingale, each component f(i) is integrable with respect to μ.

Русский

Для субмартингала каждый компонент f(i) интегрируем по μ.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru