# mathlib3documentation

measure_theory.function.conditional_expectation.indicator

# Conditional expectation of indicator functions #

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

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 #

• measure_theory.condexp_indicator: If s is a 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 measure_theory.condexp_ae_eq_restrict_zero {α : Type u_1} {E : Type u_3} {m m0 : measurable_space α} [ E] {μ : measure_theory.measure α} {f : α E} {s : set α} (hs : measurable_set s) (hf : f =ᵐ[μ.restrict s] 0) :
theorem measure_theory.condexp_indicator_aux {α : Type u_1} {E : Type u_3} {m m0 : measurable_space α} [ E] {μ : measure_theory.measure α} {f : α E} {s : set α} (hs : measurable_set s) (hf : f =ᵐ[μ.restrict s] 0) :
(s.indicator f) =ᵐ[μ] s.indicator f)

Auxiliary lemma for condexp_indicator.

theorem measure_theory.condexp_indicator {α : Type u_1} {E : Type u_3} {m m0 : measurable_space α} [ E] {μ : measure_theory.measure α} {f : α E} {s : set α} (hf_int : μ) (hs : measurable_set s) :
(s.indicator f) =ᵐ[μ] s.indicator f)

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 measure_theory.condexp_restrict_ae_eq_restrict {α : Type u_1} {E : Type u_3} {m m0 : measurable_space α} [ E] {μ : measure_theory.measure α} {f : α E} {s : set α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hs_m : measurable_set s) (hf_int : μ) :
(μ.restrict s) f =ᵐ[μ.restrict s]
theorem measure_theory.condexp_ae_eq_restrict_of_measurable_space_eq_on {α : Type u_1} {E : Type u_3} [ E] {f : α E} {s : set α} {m m₂ m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (hm₂ : m₂ m0) [measure_theory.sigma_finite (μ.trim hm)] [measure_theory.sigma_finite (μ.trim hm₂)] (hs_m : measurable_set s) (hs : (t : set α), measurable_set (s t) measurable_set (s t)) :

If the restriction to a 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₂].