mathlib documentation


Probabilistic properties of the conditional expectation #

This file contains some properties about the conditional expectation which does not belong in the main conditional expectation file.

Main result #

theorem measure_theory.condexp_indep_eq {Ω : Type u_1} {E : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] {m₁ m₂ m : measurable_space Ω} {μ : measure_theory.measure Ω} {f : Ω → E} (hle₁ : m₁ m) (hle₂ : m₂ m) [measure_theory.sigma_finite (μ.trim hle₂)] (hf : measure_theory.strongly_measurable f) (hindp : probability_theory.indep m₁ m₂ μ) :
measure_theory.condexp m₂ μ f =ᵐ[μ] λ (x : Ω), (x : Ω), f x μ

If m₁, m₂ are independent σ-algebras and f is m₁-measurable, then 𝔼[f | m₂] = 𝔼[f] almost everywhere.