Documentation

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Conditional expectation in L2 #

This file contains one step 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.

We build the conditional expectation of an L² function, as an element of L². This is the orthogonal projection on the subspace of almost everywhere m-measurable functions.

Main definitions #

Implementation notes #

Most of the results in this file are valid for a complete real normed space F. However, some lemmas also use 𝕜 : IsROrC:

noncomputable def MeasureTheory.condexpL2 {α : Type u_1} (E : Type u_2) (𝕜 : Type u_7) [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) :
{ x // x ∈ MeasureTheory.Lp E 2 } →L[𝕜] { x // x ∈ MeasureTheory.lpMeas E 𝕜 m 2 μ }

Conditional expectation of a function in L2 with respect to a sigma-algebra

Instances For
    theorem MeasureTheory.aeStronglyMeasurable'_condexpL2 {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : { x // x ∈ MeasureTheory.Lp E 2 }) :
    MeasureTheory.AEStronglyMeasurable' m (↑↑↑(↑(MeasureTheory.condexpL2 E 𝕜 hm) f)) μ
    theorem MeasureTheory.integrableOn_condexpL2_of_measure_ne_top {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hμs : ↑↑μ s ≠ ⊤) (f : { x // x ∈ MeasureTheory.Lp E 2 }) :
    MeasureTheory.IntegrableOn (↑↑↑(↑(MeasureTheory.condexpL2 E 𝕜 hm) f)) s
    theorem MeasureTheory.integrable_condexpL2_of_isFiniteMeasure {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] {f : { x // x ∈ MeasureTheory.Lp E 2 }} :
    MeasureTheory.Integrable ↑↑↑(↑(MeasureTheory.condexpL2 E 𝕜 hm) f)
    theorem MeasureTheory.norm_condexpL2_le_one {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) :
    theorem MeasureTheory.norm_condexpL2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : { x // x ∈ MeasureTheory.Lp E 2 }) :
    theorem MeasureTheory.snorm_condexpL2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : { x // x ∈ MeasureTheory.Lp E 2 }) :
    MeasureTheory.snorm (↑↑↑(↑(MeasureTheory.condexpL2 E 𝕜 hm) f)) 2 μ ≤ MeasureTheory.snorm (↑↑f) 2 μ
    theorem MeasureTheory.norm_condexpL2_coe_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : { x // x ∈ MeasureTheory.Lp E 2 }) :
    theorem MeasureTheory.inner_condexpL2_left_eq_right {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : { x // x ∈ MeasureTheory.Lp E 2 }} {g : { x // x ∈ MeasureTheory.Lp E 2 }} :
    inner (↑(↑(MeasureTheory.condexpL2 E 𝕜 hm) f)) g = inner f ↑(↑(MeasureTheory.condexpL2 E 𝕜 hm) g)
    theorem MeasureTheory.condexpL2_indicator_of_measurable {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (c : E) :
    ↑(↑(MeasureTheory.condexpL2 E 𝕜 hm) (MeasureTheory.indicatorConstLp 2 (hm s hs) hμs c)) = MeasureTheory.indicatorConstLp 2 (hm s hs) hμs c
    theorem MeasureTheory.inner_condexpL2_eq_inner_fun {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : { x // x ∈ MeasureTheory.Lp E 2 }) (g : { x // x ∈ MeasureTheory.Lp E 2 }) (hg : MeasureTheory.AEStronglyMeasurable' m (↑↑g) μ) :
    inner (↑(↑(MeasureTheory.condexpL2 E 𝕜 hm) f)) g = inner f g
    theorem MeasureTheory.integral_condexpL2_eq_of_fin_meas_real {α : Type u_1} {𝕜 : Type u_7} [IsROrC 𝕜] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0} (f : { x // x ∈ MeasureTheory.Lp 𝕜 2 }) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) :
    ∫ (x : α) in s, ↑↑↑(↑(MeasureTheory.condexpL2 𝕜 𝕜 hm) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
    theorem MeasureTheory.lintegral_nnnorm_condexpL2_le {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (f : { x // x ∈ MeasureTheory.Lp ℝ 2 }) :
    ∫⁻ (x : α) in s, ↑‖↑↑↑(↑(MeasureTheory.condexpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ
    theorem MeasureTheory.condexpL2_ae_eq_zero_of_ae_eq_zero {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) {f : { x // x ∈ MeasureTheory.Lp ℝ 2 }} (hf : ↑↑f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)] 0) :
    theorem MeasureTheory.lintegral_nnnorm_condexpL2_indicator_le_real {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (ht : MeasurableSet t) (hμt : ↑↑μ t ≠ ⊤) :
    ∫⁻ (a : α) in t, ↑‖↑↑↑(↑(MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ ≤ ↑↑μ (s ∩ t)
    theorem MeasureTheory.condexpL2_const_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : { x // x ∈ MeasureTheory.Lp E 2 }) (c : E) :
    ↑↑↑(↑(MeasureTheory.condexpL2 𝕜 𝕜 hm) (MeasureTheory.Memℒp.toLp (fun a => inner c (↑↑f a)) (_ : MeasureTheory.Memℒp (fun a => inner c (↑↑f a)) 2))) =ᶠ[MeasureTheory.Measure.ae μ] fun a => inner c (↑↑↑(↑(MeasureTheory.condexpL2 E 𝕜 hm) f) a)

    condexpL2 commutes with taking inner products with constants. See the lemma condexpL2_comp_continuousLinearMap for a more general result about commuting with continuous linear maps.

    theorem MeasureTheory.integral_condexpL2_eq {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (f : { x // x ∈ MeasureTheory.Lp E' 2 }) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) :
    ∫ (x : α) in s, ↑↑↑(↑(MeasureTheory.condexpL2 E' 𝕜 hm) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ

    condexpL2 verifies the equality of integrals defining the conditional expectation.

    theorem MeasureTheory.condexpL2_comp_continuousLinearMap {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E'' : Type u_8} (𝕜' : Type u_9) [IsROrC 𝕜'] [NormedAddCommGroup E''] [InnerProductSpace 𝕜' E''] [CompleteSpace E''] [NormedSpace ℝ E''] (hm : m ≤ m0) (T : E' →L[ℝ] E'') (f : { x // x ∈ MeasureTheory.Lp E' 2 }) :
    ↑↑↑(↑(MeasureTheory.condexpL2 E'' 𝕜' hm) (ContinuousLinearMap.compLp T f)) =ᶠ[MeasureTheory.Measure.ae μ] ↑↑(ContinuousLinearMap.compLp T ↑(↑(MeasureTheory.condexpL2 E' 𝕜 hm) f))
    theorem MeasureTheory.condexpL2_indicator_ae_eq_smul {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : E') :
    ↑↑↑(↑(MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) =ᶠ[MeasureTheory.Measure.ae μ] fun a => ↑↑↑(↑(MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a • x
    theorem MeasureTheory.condexpL2_indicator_eq_toSpanSingleton_comp {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : E') :
    theorem MeasureTheory.set_lintegral_nnnorm_condexpL2_indicator_le {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : E') {t : Set α} (ht : MeasurableSet t) (hμt : ↑↑μ t ≠ ⊤) :
    ∫⁻ (a : α) in t, ↑‖↑↑↑(↑(MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) a‖₊ ∂μ ≤ ↑↑μ (s ∩ t) * ↑‖x‖₊
    theorem MeasureTheory.lintegral_nnnorm_condexpL2_indicator_le {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : E') [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] :
    ∫⁻ (a : α), ↑‖↑↑↑(↑(MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) a‖₊ ∂μ ≤ ↑↑μ s * ↑‖x‖₊
    theorem MeasureTheory.integrable_condexpL2_indicator {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : E') :
    MeasureTheory.Integrable ↑↑↑(↑(MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x))

    If the measure μ.trim hm is sigma-finite, then the conditional expectation of a measurable set with finite measure is integrable.

    noncomputable def MeasureTheory.condexpIndSMul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : G) :
    { x // x ∈ MeasureTheory.Lp G 2 }

    Conditional expectation of the indicator of a measurable set with finite measure, in L2.

    Instances For
      theorem MeasureTheory.aeStronglyMeasurable'_condexpIndSMul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : G) :
      theorem MeasureTheory.condexpIndSMul_add {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : G) (y : G) :
      theorem MeasureTheory.condexpIndSMul_smul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (c : ℝ) (x : G) :
      theorem MeasureTheory.condexpIndSMul_smul' {α : Type u_1} {F : Type u_4} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0} [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (c : 𝕜) (x : F) :
      theorem MeasureTheory.condexpIndSMul_ae_eq_smul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : G) :
      ↑↑(MeasureTheory.condexpIndSMul hm hs hμs x) =ᶠ[MeasureTheory.Measure.ae μ] fun a => ↑↑↑(↑(MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a • x
      theorem MeasureTheory.set_lintegral_nnnorm_condexpIndSMul_le {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : G) {t : Set α} (ht : MeasurableSet t) (hμt : ↑↑μ t ≠ ⊤) :
      ∫⁻ (a : α) in t, ↑‖↑↑(MeasureTheory.condexpIndSMul hm hs hμs x) a‖₊ ∂μ ≤ ↑↑μ (s ∩ t) * ↑‖x‖₊
      theorem MeasureTheory.lintegral_nnnorm_condexpIndSMul_le {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : G) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] :
      ∫⁻ (a : α), ↑‖↑↑(MeasureTheory.condexpIndSMul hm hs hμs x) a‖₊ ∂μ ≤ ↑↑μ s * ↑‖x‖₊
      theorem MeasureTheory.integrable_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 (MeasureTheory.Measure.trim μ hm)] (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : G) :

      If the measure μ.trim hm is sigma-finite, then the conditional expectation of a measurable set with finite measure is integrable.

      theorem MeasureTheory.condexpIndSMul_empty {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedSpace ℝ G] {hm : m ≤ m0} {x : G} :
      theorem MeasureTheory.set_integral_condexpL2_indicator {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {hm : m ≤ m0} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : ↑↑μ s ≠ ⊤) (hμt : ↑↑μ t ≠ ⊤) :
      ∫ (x : α) in s, ↑↑↑(↑(MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 ht hμt 1)) x ∂μ = ENNReal.toReal (↑↑μ (t ∩ s))
      theorem MeasureTheory.set_integral_condexpIndSMul {α : 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} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : ↑↑μ s ≠ ⊤) (hμt : ↑↑μ t ≠ ⊤) (x : G') :
      ∫ (a : α) in s, ↑↑(MeasureTheory.condexpIndSMul hm ht hμt x) a ∂μ = ENNReal.toReal (↑↑μ (t ∩ s)) • x
      theorem MeasureTheory.condexpL2_indicator_nonneg {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] :
      theorem MeasureTheory.condexpIndSMul_nonneg {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0} {E : Type u_10} [NormedLatticeAddCommGroup E] [NormedSpace ℝ E] [OrderedSMul ℝ E] [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : E) (hx : 0 ≤ x) :