Conditional expectation in L1 #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains two more steps of the construction of the conditional expectation, which is
completed in measure_theory.function.conditional_expectation.basic. See that file for a
description of the full process.
The contitional expectation of an L² function is defined in
measure_theory.function.conditional_expectation.condexp_L2. 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
condexp_L1_clm : (α →₁[μ] E) →L[ℝ] (α →₁[μ] E). This is done using the same construction as the Bochner integral (see the filemeasure_theory/integral/set_to_L1).
Main definitions #
condexp_L1: 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
condexp_ind (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
measure_theory.condexp_ind_L1_fin
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
↥(measure_theory.Lp G 1 μ)
Conditional expectation of the indicator of a measurable set with finite measure, as a function in L1.
Equations
- measure_theory.condexp_ind_L1_fin hm hs hμs x = measure_theory.integrable.to_L1 ⇑(measure_theory.condexp_ind_smul hm hs hμs x) _
theorem
measure_theory.condexp_ind_L1_fin_ae_eq_condexp_ind_smul
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
⇑(measure_theory.condexp_ind_L1_fin hm hs hμs x) =ᵐ[μ] ⇑(measure_theory.condexp_ind_smul hm hs hμs x)
theorem
measure_theory.condexp_ind_L1_fin_add
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x y : G) :
measure_theory.condexp_ind_L1_fin hm hs hμs (x + y) = measure_theory.condexp_ind_L1_fin hm hs hμs x + measure_theory.condexp_ind_L1_fin hm hs hμs y
theorem
measure_theory.condexp_ind_L1_fin_smul
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : ℝ)
(x : G) :
measure_theory.condexp_ind_L1_fin hm hs hμs (c • x) = c • measure_theory.condexp_ind_L1_fin hm hs hμs x
theorem
measure_theory.condexp_ind_L1_fin_smul'
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
[normed_space ℝ F]
[smul_comm_class ℝ 𝕜 F]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : 𝕜)
(x : F) :
measure_theory.condexp_ind_L1_fin hm hs hμs (c • x) = c • measure_theory.condexp_ind_L1_fin hm hs hμs x
theorem
measure_theory.norm_condexp_ind_L1_fin_le
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
theorem
measure_theory.condexp_ind_L1_fin_disjoint_union
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤)
(hst : s ∩ t = ∅)
(x : G) :
measure_theory.condexp_ind_L1_fin hm _ _ x = measure_theory.condexp_ind_L1_fin hm hs hμs x + measure_theory.condexp_ind_L1_fin hm ht hμt x
noncomputable
def
measure_theory.condexp_ind_L1
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
[normed_space ℝ G]
{m m0 : measurable_space α}
(hm : m ≤ m0)
(μ : measure_theory.measure α)
(s : set α)
[measure_theory.sigma_finite (μ.trim hm)]
(x : G) :
↥(measure_theory.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
- measure_theory.condexp_ind_L1 hm μ s x = dite (measurable_set s ∧ ⇑μ s ≠ ⊤) (λ (hs : measurable_set s ∧ ⇑μ s ≠ ⊤), measure_theory.condexp_ind_L1_fin hm _ _ x) (λ (hs : ¬(measurable_set s ∧ ⇑μ s ≠ ⊤)), 0)
theorem
measure_theory.condexp_ind_L1_of_measurable_set_of_measure_ne_top
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
measure_theory.condexp_ind_L1 hm μ s x = measure_theory.condexp_ind_L1_fin hm hs hμs x
theorem
measure_theory.condexp_ind_L1_of_measure_eq_top
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hμs : ⇑μ s = ⊤)
(x : G) :
measure_theory.condexp_ind_L1 hm μ s x = 0
theorem
measure_theory.condexp_ind_L1_of_not_measurable_set
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : ¬measurable_set s)
(x : G) :
measure_theory.condexp_ind_L1 hm μ s x = 0
theorem
measure_theory.condexp_ind_L1_add
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(x y : G) :
measure_theory.condexp_ind_L1 hm μ s (x + y) = measure_theory.condexp_ind_L1 hm μ s x + measure_theory.condexp_ind_L1 hm μ s y
theorem
measure_theory.condexp_ind_L1_smul
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(c : ℝ)
(x : G) :
measure_theory.condexp_ind_L1 hm μ s (c • x) = c • measure_theory.condexp_ind_L1 hm μ s x
theorem
measure_theory.condexp_ind_L1_smul'
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
[normed_space ℝ F]
[smul_comm_class ℝ 𝕜 F]
(c : 𝕜)
(x : F) :
measure_theory.condexp_ind_L1 hm μ s (c • x) = c • measure_theory.condexp_ind_L1 hm μ s x
theorem
measure_theory.norm_condexp_ind_L1_le
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(x : G) :
theorem
measure_theory.continuous_condexp_ind_L1
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)] :
continuous (λ (x : G), measure_theory.condexp_ind_L1 hm μ s x)
theorem
measure_theory.condexp_ind_L1_disjoint_union
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤)
(hst : s ∩ t = ∅)
(x : G) :
measure_theory.condexp_ind_L1 hm μ (s ∪ t) x = measure_theory.condexp_ind_L1 hm μ s x + measure_theory.condexp_ind_L1 hm μ t x
noncomputable
def
measure_theory.condexp_ind
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
[normed_space ℝ G]
{m m0 : measurable_space α}
(hm : m ≤ m0)
(μ : measure_theory.measure α)
[measure_theory.sigma_finite (μ.trim hm)]
(s : set α) :
G →L[ℝ] ↥(measure_theory.Lp G 1 μ)
Conditional expectation of the indicator of a set, as a linear map from G to L1.
Equations
- measure_theory.condexp_ind hm μ s = {to_linear_map := {to_fun := measure_theory.condexp_ind_L1 hm μ s _inst_13, map_add' := _, map_smul' := _}, cont := _}
theorem
measure_theory.condexp_ind_ae_eq_condexp_ind_smul
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
⇑(⇑(measure_theory.condexp_ind hm μ s) x) =ᵐ[μ] ⇑(measure_theory.condexp_ind_smul hm hs hμs x)
theorem
measure_theory.ae_strongly_measurable'_condexp_ind
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
measure_theory.ae_strongly_measurable' m ⇑(⇑(measure_theory.condexp_ind hm μ s) x) μ
@[simp]
theorem
measure_theory.condexp_ind_empty
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)] :
measure_theory.condexp_ind hm μ ∅ = 0
theorem
measure_theory.condexp_ind_smul'
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
[normed_space ℝ F]
[smul_comm_class ℝ 𝕜 F]
(c : 𝕜)
(x : F) :
⇑(measure_theory.condexp_ind hm μ s) (c • x) = c • ⇑(measure_theory.condexp_ind hm μ s) x
theorem
measure_theory.norm_condexp_ind_apply_le
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(x : G) :
theorem
measure_theory.norm_condexp_ind_le
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)] :
theorem
measure_theory.condexp_ind_disjoint_union_apply
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤)
(hst : s ∩ t = ∅)
(x : G) :
⇑(measure_theory.condexp_ind hm μ (s ∪ t)) x = ⇑(measure_theory.condexp_ind hm μ s) x + ⇑(measure_theory.condexp_ind hm μ t) x
theorem
measure_theory.condexp_ind_disjoint_union
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤)
(hst : s ∩ t = ∅) :
measure_theory.condexp_ind hm μ (s ∪ t) = measure_theory.condexp_ind hm μ s + measure_theory.condexp_ind hm μ t
theorem
measure_theory.dominated_fin_meas_additive_condexp_ind
{α : Type u_1}
(G : Type u_5)
[normed_add_comm_group G]
{m m0 : measurable_space α}
[normed_space ℝ G]
(hm : m ≤ m0)
(μ : measure_theory.measure α)
[measure_theory.sigma_finite (μ.trim hm)] :
theorem
measure_theory.set_integral_condexp_ind
{α : Type u_1}
{G' : Type u_6}
[normed_add_comm_group G']
[normed_space ℝ G']
[complete_space G']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤)
(x : G') :
theorem
measure_theory.condexp_ind_of_measurable
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : G) :
⇑(measure_theory.condexp_ind hm μ s) c = measure_theory.indicator_const_Lp 1 _ hμs c
theorem
measure_theory.condexp_ind_nonneg
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{E : Type u_2}
[normed_lattice_add_comm_group E]
[normed_space ℝ E]
[ordered_smul ℝ E]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E)
(hx : 0 ≤ x) :
0 ≤ ⇑(measure_theory.condexp_ind hm μ s) x
noncomputable
def
measure_theory.condexp_L1_clm
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
(hm : m ≤ m0)
(μ : measure_theory.measure α)
[measure_theory.sigma_finite (μ.trim hm)] :
↥(measure_theory.Lp F' 1 μ) →L[ℝ] ↥(measure_theory.Lp F' 1 μ)
Conditional expectation of a function as a linear map from α →₁[μ] F' to itself.
Equations
theorem
measure_theory.condexp_L1_clm_smul
{α : Type u_1}
{F' : Type u_4}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group F']
[normed_space 𝕜 F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(c : 𝕜)
(f : ↥(measure_theory.Lp F' 1 μ)) :
⇑(measure_theory.condexp_L1_clm hm μ) (c • f) = c • ⇑(measure_theory.condexp_L1_clm hm μ) f
theorem
measure_theory.condexp_L1_clm_indicator_const_Lp
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{s : set α}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : F') :
⇑(measure_theory.condexp_L1_clm hm μ) (measure_theory.indicator_const_Lp 1 hs hμs x) = ⇑(measure_theory.condexp_ind hm μ s) x
theorem
measure_theory.condexp_L1_clm_indicator_const
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{s : set α}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : F') :
⇑(measure_theory.condexp_L1_clm hm μ) ↑(measure_theory.Lp.simple_func.indicator_const 1 hs hμs x) = ⇑(measure_theory.condexp_ind hm μ s) x
theorem
measure_theory.set_integral_condexp_L1_clm_of_measure_ne_top
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{s : set α}
(f : ↥(measure_theory.Lp F' 1 μ))
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤) :
Auxiliary lemma used in the proof of set_integral_condexp_L1_clm.
theorem
measure_theory.set_integral_condexp_L1_clm
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{s : set α}
(f : ↥(measure_theory.Lp F' 1 μ))
(hs : measurable_set s) :
The integral of the conditional expectation condexp_L1_clm 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
measure_theory.ae_strongly_measurable'_condexp_L1_clm
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(f : ↥(measure_theory.Lp F' 1 μ)) :
theorem
measure_theory.condexp_L1_clm_Lp_meas
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(f : ↥(measure_theory.Lp_meas F' ℝ m 1 μ)) :
⇑(measure_theory.condexp_L1_clm hm μ) ↑f = ↑f
theorem
measure_theory.condexp_L1_clm_of_ae_strongly_measurable'
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(f : ↥(measure_theory.Lp F' 1 μ))
(hfm : measure_theory.ae_strongly_measurable' m ⇑f μ) :
⇑(measure_theory.condexp_L1_clm hm μ) f = f
noncomputable
def
measure_theory.condexp_L1
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
(hm : m ≤ m0)
(μ : measure_theory.measure α)
[measure_theory.sigma_finite (μ.trim hm)]
(f : α → F') :
↥(measure_theory.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
- measure_theory.condexp_L1 hm μ f = measure_theory.set_to_fun μ (measure_theory.condexp_ind hm μ) _ f
theorem
measure_theory.condexp_L1_undef
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f : α → F'}
(hf : ¬measure_theory.integrable f μ) :
measure_theory.condexp_L1 hm μ f = 0
theorem
measure_theory.condexp_L1_eq
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f : α → F'}
(hf : measure_theory.integrable f μ) :
measure_theory.condexp_L1 hm μ f = ⇑(measure_theory.condexp_L1_clm hm μ) (measure_theory.integrable.to_L1 f hf)
@[simp]
theorem
measure_theory.condexp_L1_zero
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)] :
measure_theory.condexp_L1 hm μ 0 = 0
@[simp]
theorem
measure_theory.condexp_L1_measure_zero
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{f : α → F'}
(hm : m ≤ m0) :
measure_theory.condexp_L1 hm 0 f = 0
theorem
measure_theory.ae_strongly_measurable'_condexp_L1
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f : α → F'} :
theorem
measure_theory.condexp_L1_congr_ae
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → F'}
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(h : f =ᵐ[μ] g) :
measure_theory.condexp_L1 hm μ f = measure_theory.condexp_L1 hm μ g
theorem
measure_theory.integrable_condexp_L1
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(f : α → F') :
theorem
measure_theory.set_integral_condexp_L1
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f : α → F'}
{s : set α}
(hf : measure_theory.integrable f μ)
(hs : measurable_set s) :
The integral of the conditional expectation condexp_L1 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
measure_theory.condexp_L1_add
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f g : α → F'}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.condexp_L1 hm μ (f + g) = measure_theory.condexp_L1 hm μ f + measure_theory.condexp_L1 hm μ g
theorem
measure_theory.condexp_L1_neg
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(f : α → F') :
measure_theory.condexp_L1 hm μ (-f) = -measure_theory.condexp_L1 hm μ f
theorem
measure_theory.condexp_L1_smul
{α : Type u_1}
{F' : Type u_4}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group F']
[normed_space 𝕜 F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(c : 𝕜)
(f : α → F') :
measure_theory.condexp_L1 hm μ (c • f) = c • measure_theory.condexp_L1 hm μ f
theorem
measure_theory.condexp_L1_sub
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f g : α → F'}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.condexp_L1 hm μ (f - g) = measure_theory.condexp_L1 hm μ f - measure_theory.condexp_L1 hm μ g
theorem
measure_theory.condexp_L1_of_ae_strongly_measurable'
{α : Type u_1}
{F' : Type u_4}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f : α → F'}
(hfm : measure_theory.ae_strongly_measurable' m f μ)
(hfi : measure_theory.integrable f μ) :
⇑(measure_theory.condexp_L1 hm μ f) =ᵐ[μ] f
theorem
measure_theory.condexp_L1_mono
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{E : Type u_2}
[normed_lattice_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
[ordered_smul ℝ E]
{f g : α → E}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ)
(hfg : f ≤ᵐ[μ] g) :
⇑(measure_theory.condexp_L1 hm μ f) ≤ᵐ[μ] ⇑(measure_theory.condexp_L1 hm μ g)