Documentation

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

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 contitional expectation of an function is defined in MeasureTheory.Function.ConditionalExpectation.CondexpL2. In this file, we perform two steps.

Main definitions #

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} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] (hm : m m0) [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ) (x : G) :
(MeasureTheory.Lp G 1 μ)

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} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] (hm : m m0) [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (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} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ) (x : G) (y : G) :
    theorem MeasureTheory.condexpIndL1Fin_smul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ) (c : ) (x : G) :
    theorem MeasureTheory.condexpIndL1Fin_smul' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] [NormedSpace F] [SMulCommClass 𝕜 F] (hs : MeasurableSet s) (hμs : μ s ) (c : 𝕜) (x : F) :
    theorem MeasureTheory.norm_condexpIndL1Fin_le {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (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} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ) (hμt : μ t ) (hst : s t = ) (x : G) :
    def MeasureTheory.condexpIndL1 {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (hm : m m0) (μ : MeasureTheory.Measure α) (s : Set α) [MeasureTheory.SigmaFinite (μ.trim hm)] (x : G) :
    (MeasureTheory.Lp G 1 μ)

    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_measure_eq_top {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hμs : μ s = ) (x : G) :
      theorem MeasureTheory.condexpIndL1_of_not_measurableSet {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : ¬MeasurableSet s) (x : G) :
      theorem MeasureTheory.condexpIndL1_add {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (x : G) (y : G) :
      theorem MeasureTheory.condexpIndL1_smul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (c : ) (x : G) :
      theorem MeasureTheory.condexpIndL1_smul' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] [NormedSpace F] [SMulCommClass 𝕜 F] (c : 𝕜) (x : F) :
      theorem MeasureTheory.norm_condexpIndL1_le {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (x : G) :
      MeasureTheory.condexpIndL1 hm μ s x (μ s).toReal * x
      theorem MeasureTheory.continuous_condexpIndL1 {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] :
      Continuous fun (x : G) => MeasureTheory.condexpIndL1 hm μ s x
      theorem MeasureTheory.condexpIndL1_disjoint_union {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ) (hμt : μ t ) (hst : s t = ) (x : G) :
      def MeasureTheory.condexpInd {α : Type u_1} (G : Type u_5) [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (hm : m m0) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite (μ.trim hm)] (s : Set α) :

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

      Equations
      Instances For
        theorem MeasureTheory.condexpInd_ae_eq_condexpIndSMul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] (hm : m m0) [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (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} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ) (x : G) :
        @[simp]
        theorem MeasureTheory.condexpInd_smul' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] [NormedSpace F] [SMulCommClass 𝕜 F] (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} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {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} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] :
        MeasureTheory.condexpInd G hm μ s (μ s).toReal
        theorem MeasureTheory.condexpInd_disjoint_union_apply {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ) (hμt : μ t ) (hst : s t = ) (x : G) :
        theorem MeasureTheory.condexpInd_disjoint_union {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ) (hμt : μ t ) (hst : s t = ) :
        theorem MeasureTheory.setIntegral_condexpInd {α : Type u_1} {G' : Type u_6} [NormedAddCommGroup G'] [NormedSpace G'] [CompleteSpace G'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (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} [NormedAddCommGroup G'] [NormedSpace G'] [CompleteSpace G'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (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} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ) (c : G) :
        theorem MeasureTheory.condexpInd_nonneg {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {E : Type u_8} [NormedLatticeAddCommGroup E] [NormedSpace E] [OrderedSMul E] (hs : MeasurableSet s) (hμs : μ s ) (x : E) (hx : 0 x) :
        def MeasureTheory.condexpL1CLM {α : Type u_1} (F' : Type u_4) [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (hm : m m0) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite (μ.trim hm)] :
        (MeasureTheory.Lp F' 1 μ) →L[] (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} [RCLike 𝕜] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (c : 𝕜) (f : (MeasureTheory.Lp F' 1 μ)) :
          theorem MeasureTheory.condexpL1CLM_indicatorConstLp {α : Type u_1} {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) (x : F') :
          theorem MeasureTheory.condexpL1CLM_indicatorConst {α : Type u_1} {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) (x : F') :
          theorem MeasureTheory.setIntegral_condexpL1CLM_of_measure_ne_top {α : Type u_1} {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (f : (MeasureTheory.Lp F' 1 μ)) (hs : MeasurableSet s) (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} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (f : (MeasureTheory.Lp F' 1 μ)) (hs : MeasurableSet s) (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} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (f : (MeasureTheory.Lp F' 1 μ)) (hs : MeasurableSet s) :
          ∫ (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} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (f : (MeasureTheory.Lp F' 1 μ)) (hs : MeasurableSet s) :
          ∫ (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.condexpL1CLM_lpMeas {α : Type u_1} {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (f : (MeasureTheory.lpMeas F' m 1 μ)) :
          (MeasureTheory.condexpL1CLM F' hm μ) f = f
          def MeasureTheory.condexpL1 {α : Type u_1} {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (hm : m m0) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite (μ.trim hm)] (f : αF') :
          (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} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} (hf : ¬MeasureTheory.Integrable f μ) :
            @[simp]
            theorem MeasureTheory.condexpL1_zero {α : Type u_1} {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] :
            @[simp]
            theorem MeasureTheory.condexpL1_measure_zero {α : Type u_1} {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {f : αF'} (hm : m m0) :
            theorem MeasureTheory.condexpL1_congr_ae {α : Type u_1} {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {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} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (f : αF') :
            theorem MeasureTheory.setIntegral_condexpL1 {α : Type u_1} {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} {s : Set α} (hf : MeasureTheory.Integrable f μ) (hs : MeasurableSet s) :
            ∫ (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} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} {s : Set α} (hf : MeasureTheory.Integrable f μ) (hs : MeasurableSet s) :
            ∫ (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} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} {g : αF'} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
            theorem MeasureTheory.condexpL1_neg {α : Type u_1} {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (f : αF') :
            theorem MeasureTheory.condexpL1_smul {α : Type u_1} {F' : Type u_4} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] (c : 𝕜) (f : αF') :
            theorem MeasureTheory.condexpL1_sub {α : Type u_1} {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace F'] [CompleteSpace F'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} {g : αF'} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
            theorem MeasureTheory.condexpL1_mono {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {E : Type u_8} [NormedLatticeAddCommGroup E] [CompleteSpace E] [NormedSpace E] [OrderedSMul E] {f : αE} {g : αE} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hfg : f ≤ᵐ[μ] g) :
            (MeasureTheory.condexpL1 hm μ f) ≤ᵐ[μ] (MeasureTheory.condexpL1 hm μ g)