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 subspacelpMeas.
Implementation notes #
Most of the results in this file are valid for a complete real normed space F.
However, some lemmas also use 𝕜 : IsROrC:
condexpL2is defined only for anInnerProductSpacefor now, and we use𝕜for its field.- results about scalar multiplication are stated not only for
ℝbut also for𝕜if we happen to haveNormedSpace 𝕜 F.
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)
:
↥(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 μ)
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 : ↥(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 : ↥(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 : ↥(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)
:
‖MeasureTheory.condexpL2 E 𝕜 hm‖ ≤ 1
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 : ↥(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 : ↥(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 : ↥(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 : ↥(MeasureTheory.Lp E 2)}
{g : ↥(MeasureTheory.Lp E 2)}
:
⟪↑((MeasureTheory.condexpL2 E 𝕜 hm) f), g⟫_𝕜 = ⟪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 (_ : MeasurableSet s) hμs c)) = MeasureTheory.indicatorConstLp 2 (_ : MeasurableSet s) 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 : ↥(MeasureTheory.Lp E 2))
(g : ↥(MeasureTheory.Lp E 2))
(hg : MeasureTheory.AEStronglyMeasurable' m (↑↑g) μ)
:
⟪↑((MeasureTheory.condexpL2 E 𝕜 hm) f), g⟫_𝕜 = ⟪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 : ↥(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 : ↥(MeasureTheory.Lp ℝ 2))
:
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 : ↥(MeasureTheory.Lp ℝ 2)}
(hf : ↑↑f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)] 0)
:
↑↑↑((MeasureTheory.condexpL2 ℝ ℝ hm) 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 : ↥(MeasureTheory.Lp E 2))
(c : E)
:
↑↑↑((MeasureTheory.condexpL2 𝕜 𝕜 hm)
(MeasureTheory.Memℒp.toLp (fun (a : α) => ⟪c, ↑↑f a⟫_𝕜)
(_ : MeasureTheory.Memℒp (fun (a : α) => ⟪c, ↑↑f a⟫_𝕜) 2))) =ᶠ[MeasureTheory.Measure.ae μ] fun (a : α) => ⟪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 : ↥(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 : ↥(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')
:
↑((MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) = ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x)
↑((MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1))
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)
:
↥(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.
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)
:
MeasureTheory.AEStronglyMeasurable' m (↑↑(MeasureTheory.condexpIndSMul hm hs hμs x)) μ
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)
:
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 : MeasurableSpace α}
{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}
[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)
:
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 : 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 ≠ ⊤)
:
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)]
:
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)
:
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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
{x : G}
:
MeasureTheory.condexpIndSMul hm (_ : MeasurableSet ∅) (_ : ↑↑μ ∅ ≠ ⊤) x = 0
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)]
:
0 ≤ᶠ[MeasureTheory.Measure.ae μ] ↑↑↑((MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1))
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)
:
0 ≤ᶠ[MeasureTheory.Measure.ae μ] ↑↑(MeasureTheory.condexpIndSMul hm hs hμs x)