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: Ifsis anm-measurable set, then the conditional expectation of the indicator function ofsis almost everywhere equal to the indicator ofsof 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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{s : Set α}
(hs : MeasurableSet s)
(hf : (μ.restrict s).ae.EventuallyEq f 0)
:
(μ.restrict s).ae.EventuallyEq (MeasureTheory.condexp m μ f) 0
theorem
MeasureTheory.condexp_indicator_aux
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{s : Set α}
(hs : MeasurableSet s)
(hf : (μ.restrict sᶜ).ae.EventuallyEq f 0)
:
μ.ae.EventuallyEq (MeasureTheory.condexp m μ (s.indicator f)) (s.indicator (MeasureTheory.condexp m μ f))
Auxiliary lemma for condexp_indicator.
theorem
MeasureTheory.condexp_indicator
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{s : Set α}
(hf_int : MeasureTheory.Integrable f μ)
(hs : MeasurableSet s)
:
μ.ae.EventuallyEq (MeasureTheory.condexp m μ (s.indicator f)) (s.indicator (MeasureTheory.condexp m μ 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
MeasureTheory.condexp_restrict_ae_eq_restrict
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{s : Set α}
(hm : m ≤ m0)
[MeasureTheory.SigmaFinite (μ.trim hm)]
(hs_m : MeasurableSet s)
(hf_int : MeasureTheory.Integrable f μ)
:
(μ.restrict s).ae.EventuallyEq (MeasureTheory.condexp m (μ.restrict s) f) (MeasureTheory.condexp m μ f)
theorem
MeasureTheory.condexp_ae_eq_restrict_of_measurableSpace_eq_on
{α : Type u_1}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : α → E}
{s : Set α}
{m : MeasurableSpace α}
{m₂ : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(hm₂ : m₂ ≤ m0)
[MeasureTheory.SigmaFinite (μ.trim hm)]
[MeasureTheory.SigmaFinite (μ.trim hm₂)]
(hs_m : MeasurableSet s)
(hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t))
:
(μ.restrict s).ae.EventuallyEq (MeasureTheory.condexp m μ f) (MeasureTheory.condexp m₂ μ f)
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₂].