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 #

source
theorem MeasureTheory.condExp_ae_eq_restrict_zero {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : Measure α} {f : α → E} {s : Set α} (hs : MeasurableSet s) (hf : f =ᶠ[ae (μ.restrict s)] 0) :
condExp m μ f =ᶠ[ae (μ.restrict s)] 0
source
@[deprecated MeasureTheory.condExp_ae_eq_restrict_zero (since := "2025-01-21")]
theorem MeasureTheory.condexp_ae_eq_restrict_zero {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : Measure α} {f : α → E} {s : Set α} (hs : MeasurableSet s) (hf : f =ᶠ[ae (μ.restrict s)] 0) :
condExp m μ f =ᶠ[ae (μ.restrict s)] 0

Alias of MeasureTheory.condExp_ae_eq_restrict_zero.

source
theorem MeasureTheory.condExp_indicator_aux {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : Measure α} {f : α → E} {s : Set α} (hs : MeasurableSet s) (hf : f =ᶠ[ae (μ.restrict sᶜ)] 0) :
condExp m μ (s.indicator f) =ᶠ[ae μ] s.indicator (condExp m μ f)

Auxiliary lemma for condExp_indicator.

source
@[deprecated MeasureTheory.condExp_indicator_aux (since := "2025-01-21")]
theorem MeasureTheory.condexp_indicator_aux {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : Measure α} {f : α → E} {s : Set α} (hs : MeasurableSet s) (hf : f =ᶠ[ae (μ.restrict sᶜ)] 0) :
condExp m μ (s.indicator f) =ᶠ[ae μ] s.indicator (condExp m μ f)

Alias of MeasureTheory.condExp_indicator_aux.

Auxiliary lemma for condExp_indicator.

source
theorem MeasureTheory.condExp_indicator {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : Measure α} {f : α → E} {s : Set α} (hf_int : Integrable f μ) (hs : MeasurableSet s) :
condExp m μ (s.indicator f) =ᶠ[ae μ] s.indicator (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.

source
@[deprecated MeasureTheory.condExp_indicator (since := "2025-01-21")]
theorem MeasureTheory.condexp_indicator {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : Measure α} {f : α → E} {s : Set α} (hf_int : Integrable f μ) (hs : MeasurableSet s) :
condExp m μ (s.indicator f) =ᶠ[ae μ] s.indicator (condExp m μ f)

Alias of MeasureTheory.condExp_indicator.

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.

source
theorem MeasureTheory.condExp_restrict_ae_eq_restrict {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : Measure α} {f : α → E} {s : Set α} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs_m : MeasurableSet s) (hf_int : Integrable f μ) :
condExp m (μ.restrict s) f =ᶠ[ae (μ.restrict s)] condExp m μ f
source
@[deprecated MeasureTheory.condExp_restrict_ae_eq_restrict (since := "2025-01-21")]
theorem MeasureTheory.condexp_restrict_ae_eq_restrict {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : Measure α} {f : α → E} {s : Set α} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs_m : MeasurableSet s) (hf_int : Integrable f μ) :
condExp m (μ.restrict s) f =ᶠ[ae (μ.restrict s)] condExp m μ f

Alias of MeasureTheory.condExp_restrict_ae_eq_restrict.

source
theorem MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : α → E} {s : Set α} {m m₂ m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (hm₂ : m₂ ≤ m0) [SigmaFinite (μ.trim hm)] [SigmaFinite (μ.trim hm₂)] (hs_m : MeasurableSet s) (hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)) :
condExp m μ f =ᶠ[ae (μ.restrict s)] 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₂].

source
@[deprecated MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on (since := "2025-01-21")]
theorem MeasureTheory.condexp_ae_eq_restrict_of_measurableSpace_eq_on {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : α → E} {s : Set α} {m m₂ m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (hm₂ : m₂ ≤ m0) [SigmaFinite (μ.trim hm)] [SigmaFinite (μ.trim hm₂)] (hs_m : MeasurableSet s) (hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)) :
condExp m μ f =ᶠ[ae (μ.restrict s)] condExp m₂ μ f

Alias of MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on.

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₂].