condExp_sub — Mathlib

English

If f and g are integrable, the conditional expectation preserves subtraction: E[f−g|m] = E[f|m] − E[g|m], a.e.

Русский

Если f и g интегрируемы, то E[f−g|m] = E[f|m] − E[g|m] почти наверняка.

LaTeX

$$$\mu[f - g|m] =^{\mathrm{ae}}_{\mu} \mu[f|m] - \mu[g|m]$$$

Lean4

theorem condExp_sub (hf : Integrable f μ) (hg : Integrable g μ) (m : MeasurableSpace α) :
    μ[f - g|m] =ᵐ[μ] μ[f|m] - μ[g|m] := by
  simp_rw [sub_eq_add_neg]
  exact (condExp_add hf hg.neg _).trans (EventuallyEq.rfl.add (condExp_neg ..))

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