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 contitional 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_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.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_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.condexpIndL1Fin hm hs hμs x) =ᶠ[MeasureTheory.Measure.ae μ] ↑↑(MeasureTheory.condexpIndSMul hm hs hμs x)
theorem
MeasureTheory.condexpIndL1Fin_add
{α : 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)
(y : G)
:
MeasureTheory.condexpIndL1Fin hm hs hμs (x + y) = MeasureTheory.condexpIndL1Fin hm hs hμs x + MeasureTheory.condexpIndL1Fin hm hs hμs y
theorem
MeasureTheory.condexpIndL1Fin_smul
{α : 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 ≠ ⊤)
(c : ℝ)
(x : G)
:
MeasureTheory.condexpIndL1Fin hm hs hμs (c • x) = c • MeasureTheory.condexpIndL1Fin hm hs hμs x
theorem
MeasureTheory.condexpIndL1Fin_smul'
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_7}
[IsROrC 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
[NormedSpace ℝ F]
[SMulCommClass ℝ 𝕜 F]
(hs : MeasurableSet s)
(hμs : ↑↑μ s ≠ ⊤)
(c : 𝕜)
(x : F)
:
MeasureTheory.condexpIndL1Fin hm hs hμs (c • x) = c • MeasureTheory.condexpIndL1Fin hm hs hμs x
theorem
MeasureTheory.norm_condexpIndL1Fin_le
{α : 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)
:
theorem
MeasureTheory.condexpIndL1Fin_disjoint_union
{α : Type u_1}
{G : Type u_5}
[NormedAddCommGroup G]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : ↑↑μ s ≠ ⊤)
(hμt : ↑↑μ t ≠ ⊤)
(hst : s ∩ t = ∅)
(x : G)
:
MeasureTheory.condexpIndL1Fin hm ⋯ ⋯ x = MeasureTheory.condexpIndL1Fin hm hs hμs x + MeasureTheory.condexpIndL1Fin hm ht hμt x
def
MeasureTheory.condexpIndL1
{α : Type u_1}
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : MeasureTheory.Measure α)
(s : Set α)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(x : G)
:
↥(MeasureTheory.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_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.condexpIndL1 hm μ s x = MeasureTheory.condexpIndL1Fin hm hs hμs x
theorem
MeasureTheory.condexpIndL1_of_measure_eq_top
{α : 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)]
(hμs : ↑↑μ s = ⊤)
(x : G)
:
MeasureTheory.condexpIndL1 hm μ s x = 0
theorem
MeasureTheory.condexpIndL1_of_not_measurableSet
{α : 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)
(x : G)
:
MeasureTheory.condexpIndL1 hm μ s x = 0
theorem
MeasureTheory.condexpIndL1_add
{α : 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)]
(x : G)
(y : G)
:
MeasureTheory.condexpIndL1 hm μ s (x + y) = MeasureTheory.condexpIndL1 hm μ s x + MeasureTheory.condexpIndL1 hm μ s y
theorem
MeasureTheory.condexpIndL1_smul
{α : 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)]
(c : ℝ)
(x : G)
:
MeasureTheory.condexpIndL1 hm μ s (c • x) = c • MeasureTheory.condexpIndL1 hm μ s x
theorem
MeasureTheory.condexpIndL1_smul'
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_7}
[IsROrC 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
[NormedSpace ℝ F]
[SMulCommClass ℝ 𝕜 F]
(c : 𝕜)
(x : F)
:
MeasureTheory.condexpIndL1 hm μ s (c • x) = c • MeasureTheory.condexpIndL1 hm μ s x
theorem
MeasureTheory.norm_condexpIndL1_le
{α : 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)]
(x : G)
:
theorem
MeasureTheory.continuous_condexpIndL1
{α : 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)]
:
Continuous fun (x : G) => MeasureTheory.condexpIndL1 hm μ s x
theorem
MeasureTheory.condexpIndL1_disjoint_union
{α : Type u_1}
{G : Type u_5}
[NormedAddCommGroup G]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : ↑↑μ s ≠ ⊤)
(hμt : ↑↑μ t ≠ ⊤)
(hst : s ∩ t = ∅)
(x : G)
:
MeasureTheory.condexpIndL1 hm μ (s ∪ t) x = MeasureTheory.condexpIndL1 hm μ s x + MeasureTheory.condexpIndL1 hm μ t x
def
MeasureTheory.condexpInd
{α : Type u_1}
(G : Type u_5)
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(s : Set α)
:
G →L[ℝ] ↥(MeasureTheory.Lp G 1 μ)
Conditional expectation of the indicator of a set, as a linear map from G to L1.
Equations
- MeasureTheory.condexpInd G hm μ s = { toLinearMap := { toAddHom := { toFun := MeasureTheory.condexpIndL1 hm μ s, map_add' := ⋯ }, map_smul' := ⋯ }, cont := ⋯ }
Instances For
theorem
MeasureTheory.condexpInd_ae_eq_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.condexpInd G hm μ s) x) =ᶠ[MeasureTheory.Measure.ae μ] ↑↑(MeasureTheory.condexpIndSMul hm hs hμs x)
theorem
MeasureTheory.aestronglyMeasurable'_condexpInd
{α : 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.AEStronglyMeasurable' m (↑↑((MeasureTheory.condexpInd G hm μ s) x)) μ
@[simp]
theorem
MeasureTheory.condexpInd_empty
{α : Type u_1}
{G : Type u_5}
[NormedAddCommGroup G]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
:
MeasureTheory.condexpInd G hm μ ∅ = 0
theorem
MeasureTheory.condexpInd_smul'
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_7}
[IsROrC 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
[NormedSpace ℝ F]
[SMulCommClass ℝ 𝕜 F]
(c : 𝕜)
(x : F)
:
(MeasureTheory.condexpInd F hm μ s) (c • x) = c • (MeasureTheory.condexpInd F hm μ s) x
theorem
MeasureTheory.norm_condexpInd_apply_le
{α : 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)]
(x : G)
:
theorem
MeasureTheory.norm_condexpInd_le
{α : 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)]
:
‖MeasureTheory.condexpInd G hm μ s‖ ≤ (↑↑μ s).toReal
theorem
MeasureTheory.condexpInd_disjoint_union_apply
{α : Type u_1}
{G : Type u_5}
[NormedAddCommGroup G]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : ↑↑μ s ≠ ⊤)
(hμt : ↑↑μ t ≠ ⊤)
(hst : s ∩ t = ∅)
(x : G)
:
(MeasureTheory.condexpInd G hm μ (s ∪ t)) x = (MeasureTheory.condexpInd G hm μ s) x + (MeasureTheory.condexpInd G hm μ t) x
theorem
MeasureTheory.condexpInd_disjoint_union
{α : Type u_1}
{G : Type u_5}
[NormedAddCommGroup G]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
[NormedSpace ℝ G]
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : ↑↑μ s ≠ ⊤)
(hμt : ↑↑μ t ≠ ⊤)
(hst : s ∩ t = ∅)
:
MeasureTheory.condexpInd G hm μ (s ∪ t) = MeasureTheory.condexpInd G hm μ s + MeasureTheory.condexpInd G hm μ t
theorem
MeasureTheory.dominatedFinMeasAdditive_condexpInd
{α : Type u_1}
(G : Type u_5)
[NormedAddCommGroup G]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
[NormedSpace ℝ G]
(hm : m ≤ m0)
(μ : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
:
theorem
MeasureTheory.set_integral_condexpInd
{α : 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}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : ↑↑μ s ≠ ⊤)
(hμt : ↑↑μ t ≠ ⊤)
(x : G')
:
∫ (a : α) in s, ↑↑((MeasureTheory.condexpInd G' hm μ t) x) a ∂μ = (↑↑μ (t ∩ s)).toReal • x
theorem
MeasureTheory.condexpInd_of_measurable
{α : 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 ≠ ⊤)
(c : G)
:
(MeasureTheory.condexpInd G hm μ s) c = MeasureTheory.indicatorConstLp 1 ⋯ hμs c
theorem
MeasureTheory.condexpInd_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{E : Type u_8}
[NormedLatticeAddCommGroup E]
[NormedSpace ℝ E]
[OrderedSMul ℝ E]
(hs : MeasurableSet s)
(hμs : ↑↑μ s ≠ ⊤)
(x : E)
(hx : 0 ≤ x)
:
0 ≤ (MeasureTheory.condexpInd E hm μ s) x
def
MeasureTheory.condexpL1CLM
{α : Type u_1}
(F' : Type u_4)
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
:
↥(MeasureTheory.Lp F' 1 μ) →L[ℝ] ↥(MeasureTheory.Lp F' 1 μ)
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_4}
{𝕜 : Type u_7}
[IsROrC 𝕜]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(c : 𝕜)
(f : ↥(MeasureTheory.Lp F' 1 μ))
:
(MeasureTheory.condexpL1CLM F' hm μ) (c • f) = c • (MeasureTheory.condexpL1CLM F' hm μ) f
theorem
MeasureTheory.condexpL1CLM_indicatorConstLp
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{s : Set α}
(hs : MeasurableSet s)
(hμs : ↑↑μ s ≠ ⊤)
(x : F')
:
(MeasureTheory.condexpL1CLM F' hm μ) (MeasureTheory.indicatorConstLp 1 hs hμs x) = (MeasureTheory.condexpInd F' hm μ s) x
theorem
MeasureTheory.condexpL1CLM_indicatorConst
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{s : Set α}
(hs : MeasurableSet s)
(hμs : ↑↑μ s ≠ ⊤)
(x : F')
:
(MeasureTheory.condexpL1CLM F' hm μ) ↑(MeasureTheory.Lp.simpleFunc.indicatorConst 1 hs hμs x) = (MeasureTheory.condexpInd F' hm μ s) x
theorem
MeasureTheory.set_integral_condexpL1CLM_of_measure_ne_top
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{s : Set α}
(f : ↥(MeasureTheory.Lp F' 1 μ))
(hs : MeasurableSet s)
(hμs : ↑↑μ s ≠ ⊤)
:
∫ (x : α) in s, ↑↑((MeasureTheory.condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
Auxiliary lemma used in the proof of set_integral_condexpL1CLM.
theorem
MeasureTheory.set_integral_condexpL1CLM
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{s : Set α}
(f : ↥(MeasureTheory.Lp F' 1 μ))
(hs : MeasurableSet s)
:
∫ (x : α) in s, ↑↑((MeasureTheory.condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
The integral of the conditional expectation condexpL1CLM over an m-measurable set is equal
to the integral of f on that set. See also set_integral_condexp, the similar statement for
condexp.
theorem
MeasureTheory.aestronglyMeasurable'_condexpL1CLM
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(f : ↥(MeasureTheory.Lp F' 1 μ))
:
MeasureTheory.AEStronglyMeasurable' m (↑↑((MeasureTheory.condexpL1CLM F' hm μ) f)) μ
theorem
MeasureTheory.condexpL1CLM_lpMeas
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(f : ↥(MeasureTheory.lpMeas F' ℝ m 1 μ))
:
(MeasureTheory.condexpL1CLM F' hm μ) ↑f = ↑f
theorem
MeasureTheory.condexpL1CLM_of_aestronglyMeasurable'
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(f : ↥(MeasureTheory.Lp F' 1 μ))
(hfm : MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ)
:
(MeasureTheory.condexpL1CLM F' hm μ) f = f
def
MeasureTheory.condexpL1
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(hm : m ≤ m0)
(μ : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(f : α → F')
:
↥(MeasureTheory.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_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{f : α → F'}
(hf : ¬MeasureTheory.Integrable f μ)
:
MeasureTheory.condexpL1 hm μ f = 0
theorem
MeasureTheory.condexpL1_eq
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{f : α → F'}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.condexpL1 hm μ f = (MeasureTheory.condexpL1CLM F' hm μ) (MeasureTheory.Integrable.toL1 f hf)
@[simp]
theorem
MeasureTheory.condexpL1_zero
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
:
MeasureTheory.condexpL1 hm μ 0 = 0
@[simp]
theorem
MeasureTheory.condexpL1_measure_zero
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{f : α → F'}
(hm : m ≤ m0)
:
MeasureTheory.condexpL1 hm 0 f = 0
theorem
MeasureTheory.aestronglyMeasurable'_condexpL1
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{f : α → F'}
:
MeasureTheory.AEStronglyMeasurable' m (↑↑(MeasureTheory.condexpL1 hm μ f)) μ
theorem
MeasureTheory.condexpL1_congr_ae
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → F'}
{g : α → F'}
(hm : m ≤ m0)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(h : f =ᶠ[MeasureTheory.Measure.ae μ] g)
:
MeasureTheory.condexpL1 hm μ f = MeasureTheory.condexpL1 hm μ g
theorem
MeasureTheory.integrable_condexpL1
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(f : α → F')
:
MeasureTheory.Integrable (↑↑(MeasureTheory.condexpL1 hm μ f)) μ
theorem
MeasureTheory.set_integral_condexpL1
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{f : α → F'}
{s : Set α}
(hf : MeasureTheory.Integrable f μ)
(hs : MeasurableSet s)
:
∫ (x : α) in s, ↑↑(MeasureTheory.condexpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ
The integral of the conditional expectation condexpL1 over an m-measurable set is equal to
the integral of f on that set. See also set_integral_condexp, the similar statement for
condexp.
theorem
MeasureTheory.condexpL1_add
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{f : α → F'}
{g : α → F'}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.condexpL1 hm μ (f + g) = MeasureTheory.condexpL1 hm μ f + MeasureTheory.condexpL1 hm μ g
theorem
MeasureTheory.condexpL1_neg
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(f : α → F')
:
MeasureTheory.condexpL1 hm μ (-f) = -MeasureTheory.condexpL1 hm μ f
theorem
MeasureTheory.condexpL1_smul
{α : Type u_1}
{F' : Type u_4}
{𝕜 : Type u_7}
[IsROrC 𝕜]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
(c : 𝕜)
(f : α → F')
:
MeasureTheory.condexpL1 hm μ (c • f) = c • MeasureTheory.condexpL1 hm μ f
theorem
MeasureTheory.condexpL1_sub
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{f : α → F'}
{g : α → F'}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.condexpL1 hm μ (f - g) = MeasureTheory.condexpL1 hm μ f - MeasureTheory.condexpL1 hm μ g
theorem
MeasureTheory.condexpL1_of_aestronglyMeasurable'
{α : Type u_1}
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{f : α → F'}
(hfm : MeasureTheory.AEStronglyMeasurable' m f μ)
(hfi : MeasureTheory.Integrable f μ)
:
↑↑(MeasureTheory.condexpL1 hm μ f) =ᶠ[MeasureTheory.Measure.ae μ] f
theorem
MeasureTheory.condexpL1_mono
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)]
{E : Type u_8}
[NormedLatticeAddCommGroup E]
[CompleteSpace E]
[NormedSpace ℝ E]
[OrderedSMul ℝ E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
(hfg : f ≤ᶠ[MeasureTheory.Measure.ae μ] g)
:
↑↑(MeasureTheory.condexpL1 hm μ f) ≤ᶠ[MeasureTheory.Measure.ae μ] ↑↑(MeasureTheory.condexpL1 hm μ g)