Conditional expectation in L1 #

This file contains two more steps of the construction of the conditional expectation, which is completed in MeasureTheory.Function.ConditionalExpectation.Basic. See that file for a description of the full process.

The conditional expectation of an L² function is defined in MeasureTheory.Function.ConditionalExpectation.CondexpL2. In this file, we perform two steps.

• Show that the conditional expectation of the indicator of a measurable set with finite measure is integrable and define a map Set α → (E →L[ℝ] (α →₁[μ] E)) which to a set associates a linear map. That linear map sends x ∈ E to the conditional expectation of the indicator of the set with value x.
• Extend that map to condexpL1CLM : (α →₁[μ] E) →L[ℝ] (α →₁[μ] E). This is done using the same construction as the Bochner integral (see the file MeasureTheory/Integral/SetToL1).

Main definitions #

• condexpL1: Conditional expectation of a function as a linear map from L1 to itself.

Conditional expectation of an indicator as a continuous linear map. #

The goal of this section is to build condexpInd (hm : m ≤ m0) (μ : Measure α) (s : Set s) : G →L[ℝ] α →₁[μ] G, which takes x : G to the conditional expectation of the indicator of the set s with value x, seen as an element of α →₁[μ] G.

def MeasureTheory.condexpIndL1Fin {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] (hm : m m0) [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (hμs : μ s ) (x : G) :
{ x : α →ₘ[μ] G // x }

Conditional expectation of the indicator of a measurable set with finite measure, as a function in L1.

Equations
Instances For
theorem MeasureTheory.condexpIndL1Fin_ae_eq_condexpIndSMul {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] (hm : m m0) [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (hμs : μ s ) (x : G) :
(MeasureTheory.condexpIndL1Fin hm hs hμs x) =ᵐ[μ] (MeasureTheory.condexpIndSMul hm hs hμs x)
theorem MeasureTheory.condexpIndL1Fin_add {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (hμs : μ s ) (x : G) (y : G) :
theorem MeasureTheory.condexpIndL1Fin_smul {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (hμs : μ s ) (c : ) (x : G) :
theorem MeasureTheory.condexpIndL1Fin_smul' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_7} [] [] {m : } {m0 : } {μ : } {s : Set α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] [] [] (hs : ) (hμs : μ s ) (c : 𝕜) (x : F) :
theorem MeasureTheory.norm_condexpIndL1Fin_le {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (hμs : μ s ) (x : G) :
MeasureTheory.condexpIndL1Fin hm hs hμs x (μ s).toReal * x
theorem MeasureTheory.condexpIndL1Fin_disjoint_union {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} {t : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (ht : ) (hμs : μ s ) (hμt : μ t ) (hst : s t = ) (x : G) :
def MeasureTheory.condexpIndL1 {α : Type u_1} {G : Type u_5} [] {m : } {m0 : } (hm : m m0) (μ : ) (s : Set α) [MeasureTheory.SigmaFinite (μ.trim hm)] (x : G) :
{ x : α →ₘ[μ] G // x }

Conditional expectation of the indicator of a set, as a function in L1. Its value for sets which are not both measurable and of finite measure is not used: we set it to 0.

Equations
Instances For
theorem MeasureTheory.condexpIndL1_of_measurableSet_of_measure_ne_top {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (hμs : μ s ) (x : G) :
theorem MeasureTheory.condexpIndL1_of_measure_eq_top {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hμs : μ s = ) (x : G) :
= 0
theorem MeasureTheory.condexpIndL1_of_not_measurableSet {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (x : G) :
= 0
theorem MeasureTheory.condexpIndL1_add {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (x : G) (y : G) :
theorem MeasureTheory.condexpIndL1_smul {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (c : ) (x : G) :
theorem MeasureTheory.condexpIndL1_smul' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_7} [] [] {m : } {m0 : } {μ : } {s : Set α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] [] [] (c : 𝕜) (x : F) :
theorem MeasureTheory.norm_condexpIndL1_le {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (x : G) :
(μ s).toReal * x
theorem MeasureTheory.continuous_condexpIndL1 {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] :
Continuous fun (x : G) =>
theorem MeasureTheory.condexpIndL1_disjoint_union {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} {t : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (ht : ) (hμs : μ s ) (hμt : μ t ) (hst : s t = ) (x : G) :
def MeasureTheory.condexpInd {α : Type u_1} (G : Type u_5) [] {m : } {m0 : } (hm : m m0) (μ : ) [MeasureTheory.SigmaFinite (μ.trim hm)] (s : Set α) :
G →L[] { x : α →ₘ[μ] G // x }

Conditional expectation of the indicator of a set, as a linear map from G to L1.

Equations
• = { toFun := , map_add' := , map_smul' := , cont := }
Instances For
theorem MeasureTheory.condexpInd_ae_eq_condexpIndSMul {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] (hm : m m0) [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (hμs : μ s ) (x : G) :
((MeasureTheory.condexpInd G hm μ s) x) =ᵐ[μ] (MeasureTheory.condexpIndSMul hm hs hμs x)
theorem MeasureTheory.aestronglyMeasurable'_condexpInd {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (hμs : μ s ) (x : G) :
@[simp]
theorem MeasureTheory.condexpInd_empty {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] :
= 0
theorem MeasureTheory.condexpInd_smul' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_7} [] [] {m : } {m0 : } {μ : } {s : Set α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] [] [] (c : 𝕜) (x : F) :
(MeasureTheory.condexpInd F hm μ s) (c x) = c (MeasureTheory.condexpInd F hm μ s) x
theorem MeasureTheory.norm_condexpInd_apply_le {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (x : G) :
(MeasureTheory.condexpInd G hm μ s) x (μ s).toReal * x
theorem MeasureTheory.norm_condexpInd_le {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] :
(μ s).toReal
theorem MeasureTheory.condexpInd_disjoint_union_apply {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} {t : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (ht : ) (hμs : μ s ) (hμt : μ t ) (hst : s t = ) (x : G) :
theorem MeasureTheory.condexpInd_disjoint_union {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} {t : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (ht : ) (hμs : μ s ) (hμt : μ t ) (hst : s t = ) :
theorem MeasureTheory.dominatedFinMeasAdditive_condexpInd {α : Type u_1} (G : Type u_5) {m : } {m0 : } [] (hm : m m0) (μ : ) [MeasureTheory.SigmaFinite (μ.trim hm)] :
theorem MeasureTheory.setIntegral_condexpInd {α : Type u_1} {G' : Type u_6} [] [] [] {m : } {m0 : } {μ : } {s : Set α} {t : Set α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (ht : ) (hμs : μ s ) (hμt : μ t ) (x : G') :
∫ (a : α) in s, ((MeasureTheory.condexpInd G' hm μ t) x) aμ = (μ (t s)).toReal x
@[deprecated MeasureTheory.setIntegral_condexpInd]
theorem MeasureTheory.set_integral_condexpInd {α : Type u_1} {G' : Type u_6} [] [] [] {m : } {m0 : } {μ : } {s : Set α} {t : Set α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (ht : ) (hμs : μ s ) (hμt : μ t ) (x : G') :
∫ (a : α) in s, ((MeasureTheory.condexpInd G' hm μ t) x) aμ = (μ (t s)).toReal x

Alias of MeasureTheory.setIntegral_condexpInd.

theorem MeasureTheory.condexpInd_of_measurable {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ) (hμs : μ s ) (c : G) :
theorem MeasureTheory.condexpInd_nonneg {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {E : Type u_8} [] [] (hs : ) (hμs : μ s ) (x : E) (hx : 0 x) :
def MeasureTheory.condexpL1CLM {α : Type u_1} (F' : Type u_4) [] [] [] {m : } {m0 : } (hm : m m0) (μ : ) [MeasureTheory.SigmaFinite (μ.trim hm)] :
{ x : α →ₘ[μ] F' // x MeasureTheory.Lp F' 1 μ } →L[] { x : α →ₘ[μ] F' // x MeasureTheory.Lp F' 1 μ }

Conditional expectation of a function as a linear map from α →₁[μ] F' to itself.

Equations
Instances For
theorem MeasureTheory.condexpL1CLM_smul {α : Type u_1} {F' : Type u_4} {𝕜 : Type u_7} [] [] [NormedSpace 𝕜 F'] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (c : 𝕜) (f : { x : α →ₘ[μ] F' // x MeasureTheory.Lp F' 1 μ }) :
theorem MeasureTheory.condexpL1CLM_indicatorConstLp {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (hs : ) (hμs : μ s ) (x : F') :
theorem MeasureTheory.condexpL1CLM_indicatorConst {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (hs : ) (hμs : μ s ) (x : F') :
theorem MeasureTheory.setIntegral_condexpL1CLM_of_measure_ne_top {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (f : { x : α →ₘ[μ] F' // x MeasureTheory.Lp F' 1 μ }) (hs : ) (hμs : μ s ) :
∫ (x : α) in s, ((MeasureTheory.condexpL1CLM F' hm μ) f) xμ = ∫ (x : α) in s, f xμ

Auxiliary lemma used in the proof of setIntegral_condexpL1CLM.

@[deprecated MeasureTheory.setIntegral_condexpL1CLM_of_measure_ne_top]
theorem MeasureTheory.set_integral_condexpL1CLM_of_measure_ne_top {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (f : { x : α →ₘ[μ] F' // x MeasureTheory.Lp F' 1 μ }) (hs : ) (hμs : μ s ) :
∫ (x : α) in s, ((MeasureTheory.condexpL1CLM F' hm μ) f) xμ = ∫ (x : α) in s, f xμ

Alias of MeasureTheory.setIntegral_condexpL1CLM_of_measure_ne_top.

Auxiliary lemma used in the proof of setIntegral_condexpL1CLM.

theorem MeasureTheory.setIntegral_condexpL1CLM {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (f : { x : α →ₘ[μ] F' // x MeasureTheory.Lp F' 1 μ }) (hs : ) :
∫ (x : α) in s, ((MeasureTheory.condexpL1CLM F' hm μ) f) xμ = ∫ (x : α) in s, f xμ

The integral of the conditional expectation condexpL1CLM over an m-measurable set is equal to the integral of f on that set. See also setIntegral_condexp, the similar statement for condexp.

@[deprecated MeasureTheory.setIntegral_condexpL1CLM]
theorem MeasureTheory.set_integral_condexpL1CLM {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (f : { x : α →ₘ[μ] F' // x MeasureTheory.Lp F' 1 μ }) (hs : ) :
∫ (x : α) in s, ((MeasureTheory.condexpL1CLM F' hm μ) f) xμ = ∫ (x : α) in s, f xμ

Alias of MeasureTheory.setIntegral_condexpL1CLM.

The integral of the conditional expectation condexpL1CLM over an m-measurable set is equal to the integral of f on that set. See also setIntegral_condexp, the similar statement for condexp.

theorem MeasureTheory.aestronglyMeasurable'_condexpL1CLM {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (f : { x : α →ₘ[μ] F' // x MeasureTheory.Lp F' 1 μ }) :
theorem MeasureTheory.condexpL1CLM_lpMeas {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (f : { x : { x : α →ₘ[μ] F' // x MeasureTheory.Lp F' 1 μ } // x }) :
(MeasureTheory.condexpL1CLM F' hm μ) f = f
theorem MeasureTheory.condexpL1CLM_of_aestronglyMeasurable' {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (f : { x : α →ₘ[μ] F' // x MeasureTheory.Lp F' 1 μ }) (hfm : ) :
def MeasureTheory.condexpL1 {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } (hm : m m0) (μ : ) [MeasureTheory.SigmaFinite (μ.trim hm)] (f : αF') :
{ x : α →ₘ[μ] F' // x MeasureTheory.Lp F' 1 μ }

Conditional expectation of a function, in L1. Its value is 0 if the function is not integrable. The function-valued condexp should be used instead in most cases.

Equations
Instances For
theorem MeasureTheory.condexpL1_undef {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} (hf : ) :
= 0
theorem MeasureTheory.condexpL1_eq {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} (hf : ) :
@[simp]
theorem MeasureTheory.condexpL1_zero {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] :
= 0
@[simp]
theorem MeasureTheory.condexpL1_measure_zero {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {f : αF'} (hm : m m0) :
= 0
theorem MeasureTheory.aestronglyMeasurable'_condexpL1 {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} :
theorem MeasureTheory.condexpL1_congr_ae {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {f : αF'} {g : αF'} (hm : m m0) [MeasureTheory.SigmaFinite (μ.trim hm)] (h : f =ᵐ[μ] g) :
=
theorem MeasureTheory.integrable_condexpL1 {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (f : αF') :
theorem MeasureTheory.setIntegral_condexpL1 {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} {s : Set α} (hf : ) (hs : ) :
∫ (x : α) in s, (MeasureTheory.condexpL1 hm μ f) xμ = ∫ (x : α) in s, f xμ

The integral of the conditional expectation condexpL1 over an m-measurable set is equal to the integral of f on that set. See also setIntegral_condexp, the similar statement for condexp.

@[deprecated MeasureTheory.setIntegral_condexpL1]
theorem MeasureTheory.set_integral_condexpL1 {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} {s : Set α} (hf : ) (hs : ) :
∫ (x : α) in s, (MeasureTheory.condexpL1 hm μ f) xμ = ∫ (x : α) in s, f xμ

Alias of MeasureTheory.setIntegral_condexpL1.

The integral of the conditional expectation condexpL1 over an m-measurable set is equal to the integral of f on that set. See also setIntegral_condexp, the similar statement for condexp.

theorem MeasureTheory.condexpL1_add {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} {g : αF'} (hf : ) (hg : ) :
theorem MeasureTheory.condexpL1_neg {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (f : αF') :
theorem MeasureTheory.condexpL1_smul {α : Type u_1} {F' : Type u_4} {𝕜 : Type u_7} [] [] [NormedSpace 𝕜 F'] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (c : 𝕜) (f : αF') :
theorem MeasureTheory.condexpL1_sub {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} {g : αF'} (hf : ) (hg : ) :
theorem MeasureTheory.condexpL1_of_aestronglyMeasurable' {α : Type u_1} {F' : Type u_4} [] [] [] {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} (hfm : ) (hfi : ) :
(MeasureTheory.condexpL1 hm μ f) =ᵐ[μ] f
theorem MeasureTheory.condexpL1_mono {α : Type u_1} {m : } {m0 : } {μ : } {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {E : Type u_8} [] [] [] {f : αE} {g : αE} (hf : ) (hg : ) (hfg : f ≤ᵐ[μ] g) :
(MeasureTheory.condexpL1 hm μ f) ≤ᵐ[μ] (MeasureTheory.condexpL1 hm μ g)