condExp_add — Mathlib

English

Conditional expectation respects addition: μ[(f+g)|m] equals μ[f|m] + μ[g|m] a.e., for integrable f and g.

Русский

Условное ожидание сохраняет сложение: μ[(f+g)|m] = μ[f|m] + μ[g|m] a.e. для интегрируемых f и g.

LaTeX

$$$$\\mu[f+g|m] =_{\\text{ae}} \\mu[f|m] + \\mu[g|m].$$$$

Lean4

theorem condExp_add (hf : Integrable f μ) (hg : Integrable g μ) (m : MeasurableSpace α) :
    μ[f + g|m] =ᵐ[μ] μ[f|m] + μ[g|m] := by
  by_cases hm : m ≤ m₀
  swap; · simp_rw [condExp_of_not_le hm]; simp
  by_cases hμm : SigmaFinite (μ.trim hm)
  swap; · simp_rw [condExp_of_not_sigmaFinite hm hμm]; simp
  refine (condExp_ae_eq_condExpL1 hm _).trans ?_
  rw [condExpL1_add hf hg]
  exact (coeFn_add _ _).trans ((condExp_ae_eq_condExpL1 hm _).symm.add (condExp_ae_eq_condExpL1 hm _).symm)

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