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

• condexpL2: Conditional expectation of a function in L2 with respect to a sigma-algebra: it is the orthogonal projection on the subspace lpMeas.

Implementation notes

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

• condexpL2 is defined only for an InnerProductSpace for now, and we use 𝕜 for its field.
• results about scalar multiplication are stated not only for ℝ but also for 𝕜 if we happen to have NormedSpace 𝕜 F.

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

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

Equations

• MeasureTheory.condexpL2 E 𝕜 hm = orthogonalProjection (MeasureTheory.lpMeas E 𝕜 m 2 μ)

theorem MeasureTheory.aeStronglyMeasurable'_condexpL2 {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hμs : μ s ≠ ⊤) (f : ↥(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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] {f : ↥(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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) : ‖MeasureTheory.condexpL2 E 𝕜 hm‖ ≤ 1

theorem MeasureTheory.norm_condexpL2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E 2 μ)) : ‖(MeasureTheory.condexpL2 E 𝕜 hm) f‖ ≤ ‖f‖

theorem MeasureTheory.eLpNorm_condexpL2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E 2 μ)) : MeasureTheory.eLpNorm (↑↑↑((MeasureTheory.condexpL2 E 𝕜 hm) f)) 2 μ ≤ MeasureTheory.eLpNorm (↑↑f) 2 μ

@[deprecated MeasureTheory.eLpNorm_condexpL2_le]

theorem MeasureTheory.snorm_condexpL2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E 2 μ)) : MeasureTheory.eLpNorm (↑↑↑((MeasureTheory.condexpL2 E 𝕜 hm) f)) 2 μ ≤ MeasureTheory.eLpNorm (↑↑f) 2 μ

Alias of MeasureTheory.eLpNorm_condexpL2_le.

theorem MeasureTheory.norm_condexpL2_coe_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E 2 μ)) : ‖↑((MeasureTheory.condexpL2 E 𝕜 hm) f)‖ ≤ ‖f‖

