Probabilistic properties of the conditional expectation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main result #

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

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.