stronglyMeasurable

Mathlib.Probability.Martingale.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Martingale.stronglyMeasurable

English

For a martingale f and i ≤ j, the conditional expectation μ[f j|ℱ i] equals f i almost everywhere.

Русский

Для мартингейла f и i ≤ j условное ожидание μ[f j|ℱ i] равно f i почти наверняка.

LaTeX

$$$\\mu[f(j) \\mid \\mathcal{F}(i)] =_{\\mathrm{ae}} f(i)\\quad(i \\le j)$$$

Lean4

protected theorem stronglyMeasurable (hf : Martingale f ℱ μ) (i : ι) : StronglyMeasurable[ℱ i] (f i) :=
  hf.adapted i

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

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

Разделы

Аффилиация

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