Conditional expectation in L1 #
This file contains two more steps of the construction of the conditional expectation, which is
completed in Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean. 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.
noncomputable 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
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)
:
↑↑(condExpIndL1Fin hm hs hμs x) =ᵐ[μ] ↑↑(condExpIndSMul hm hs hμs x)
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)
:
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)
:
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)
:
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)
:
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)
:
noncomputable 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
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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
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)
:
noncomputable 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
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)
:
↑↑((condExpInd G hm μ s) x) =ᵐ[μ] ↑↑(condExpIndSMul hm hs hμs x)
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)]
:
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)
:
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)
:
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)]
:
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)
:
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')
:
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)
:
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]
[IsOrderedModule ℝ E]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : E)
(hx : 0 ≤ x)
:
noncomputable def
MeasureTheory.condExpL1CLM
{α : Type u_1}
(F' : Type u_3)
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : Measure α)
[CompleteSpace ↥(Lp F' 1 μ)]
[SigmaFinite (μ.trim hm)]
:
Conditional expectation of a function as a linear map from α →₁[μ] F' to itself.
Equations
Instances For
theorem
MeasureTheory.condExpL1CLM_smul
{α : Type u_1}
{F' : Type u_3}
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
[CompleteSpace F']
(c : 𝕜)
(f : ↥(Lp F' 1 μ))
:
theorem
MeasureTheory.condExpL1CLM_indicatorConstLp
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{s : Set α}
[CompleteSpace F']
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : F')
:
theorem
MeasureTheory.condExpL1CLM_indicatorConst
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{s : Set α}
[CompleteSpace F']
(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']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{s : Set α}
[CompleteSpace F']
(f : ↥(Lp F' 1 μ))
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
:
Auxiliary lemma used in the proof of setIntegral_condExpL1CLM.
theorem
MeasureTheory.setIntegral_condExpL1CLM
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{s : Set α}
[CompleteSpace F']
(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']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
[CompleteSpace F']
(f : ↥(Lp F' 1 μ))
:
AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ
theorem
MeasureTheory.condExpL1CLM_lpMeas
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
[CompleteSpace F']
(f : ↥(lpMeas F' ℝ m 1 μ))
:
theorem
MeasureTheory.condExpL1CLM_of_aestronglyMeasurable'
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
[CompleteSpace F']
(f : ↥(Lp F' 1 μ))
(hfm : AEStronglyMeasurable (↑↑f) μ)
:
noncomputable def
MeasureTheory.condExpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ 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
theorem
MeasureTheory.condExpL1_undef
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
(hf : ¬Integrable f μ)
:
theorem
MeasureTheory.condExpL1_eq
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
[CompleteSpace F']
(hf : Integrable f μ)
:
@[simp]
theorem
MeasureTheory.condExpL1_zero
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
:
@[simp]
theorem
MeasureTheory.condExpL1_measure_zero
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{f : α → F'}
(hm : m ≤ m0)
:
theorem
MeasureTheory.condExpL1_congr_ae
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f g : α → F'}
(hm✝ : m ≤ m0)
(h : f =ᵐ[μ] g)
:
theorem
MeasureTheory.aestronglyMeasurable_condExpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
:
AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ
theorem
MeasureTheory.integrable_condExpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : α → F')
:
Integrable (↑↑(condExpL1 hm μ f)) μ
theorem
MeasureTheory.setIntegral_condExpL1
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
{s : Set α}
[CompleteSpace F']
(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.
theorem
MeasureTheory.condExpL1_add
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f g : α → F'}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
theorem
MeasureTheory.condExpL1_neg
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(f : α → F')
:
theorem
MeasureTheory.condExpL1_smul
{α : Type u_1}
{F' : Type u_3}
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
(c : 𝕜)
(f : α → F')
:
theorem
MeasureTheory.condExpL1_sub
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f g : α → F'}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
theorem
MeasureTheory.condExpL1_of_aestronglyMeasurable'
{α : Type u_1}
{F' : Type u_3}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m m0 : MeasurableSpace α}
{μ : Measure α}
{hm : m ≤ m0}
[SigmaFinite (μ.trim hm)]
{f : α → F'}
[CompleteSpace 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]
[ClosedIciTopology E]
[IsOrderedAddMonoid E]
[NormedSpace ℝ E]
[IsOrderedModule ℝ E]
{f g : α → E}
(hf : Integrable f μ)
(hg : Integrable g μ)
(hfg : f ≤ᵐ[μ] g)
: