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 sendsx ∈ Eto the conditional expectation of the indicator of the set with valuex. - Extend that map to
condExpL1CLM : (α →₁[μ] E) →L[ℝ] (α →₁[μ] E). This is done using the same construction as the Bochner integral (see the fileMeasureTheory/Integral/SetToL1).
Main definitions #
condExpL1: Conditional expectation of a function as a linear map fromL1to 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_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
(hm : m ≤ m0)
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
↥(Lp G 1 μ)
Conditional expectation of the indicator of a measurable set with finite measure, as a function in L1.
Equations
- MeasureTheory.condExpIndL1Fin hm hs hμs x = MeasureTheory.Integrable.toL1 ↑↑(MeasureTheory.condExpIndSMul hm hs hμs x) ⋯
Instances For
@[deprecated MeasureTheory.condExpIndL1Fin (since := "2025-01-21")]
def
MeasureTheory.condexpIndL1Fin
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
(hm : m ≤ m0)
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
↥(Lp G 1 μ)
Alias of MeasureTheory.condExpIndL1Fin.
Conditional expectation of the indicator of a measurable set with finite measure, as a function in L1.
Instances For
theorem
MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
(hm : m ≤ m0)
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
@[deprecated MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul (since := "2025-01-21")]
theorem
MeasureTheory.condexpIndL1Fin_ae_eq_condexpIndSMul
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
(hm : m ≤ m0)
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
Alias of MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul.
theorem
MeasureTheory.condExpIndL1Fin_add
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x y : G)
:
@[deprecated MeasureTheory.condExpIndL1Fin_add (since := "2025-01-21")]
theorem
MeasureTheory.condexpIndL1Fin_add
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x y : G)
:
Alias of MeasureTheory.condExpIndL1Fin_add.
theorem
MeasureTheory.condExpIndL1Fin_smul
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(c : ℝ)
(x : G)
:
@[deprecated MeasureTheory.condExpIndL1Fin_smul (since := "2025-01-21")]
theorem
MeasureTheory.condexpIndL1Fin_smul
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(c : ℝ)
(x : G)
:
Alias of MeasureTheory.condExpIndL1Fin_smul.
theorem
MeasureTheory.condExpIndL1Fin_smul'
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
[NormedSpace ℝ F]
[SMulCommClass ℝ 𝕜 F]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(c : 𝕜)
(x : F)
:
@[deprecated MeasureTheory.condExpIndL1Fin_smul' (since := "2025-01-21")]
theorem
MeasureTheory.condexpIndL1Fin_smul'
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
[NormedSpace ℝ F]
[SMulCommClass ℝ 𝕜 F]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(c : 𝕜)
(x : F)
:
Alias of MeasureTheory.condExpIndL1Fin_smul'.
theorem
MeasureTheory.norm_condExpIndL1Fin_le
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
@[deprecated MeasureTheory.norm_condExpIndL1Fin_le (since := "2025-01-21")]
theorem
MeasureTheory.norm_condexpIndL1Fin_le
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
Alias of MeasureTheory.norm_condExpIndL1Fin_le.
theorem
MeasureTheory.condExpIndL1Fin_disjoint_union
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : μ s ≠ ⊤)
(hμt : μ t ≠ ⊤)
(hst : Disjoint s t)
(x : G)
:
@[deprecated MeasureTheory.condExpIndL1Fin_disjoint_union (since := "2025-01-21")]
theorem
MeasureTheory.condexpIndL1Fin_disjoint_union
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : μ s ≠ ⊤)
(hμt : μ t ≠ ⊤)
(hst : Disjoint s t)
(x : G)
:
def
MeasureTheory.condExpIndL1
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{m m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : Measure α)
(s : Set α)
[SigmaFinite (μ.trim hm)]
(x : G)
:
↥(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
- MeasureTheory.condExpIndL1 hm μ s x = if hs : MeasurableSet s ∧ μ s ≠ ⊤ then MeasureTheory.condExpIndL1Fin hm ⋯ ⋯ x else 0
Instances For
@[deprecated MeasureTheory.condExpIndL1 (since := "2025-01-21")]
def
MeasureTheory.condexpIndL1
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{m m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : Measure α)
(s : Set α)
[SigmaFinite (μ.trim hm)]
(x : G)
:
↥(Lp G 1 μ)
Alias of MeasureTheory.condExpIndL1.
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.
Instances For
theorem
MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
@[deprecated MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top (since := "2025-01-21")]
theorem
MeasureTheory.condexpIndL1_of_measurableSet_of_measure_ne_top
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
Alias of MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top.
theorem
MeasureTheory.condExpIndL1_of_measure_eq_top
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hμs : μ s = ⊤)
(x : G)
:
@[deprecated MeasureTheory.condExpIndL1_of_measure_eq_top (since := "2025-01-21")]
theorem
MeasureTheory.condexpIndL1_of_measure_eq_top
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hμs : μ s = ⊤)
(x : G)
:
theorem
MeasureTheory.condExpIndL1_of_not_measurableSet
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : ¬MeasurableSet s)
(x : G)
:
@[deprecated MeasureTheory.condExpIndL1_of_not_measurableSet (since := "2025-01-21")]
theorem
MeasureTheory.condexpIndL1_of_not_measurableSet
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : ¬MeasurableSet s)
(x : G)
:
theorem
MeasureTheory.condExpIndL1_add
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(x y : G)
:
@[deprecated MeasureTheory.condExpIndL1_add (since := "2025-01-21")]
theorem
MeasureTheory.condexpIndL1_add
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(x y : G)
:
Alias of MeasureTheory.condExpIndL1_add.
theorem
MeasureTheory.condExpIndL1_smul
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(c : ℝ)
(x : G)
:
@[deprecated MeasureTheory.condExpIndL1_smul (since := "2025-01-21")]
theorem
MeasureTheory.condexpIndL1_smul
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(c : ℝ)
(x : G)
:
Alias of MeasureTheory.condExpIndL1_smul.
theorem
MeasureTheory.condExpIndL1_smul'
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
[NormedSpace ℝ F]
[SMulCommClass ℝ 𝕜 F]
(c : 𝕜)
(x : F)
:
@[deprecated MeasureTheory.condExpIndL1_smul' (since := "2025-01-21")]
theorem
MeasureTheory.condexpIndL1_smul'
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
[NormedSpace ℝ F]
[SMulCommClass ℝ 𝕜 F]
(c : 𝕜)
(x : F)
:
Alias of MeasureTheory.condExpIndL1_smul'.
theorem
MeasureTheory.norm_condExpIndL1_le
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(x : G)
:
@[deprecated MeasureTheory.norm_condExpIndL1_le (since := "2025-01-21")]
theorem
MeasureTheory.norm_condexpIndL1_le
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(x : G)
:
Alias of MeasureTheory.norm_condExpIndL1_le.
theorem
MeasureTheory.continuous_condExpIndL1
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
:
Continuous fun (x : G) => condExpIndL1 hm μ s x
@[deprecated MeasureTheory.continuous_condExpIndL1 (since := "2025-01-21")]
theorem
MeasureTheory.continuous_condexpIndL1
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
:
Continuous fun (x : G) => condExpIndL1 hm μ s x
Alias of MeasureTheory.continuous_condExpIndL1.
theorem
MeasureTheory.condExpIndL1_disjoint_union
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : μ s ≠ ⊤)
(hμt : μ t ≠ ⊤)
(hst : Disjoint s t)
(x : G)
:
@[deprecated MeasureTheory.condExpIndL1_disjoint_union (since := "2025-01-21")]
theorem
MeasureTheory.condexpIndL1_disjoint_union
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : μ s ≠ ⊤)
(hμt : μ t ≠ ⊤)
(hst : Disjoint s t)
(x : G)
:
def
MeasureTheory.condExpInd
{α : Type u_1}
(G : Type u_4)
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{m m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : Measure α)
[SigmaFinite (μ.trim hm)]
(s : Set α)
:
Conditional expectation of the indicator of a set, as a linear map from G to L1.
Equations
- MeasureTheory.condExpInd G hm μ s = { toFun := MeasureTheory.condExpIndL1 hm μ s, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
@[deprecated MeasureTheory.condExpInd (since := "2025-01-21")]
def
MeasureTheory.condexpInd
{α : Type u_1}
(G : Type u_4)
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{m m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : Measure α)
[SigmaFinite (μ.trim hm)]
(s : Set α)
:
Alias of MeasureTheory.condExpInd.
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_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
(hm : m ≤ m0)
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
@[deprecated MeasureTheory.condExpInd_ae_eq_condExpIndSMul (since := "2025-01-21")]
theorem
MeasureTheory.condexpInd_ae_eq_condexpIndSMul
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
(hm : m ≤ m0)
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
theorem
MeasureTheory.aestronglyMeasurable_condExpInd
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
AEStronglyMeasurable (↑↑((condExpInd G hm μ s) x)) μ
@[deprecated MeasureTheory.aestronglyMeasurable_condExpInd (since := "2025-01-24")]
theorem
MeasureTheory.aestronglyMeasurable'_condExpInd
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
AEStronglyMeasurable (↑↑((condExpInd G hm μ s) x)) μ
@[deprecated MeasureTheory.aestronglyMeasurable_condExpInd (since := "2025-01-21")]
theorem
MeasureTheory.aestronglyMeasurable'_condexpInd
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : G)
:
AEStronglyMeasurable (↑↑((condExpInd G hm μ s) x)) μ
@[simp]
theorem
MeasureTheory.condExpInd_empty
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
:
@[deprecated MeasureTheory.condExpInd_empty (since := "2025-01-21")]
theorem
MeasureTheory.condexpInd_empty
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
:
Alias of MeasureTheory.condExpInd_empty.
theorem
MeasureTheory.condExpInd_smul'
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
[NormedSpace ℝ F]
[SMulCommClass ℝ 𝕜 F]
(c : 𝕜)
(x : F)
:
@[deprecated MeasureTheory.condExpInd_smul' (since := "2025-01-21")]
theorem
MeasureTheory.condexpInd_smul'
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
[NormedSpace ℝ F]
[SMulCommClass ℝ 𝕜 F]
(c : 𝕜)
(x : F)
:
Alias of MeasureTheory.condExpInd_smul'.
theorem
MeasureTheory.norm_condExpInd_apply_le
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(x : G)
:
@[deprecated MeasureTheory.norm_condExpInd_apply_le (since := "2025-01-21")]
theorem
MeasureTheory.norm_condexpInd_apply_le
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(x : G)
:
Alias of MeasureTheory.norm_condExpInd_apply_le.
theorem
MeasureTheory.norm_condExpInd_le
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
:
@[deprecated MeasureTheory.norm_condExpInd_le (since := "2025-01-21")]
theorem
MeasureTheory.norm_condexpInd_le
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
:
Alias of MeasureTheory.norm_condExpInd_le.
theorem
MeasureTheory.condExpInd_disjoint_union_apply
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : μ s ≠ ⊤)
(hμt : μ t ≠ ⊤)
(hst : Disjoint s t)
(x : G)
:
@[deprecated MeasureTheory.condExpInd_disjoint_union_apply (since := "2025-01-21")]
theorem
MeasureTheory.condexpInd_disjoint_union_apply
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : μ s ≠ ⊤)
(hμt : μ t ≠ ⊤)
(hst : Disjoint s t)
(x : G)
:
theorem
MeasureTheory.condExpInd_disjoint_union
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : μ s ≠ ⊤)
(hμt : μ t ≠ ⊤)
(hst : Disjoint s t)
:
@[deprecated MeasureTheory.condExpInd_disjoint_union (since := "2025-01-21")]
theorem
MeasureTheory.condexpInd_disjoint_union
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : μ s ≠ ⊤)
(hμt : μ t ≠ ⊤)
(hst : Disjoint s t)
:
Alias of MeasureTheory.condExpInd_disjoint_union.
theorem
MeasureTheory.dominatedFinMeasAdditive_condExpInd
{α : Type u_1}
(G : Type u_4)
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
[NormedSpace ℝ G]
(hm : m ≤ m0)
(μ : Measure α)
[SigmaFinite (μ.trim hm)]
:
DominatedFinMeasAdditive μ (condExpInd G hm μ) 1
@[deprecated MeasureTheory.dominatedFinMeasAdditive_condExpInd (since := "2025-01-21")]
theorem
MeasureTheory.dominatedFinMeasAdditive_condexpInd
{α : Type u_1}
(G : Type u_4)
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
[NormedSpace ℝ G]
(hm : m ≤ m0)
(μ : Measure α)
[SigmaFinite (μ.trim hm)]
:
DominatedFinMeasAdditive μ (condExpInd G hm μ) 1
theorem
MeasureTheory.setIntegral_condExpInd
{α : Type u_1}
{G' : Type u_5}
[NormedAddCommGroup G']
[NormedSpace ℝ G']
[CompleteSpace G']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : μ s ≠ ⊤)
(hμt : μ t ≠ ⊤)
(x : G')
:
@[deprecated MeasureTheory.setIntegral_condExpInd (since := "2025-01-21")]
theorem
MeasureTheory.setIntegral_condexpInd
{α : Type u_1}
{G' : Type u_5}
[NormedAddCommGroup G']
[NormedSpace ℝ G']
[CompleteSpace G']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : μ s ≠ ⊤)
(hμt : μ t ≠ ⊤)
(x : G')
:
Alias of MeasureTheory.setIntegral_condExpInd.
theorem
MeasureTheory.condExpInd_of_measurable
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(c : G)
:
@[deprecated MeasureTheory.condExpInd_of_measurable (since := "2025-01-21")]
theorem
MeasureTheory.condexpInd_of_measurable
{α : Type u_1}
{G : Type u_4}
[NormedAddCommGroup G]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(c : G)
:
Alias of MeasureTheory.condExpInd_of_measurable.
theorem
MeasureTheory.condExpInd_nonneg
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{E : Type u_7}
[NormedAddCommGroup E]
[PartialOrder E]
[NormedSpace ℝ E]
[OrderedSMul ℝ E]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : E)
(hx : 0 ≤ x)
:
@[deprecated MeasureTheory.condExpInd_nonneg (since := "2025-01-21")]
theorem
MeasureTheory.condexpInd_nonneg
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{E : Type u_7}
[NormedAddCommGroup E]
[PartialOrder E]
[NormedSpace ℝ E]
[OrderedSMul ℝ E]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : E)
(hx : 0 ≤ x)
:
Alias of MeasureTheory.condExpInd_nonneg.
def
MeasureTheory.condExpL1CLM
{α : Type u_1}
(F' : Type u_3)
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : Measure α)
[SigmaFinite (μ.trim hm)]
:
Conditional expectation of a function as a linear map from α →₁[μ] F' to itself.
Equations
Instances For
@[deprecated MeasureTheory.condExpL1CLM (since := "2025-01-21")]
def
MeasureTheory.condexpL1CLM
{α : Type u_1}
(F' : Type u_3)
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : Measure α)
[SigmaFinite (μ.trim hm)]
:
Alias of MeasureTheory.condExpL1CLM.
Conditional expectation of a function as a linear map from α →₁[μ] F' to itself.
Instances For
theorem
MeasureTheory.condExpL1CLM_smul
{α : Type u_1}
{F' : Type u_3}
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(c : 𝕜)
(f : ↥(Lp F' 1 μ))
:
@[deprecated MeasureTheory.condExpL1CLM_smul (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1CLM_smul
{α : Type u_1}
{F' : Type u_3}
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(c : 𝕜)
(f : ↥(Lp F' 1 μ))
:
Alias of MeasureTheory.condExpL1CLM_smul.
theorem
MeasureTheory.condExpL1CLM_indicatorConstLp
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : F')
:
@[deprecated MeasureTheory.condExpL1CLM_indicatorConstLp (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1CLM_indicatorConstLp
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : F')
:
theorem
MeasureTheory.condExpL1CLM_indicatorConst
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : F')
:
@[deprecated MeasureTheory.condExpL1CLM_indicatorConst (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1CLM_indicatorConst
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[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_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{s : Set α}
(f : ↥(Lp F' 1 μ))
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
:
Auxiliary lemma used in the proof of setIntegral_condExpL1CLM.
@[deprecated MeasureTheory.setIntegral_condExpL1CLM_of_measure_ne_top (since := "2025-01-21")]
theorem
MeasureTheory.setIntegral_condexpL1CLM_of_measure_ne_top
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{s : Set α}
(f : ↥(Lp F' 1 μ))
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
:
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_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{s : Set α}
(f : ↥(Lp F' 1 μ))
(hs : MeasurableSet s)
:
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_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : ↥(Lp F' 1 μ))
:
AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ
@[deprecated MeasureTheory.aestronglyMeasurable_condExpL1CLM (since := "2025-01-24")]
theorem
MeasureTheory.aestronglyMeasurable'_condExpL1CLM
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : ↥(Lp F' 1 μ))
:
AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ
@[deprecated MeasureTheory.aestronglyMeasurable_condExpL1CLM (since := "2025-01-21")]
theorem
MeasureTheory.aestronglyMeasurable_condexpL1CLM
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : ↥(Lp F' 1 μ))
:
AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ
@[deprecated MeasureTheory.aestronglyMeasurable_condexpL1CLM (since := "2025-01-24")]
theorem
MeasureTheory.aestronglyMeasurable'_condexpL1CLM
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : ↥(Lp F' 1 μ))
:
AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ
Alias of MeasureTheory.aestronglyMeasurable_condExpL1CLM.
theorem
MeasureTheory.condExpL1CLM_lpMeas
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : ↥(lpMeas F' ℝ m 1 μ))
:
@[deprecated MeasureTheory.condExpL1CLM_lpMeas (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1CLM_lpMeas
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : ↥(lpMeas F' ℝ m 1 μ))
:
Alias of MeasureTheory.condExpL1CLM_lpMeas.
theorem
MeasureTheory.condExpL1CLM_of_aestronglyMeasurable'
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : ↥(Lp F' 1 μ))
(hfm : AEStronglyMeasurable (↑↑f) μ)
:
@[deprecated MeasureTheory.condExpL1CLM_of_aestronglyMeasurable' (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1CLM_of_aestronglyMeasurable'
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : ↥(Lp F' 1 μ))
(hfm : AEStronglyMeasurable (↑↑f) μ)
:
Alias of MeasureTheory.condExpL1CLM_of_aestronglyMeasurable'.
def
MeasureTheory.condExpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : Measure α)
[SigmaFinite (μ.trim hm)]
(f : α → F')
:
↥(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
- MeasureTheory.condExpL1 hm μ f = MeasureTheory.setToFun μ (MeasureTheory.condExpInd F' hm μ) ⋯ f
Instances For
@[deprecated MeasureTheory.condExpL1 (since := "2025-01-21")]
def
MeasureTheory.condexpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : Measure α)
[SigmaFinite (μ.trim hm)]
(f : α → F')
:
↥(Lp F' 1 μ)
Alias of MeasureTheory.condExpL1.
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_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
(hf : ¬Integrable f μ)
:
@[deprecated MeasureTheory.condExpL1_undef (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1_undef
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
(hf : ¬Integrable f μ)
:
Alias of MeasureTheory.condExpL1_undef.
theorem
MeasureTheory.condExpL1_eq
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
(hf : Integrable f μ)
:
@[deprecated MeasureTheory.condExpL1_eq (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1_eq
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
(hf : Integrable f μ)
:
Alias of MeasureTheory.condExpL1_eq.
@[simp]
theorem
MeasureTheory.condExpL1_zero
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
:
@[deprecated MeasureTheory.condExpL1_zero (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1_zero
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
:
Alias of MeasureTheory.condExpL1_zero.
@[simp]
theorem
MeasureTheory.condExpL1_measure_zero
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{f : α → F'}
(hm : m ≤ m0)
:
@[deprecated MeasureTheory.condExpL1_measure_zero (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1_measure_zero
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{f : α → F'}
(hm : m ≤ m0)
:
Alias of MeasureTheory.condExpL1_measure_zero.
theorem
MeasureTheory.aestronglyMeasurable_condExpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
:
AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ
@[deprecated MeasureTheory.aestronglyMeasurable_condExpL1 (since := "2025-01-24")]
theorem
MeasureTheory.aestronglyMeasurable'_condExpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
:
AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ
@[deprecated MeasureTheory.aestronglyMeasurable_condExpL1 (since := "2025-01-21")]
theorem
MeasureTheory.aestronglyMeasurable_condexpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
:
AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ
@[deprecated MeasureTheory.aestronglyMeasurable_condexpL1 (since := "2025-01-24")]
theorem
MeasureTheory.aestronglyMeasurable'_condexpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
:
AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ
Alias of MeasureTheory.aestronglyMeasurable_condExpL1.
theorem
MeasureTheory.condExpL1_congr_ae
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{f g : α → F'}
(hm : m ≤ m0)
[SigmaFinite (μ.trim hm)]
(h : f =ᶠ[ae μ] g)
:
@[deprecated MeasureTheory.condExpL1_congr_ae (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1_congr_ae
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{f g : α → F'}
(hm : m ≤ m0)
[SigmaFinite (μ.trim hm)]
(h : f =ᶠ[ae μ] g)
:
Alias of MeasureTheory.condExpL1_congr_ae.
theorem
MeasureTheory.integrable_condExpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : α → F')
:
Integrable (↑↑(condExpL1 hm μ f)) μ
@[deprecated MeasureTheory.integrable_condExpL1 (since := "2025-01-21")]
theorem
MeasureTheory.integrable_condexpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : α → F')
:
Integrable (↑↑(condExpL1 hm μ f)) μ
Alias of MeasureTheory.integrable_condExpL1.
theorem
MeasureTheory.setIntegral_condExpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
{s : Set α}
(hf : Integrable f μ)
(hs : MeasurableSet s)
:
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 (since := "2025-01-21")]
theorem
MeasureTheory.setIntegral_condexpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
{s : Set α}
(hf : Integrable f μ)
(hs : MeasurableSet s)
:
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_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f g : α → F'}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
@[deprecated MeasureTheory.condExpL1_add (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1_add
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f g : α → F'}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
Alias of MeasureTheory.condExpL1_add.
theorem
MeasureTheory.condExpL1_neg
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : α → F')
:
@[deprecated MeasureTheory.condExpL1_neg (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1_neg
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : α → F')
:
Alias of MeasureTheory.condExpL1_neg.
theorem
MeasureTheory.condExpL1_smul
{α : Type u_1}
{F' : Type u_3}
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(c : 𝕜)
(f : α → F')
:
@[deprecated MeasureTheory.condExpL1_smul (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1_smul
{α : Type u_1}
{F' : Type u_3}
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(c : 𝕜)
(f : α → F')
:
Alias of MeasureTheory.condExpL1_smul.
theorem
MeasureTheory.condExpL1_sub
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f g : α → F'}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
@[deprecated MeasureTheory.condExpL1_sub (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1_sub
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f g : α → F'}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
Alias of MeasureTheory.condExpL1_sub.
theorem
MeasureTheory.condExpL1_of_aestronglyMeasurable'
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
(hfm : AEStronglyMeasurable f μ)
(hfi : Integrable f μ)
:
@[deprecated MeasureTheory.condExpL1_of_aestronglyMeasurable' (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1_of_aestronglyMeasurable'
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
(hfm : AEStronglyMeasurable f μ)
(hfi : Integrable f μ)
:
theorem
MeasureTheory.condExpL1_mono
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{E : Type u_7}
[NormedAddCommGroup E]
[PartialOrder E]
[OrderClosedTopology E]
[IsOrderedAddMonoid E]
[CompleteSpace E]
[NormedSpace ℝ E]
[OrderedSMul ℝ E]
{f g : α → E}
(hf : Integrable f μ)
(hg : Integrable g μ)
(hfg : f ≤ᶠ[ae μ] g)
:
@[deprecated MeasureTheory.condExpL1_mono (since := "2025-01-21")]
theorem
MeasureTheory.condexpL1_mono
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{E : Type u_7}
[NormedAddCommGroup E]
[PartialOrder E]
[OrderClosedTopology E]
[IsOrderedAddMonoid E]
[CompleteSpace E]
[NormedSpace ℝ E]
[OrderedSMul ℝ E]
{f g : α → E}
(hf : Integrable f μ)
(hg : Integrable g μ)
(hfg : f ≤ᶠ[ae μ] g)
:
Alias of MeasureTheory.condExpL1_mono.