# mathlib3documentation

measure_theory.function.conditional_expectation.condexp_L1

# 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 sends x ∈ E to the conditional expectation of the indicator of the set with value x.
• Extend that map to condexp_L1_clm : (α →₁[μ] E) →L[ℝ] (α →₁[μ] E). This is done using the same construction as the Bochner integral (see the file measure_theory/integral/set_to_L1).

## Main definitions #

• condexp_L1: Conditional expectation of a function as a linear map from L1 to 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} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : G) :
μ)

Conditional expectation of the indicator of a measurable set with finite measure, as a function in L1.

Equations
• hμs x = _
theorem measure_theory.condexp_ind_L1_fin_ae_eq_condexp_ind_smul {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : G) :
hμs x) =ᵐ[μ] hμs x)
theorem measure_theory.condexp_ind_L1_fin_add {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x y : G) :
hμs (x + y) = hμs x + hμs y
theorem measure_theory.condexp_ind_L1_fin_smul {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (c : ) (x : G) :
hμs (c x) = c 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 𝕜] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] [ F] [ F] (hs : measurable_set s) (hμs : μ s ) (c : 𝕜) (x : F) :
hμs (c x) = c hμs x
theorem measure_theory.norm_condexp_ind_L1_fin_le {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : G) :
hμs x (μ s).to_real * x
theorem measure_theory.condexp_ind_L1_fin_disjoint_union {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} [ 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) :
= hμs x + hμt x
noncomputable def measure_theory.condexp_ind_L1 {α : Type u_1} {G : Type u_5} [ G] {m m0 : measurable_space α} (hm : m m0) (μ : measure_theory.measure α) (s : set α) [measure_theory.sigma_finite (μ.trim hm)] (x : G) :
μ)

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
theorem measure_theory.condexp_ind_L1_of_measurable_set_of_measure_ne_top {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : G) :
x = hμs x
theorem measure_theory.condexp_ind_L1_of_measure_eq_top {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hμs : μ s = ) (x : G) :
x = 0
theorem measure_theory.condexp_ind_L1_of_not_measurable_set {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : ¬) (x : G) :
x = 0
theorem measure_theory.condexp_ind_L1_add {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (x y : G) :
(x + y) = x + y
theorem measure_theory.condexp_ind_L1_smul {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (c : ) (x : G) :
(c x) = c x
theorem measure_theory.condexp_ind_L1_smul' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] [ F] [ F] (c : 𝕜) (x : F) :
(c x) = c x
theorem measure_theory.norm_condexp_ind_L1_le {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ 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} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] :
continuous (λ (x : G), x)
theorem measure_theory.condexp_ind_L1_disjoint_union {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} [ 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) :
(s t) x = x + x
noncomputable def measure_theory.condexp_ind {α : Type u_1} {G : Type u_5} [ G] {m m0 : measurable_space α} (hm : m m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite (μ.trim hm)] (s : set α) :

Conditional expectation of the indicator of a set, as a linear map from G to L1.

Equations
theorem measure_theory.condexp_ind_ae_eq_condexp_ind_smul {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : G) :
( s) x) =ᵐ[μ] hμs x)
theorem measure_theory.ae_strongly_measurable'_condexp_ind {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : G) :
μ
@[simp]
theorem measure_theory.condexp_ind_empty {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] :
= 0
theorem measure_theory.condexp_ind_smul' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] [ F] [ F] (c : 𝕜) (x : F) :
s) (c x) = c s) x
theorem measure_theory.norm_condexp_ind_apply_le {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ 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} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ 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} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} [ 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) :
(s t)) x = s) x + t) x
theorem measure_theory.condexp_ind_disjoint_union {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} [ 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 = ) :
(s t) = +
theorem measure_theory.set_integral_condexp_ind {α : Type u_1} {G' : Type u_6} [ 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') :
(a : α) in s, ( t) x) a μ = (μ (t s)).to_real x
theorem measure_theory.condexp_ind_of_measurable {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (c : G) :
s) c = 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} [ E] [ E] (hs : measurable_set s) (hμs : μ s ) (x : E) (hx : 0 x) :
0 s) x
noncomputable def measure_theory.condexp_L1_clm {α : Type u_1} {F' : Type u_4} [ F'] [complete_space F'] {m m0 : measurable_space α} (hm : m m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite (μ.trim hm)] :
1 μ) →L[] 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 𝕜] [ F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (c : 𝕜) (f : 1 μ)) :
(c f) = c f
theorem measure_theory.condexp_L1_clm_indicator_const_Lp {α : Type u_1} {F' : Type u_4} [ 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') :
hμs x) = s) x
theorem measure_theory.condexp_L1_clm_indicator_const {α : Type u_1} {F' : Type u_4} [ 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') :
x) = s) x
theorem measure_theory.set_integral_condexp_L1_clm_of_measure_ne_top {α : Type u_1} {F' : Type u_4} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {s : set α} (f : 1 μ)) (hs : measurable_set s) (hμs : μ s ) :
(x : α) in s, ( f) x μ = (x : α) in s, f x μ

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} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {s : set α} (f : 1 μ)) (hs : measurable_set s) :
(x : α) in s, ( f) x μ = (x : α) in s, f x μ

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} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (f : 1 μ)) :
theorem measure_theory.condexp_L1_clm_Lp_meas {α : Type u_1} {F' : Type u_4} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (f : m 1 μ)) :
f = f
theorem measure_theory.condexp_L1_clm_of_ae_strongly_measurable' {α : Type u_1} {F' : Type u_4} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (f : 1 μ)) (hfm : μ) :
f = f
noncomputable def measure_theory.condexp_L1 {α : Type u_1} {F' : Type u_4} [ F'] [complete_space F'] {m m0 : measurable_space α} (hm : m m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite (μ.trim hm)] (f : α 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
• = f
theorem measure_theory.condexp_L1_undef {α : Type u_1} {F' : Type u_4} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f : α F'} (hf : ¬) :
= 0
theorem measure_theory.condexp_L1_eq {α : Type u_1} {F' : Type u_4} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f : α F'} (hf : μ) :
=
@[simp]
theorem measure_theory.condexp_L1_zero {α : Type u_1} {F' : Type u_4} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] :
= 0
@[simp]
theorem measure_theory.condexp_L1_measure_zero {α : Type u_1} {F' : Type u_4} [ F'] [complete_space F'] {m m0 : measurable_space α} {f : α F'} (hm : m m0) :
= 0
theorem measure_theory.ae_strongly_measurable'_condexp_L1 {α : Type u_1} {F' : Type u_4} [ 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} [ 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) :
=
theorem measure_theory.integrable_condexp_L1 {α : Type u_1} {F' : Type u_4} [ 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} [ 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 : μ) (hs : measurable_set s) :
(x : α) in s, f) x μ = (x : α) in s, f x μ

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} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f g : α F'} (hf : μ) (hg : μ) :
(f + g) = +
theorem measure_theory.condexp_L1_neg {α : Type u_1} {F' : Type u_4} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (f : α F') :
(-f) = -
theorem measure_theory.condexp_L1_smul {α : Type u_1} {F' : Type u_4} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (c : 𝕜) (f : α F') :
(c f) = c
theorem measure_theory.condexp_L1_sub {α : Type u_1} {F' : Type u_4} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f g : α F'} (hf : μ) (hg : μ) :
(f - g) = -
theorem measure_theory.condexp_L1_of_ae_strongly_measurable' {α : Type u_1} {F' : Type u_4} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f : α F'} (hfm : μ) (hfi : μ) :
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} [ E] [ E] {f g : α E} (hf : μ) (hg : μ) (hfg : f ≤ᵐ[μ] g) :
f) ≤ᵐ[μ] g)