condExp_zero — Mathlib

English

The zero function has conditional expectation zero, under the given measurability conditions.

Русский

Нулевая функция имеет условное ожидание ноль при заданных условиях измеримости.

LaTeX

$$$$\\mu[(0)\\!|m] = 0.$$$$

Lean4

@[simp]
theorem condExp_zero : μ[(0 : α → E)|m] = 0 := by
  by_cases hm : m ≤ m₀
  swap; · rw [condExp_of_not_le hm]
  by_cases hμm : SigmaFinite (μ.trim hm)
  swap; · rw [condExp_of_not_sigmaFinite hm hμm]
  exact condExp_of_stronglyMeasurable hm stronglyMeasurable_zero (integrable_zero _ _ _)

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