# Documentation

Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

# Conditional expectation of indicator functions #

This file proves some results about the conditional expectation of an indicator function and as a corollary, also proves several results about the behaviour of the conditional expectation on a restricted measure.

## Main result #

• MeasureTheory.condexp_indicator: If s is an m-measurable set, then the conditional expectation of the indicator function of s is almost everywhere equal to the indicator of s of the conditional expectation. Namely, 𝔼[s.indicator f | m] = s.indicator 𝔼[f | m] a.e.
theorem MeasureTheory.condexp_ae_eq_restrict_zero {α : Type u_1} {E : Type u_3} {m : } {m0 : } [] [] {μ : } {f : αE} {s : Set α} (hs : ) (hf : ) :
theorem MeasureTheory.condexp_indicator_aux {α : Type u_1} {E : Type u_3} {m : } {m0 : } [] [] {μ : } {f : αE} {s : Set α} (hs : ) (hf : ) :

Auxiliary lemma for condexp_indicator.

theorem MeasureTheory.condexp_indicator {α : Type u_1} {E : Type u_3} {m : } {m0 : } [] [] {μ : } {f : αE} {s : Set α} (hf_int : ) (hs : ) :

The conditional expectation of the indicator of a function over an m-measurable set with respect to the σ-algebra m is a.e. equal to the indicator of the conditional expectation.

theorem MeasureTheory.condexp_restrict_ae_eq_restrict {α : Type u_1} {E : Type u_3} {m : } {m0 : } [] [] {μ : } {f : αE} {s : Set α} (hm : m m0) (hs_m : ) (hf_int : ) :
theorem MeasureTheory.condexp_ae_eq_restrict_of_measurableSpace_eq_on {α : Type u_1} {E : Type u_3} [] [] {f : αE} {s : Set α} {m : } {m₂ : } {m0 : } {μ : } (hm : m m0) (hm₂ : m₂ m0) (hs_m : ) (hs : ∀ (t : Set α), MeasurableSet (s t) MeasurableSet (s t)) :

If the restriction to an m-measurable set s of a σ-algebra m is equal to the restriction to s of another σ-algebra m₂ (hypothesis hs), then μ[f | m] =ᵐ[μ.restrict s] μ[f | m₂].