theorem MeasureTheory.inner_condexpL2_left_eq_right {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f g : ↥(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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : E) : ↑((MeasureTheory.condexpL2 E 𝕜 hm) (MeasureTheory.indicatorConstLp 2 ⋯ hμs c)) = MeasureTheory.indicatorConstLp 2 ⋯ hμs c

theorem MeasureTheory.inner_condexpL2_eq_inner_fun {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f g : ↥(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} [RCLike 𝕜] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0} (f : ↥(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 m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (f : ↥(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 m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) {f : ↥(MeasureTheory.Lp ℝ 2 μ)} (hf : ↑↑f =ᵐ[μ.restrict s] 0) : ↑↑↑((MeasureTheory.condexpL2 ℝ ℝ hm) f) =ᵐ[μ.restrict s] 0

theorem MeasureTheory.lintegral_nnnorm_condexpL2_indicator_le_real {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s 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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E 2 μ)) (c : E) : ↑↑↑((MeasureTheory.condexpL2 𝕜 𝕜 hm) (MeasureTheory.Memℒp.toLp (fun (a : α) => inner c (↑↑f a)) ⋯)) =ᵐ[μ] 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} [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (f : ↥(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) [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E'' : Type u_8} (𝕜' : Type u_9) [RCLike 𝕜'] [NormedAddCommGroup E''] [InnerProductSpace 𝕜' E''] [CompleteSpace E''] [NormedSpace ℝ E''] (hm : m ≤ m0) (T : E' →L[ℝ] E'') (f : ↥(MeasureTheory.Lp E' 2 μ)) : ↑↑↑((MeasureTheory.condexpL2 E'' 𝕜' hm) (T.compLp f)) =ᵐ[μ] ↑↑(T.compLp ↑((MeasureTheory.condexpL2 E' 𝕜 hm) f))

theorem MeasureTheory.condexpL2_indicator_ae_eq_smul {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m 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)) =ᵐ[μ] 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) [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m 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)) = (ContinuousLinearMap.toSpanSingleton ℝ x).compLp ↑((MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1))

theorem MeasureTheory.setLIntegral_nnnorm_condexpL2_indicator_le {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m 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‖₊

@[deprecated MeasureTheory.setLIntegral_nnnorm_condexpL2_indicator_le]

theorem MeasureTheory.set_lintegral_nnnorm_condexpL2_indicator_le {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m 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‖₊

Alias of MeasureTheory.setLIntegral_nnnorm_condexpL2_indicator_le.

theorem MeasureTheory.lintegral_nnnorm_condexpL2_indicator_le {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E') [MeasureTheory.SigmaFinite (μ.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} [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) [MeasureTheory.SigmaFinite (μ.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 m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : ↥(MeasureTheory.Lp G 2 μ)

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

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.aeStronglyMeasurable'_condexpIndSMul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : MeasureTheory.AEStronglyMeasurable' m (↑↑(MeasureTheory.condexpIndSMul hm hs hμs x)) μ

theorem MeasureTheory.condexpIndSMul_add {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x y : G) : MeasureTheory.condexpIndSMul hm hs hμs (x + y) = MeasureTheory.condexpIndSMul hm hs hμs x + MeasureTheory.condexpIndSMul hm hs hμs y

theorem MeasureTheory.condexpIndSMul_smul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : ℝ) (x : G) : MeasureTheory.condexpIndSMul hm hs hμs (c • x) = c • MeasureTheory.condexpIndSMul hm hs hμs x

theorem MeasureTheory.condexpIndSMul_smul' {α : Type u_1} {F : Type u_4} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0} [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : 𝕜) (x : F) : MeasureTheory.condexpIndSMul hm hs hμs (c • x) = c • MeasureTheory.condexpIndSMul hm hs hμs x

theorem MeasureTheory.condexpIndSMul_ae_eq_smul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m 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) =ᵐ[μ] fun (a : α) => ↑↑↑((MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a • x

theorem MeasureTheory.setLIntegral_nnnorm_condexpIndSMul_le {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m 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‖₊

@[deprecated MeasureTheory.setLIntegral_nnnorm_condexpIndSMul_le]

theorem MeasureTheory.set_lintegral_nnnorm_condexpIndSMul_le {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m 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‖₊

Alias of MeasureTheory.setLIntegral_nnnorm_condexpIndSMul_le.

theorem MeasureTheory.lintegral_nnnorm_condexpIndSMul_le {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) [MeasureTheory.SigmaFinite (μ.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 m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : MeasureTheory.Integrable (↑↑(MeasureTheory.condexpIndSMul hm 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.

theorem MeasureTheory.condexpIndSMul_empty {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedSpace ℝ G] {hm : m ≤ m0} {x : G} : MeasureTheory.condexpIndSMul hm ⋯ ⋯ x = 0

theorem MeasureTheory.setIntegral_condexpL2_indicator {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s 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 ∂μ = (μ (t ∩ s)).toReal

@[deprecated MeasureTheory.setIntegral_condexpL2_indicator]

theorem MeasureTheory.set_integral_condexpL2_indicator {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s 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 ∂μ = (μ (t ∩ s)).toReal

Alias of MeasureTheory.setIntegral_condexpL2_indicator.

theorem MeasureTheory.setIntegral_condexpIndSMul {α : Type u_1} {G' : Type u_6} [NormedAddCommGroup G'] [NormedSpace ℝ G'] [CompleteSpace G'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s 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 ∂μ = (μ (t ∩ s)).toReal • x

@[deprecated MeasureTheory.setIntegral_condexpIndSMul]

theorem MeasureTheory.set_integral_condexpIndSMul {α : Type u_1} {G' : Type u_6} [NormedAddCommGroup G'] [NormedSpace ℝ G'] [CompleteSpace G'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s 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 ∂μ = (μ (t ∩ s)).toReal • x

Alias of MeasureTheory.setIntegral_condexpIndSMul.

theorem MeasureTheory.condexpL2_indicator_nonneg {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) [MeasureTheory.SigmaFinite (μ.trim hm)] : 0 ≤ᵐ[μ] ↑↑↑((MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1))

theorem MeasureTheory.condexpIndSMul_nonneg {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0} {E : Type u_10} [NormedLatticeAddCommGroup E] [NormedSpace ℝ E] [OrderedSMul ℝ E] [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E) (hx : 0 ≤ x) : 0 ≤ᵐ[μ] ↑↑(MeasureTheory.condexpIndSMul hm hs hμs x)