condExp_ae_eq

Mathlib.Probability.Martingale.Basic

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

English

If i ≤ j and s ∈ ℱ i is measurable, then the integrals of f i and f j over s are equal.

Русский

Пусть i ≤ j и s измеримо в ℱ i; тогда интегралы по s от f i и f j равны.

LaTeX

$$$\\int_{s} f(i) \\, d\\mu = \\int_{s} f(j) \\, d\\mu$$$

Lean4

theorem condExp_ae_eq (hf : Martingale f ℱ μ) {i j : ι} (hij : i ≤ j) : μ[f j|ℱ i] =ᵐ[μ] f i :=
  hf.2 i j hij

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

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

Разделы

Аффилиация

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