From e14cf589accbd72d970ef8486ca2d9c39f58c346 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Degenne?= <Remydegenne@gmail.com>
Date: Fri, 24 Sep 2021 12:53:07 +0000
Subject: [PATCH] feat(measure_theory/function/conditional_expectation): define
 the conditional expectation of a function, prove the equality of integrals
 (#9114)

This PR puts together the generalized Bochner integral construction of #8939 and the set function `condexp_ind` of #8920 to define the conditional expectation of a function.

The equality of integrals that defines the conditional expectation is proven in `set_integral_condexp`.
---
 .../decomposition/radon_nikodym.lean          |   4 +-
 .../function/conditional_expectation.lean     | 537 +++++++++++++++++-
 src/measure_theory/integral/set_integral.lean |  15 +
 3 files changed, 551 insertions(+), 5 deletions(-)

diff --git a/src/measure_theory/decomposition/radon_nikodym.lean b/src/measure_theory/decomposition/radon_nikodym.lean
index 3a4f18d607232..f42b12d7b9e05 100644
--- a/src/measure_theory/decomposition/radon_nikodym.lean
+++ b/src/measure_theory/decomposition/radon_nikodym.lean
@@ -14,7 +14,9 @@ This file proves the Radon-Nikodym theorem. The Radon-Nikodym theorem states tha
 In particular, we have `f = radon_nikodym_deriv μ ν`.
 
 The Radon-Nikodym theorem will allow us to define many important concepts in probability theory,
-most notably conditional expectations and probability cumulative functions.
+most notably probability cumulative functions. It could also be used to define the conditional
+expectation of a real function, but we take a different approach (see the file
+`measure_theory/function/conditional_expectation`).
 
 ## Main results
 
diff --git a/src/measure_theory/function/conditional_expectation.lean b/src/measure_theory/function/conditional_expectation.lean
index 1bff2c8c05e83..d8fa51dde899b 100644
--- a/src/measure_theory/function/conditional_expectation.lean
+++ b/src/measure_theory/function/conditional_expectation.lean
@@ -9,15 +9,67 @@ import measure_theory.function.ae_eq_of_integral
 
 /-! # Conditional expectation
 
-We build the conditional expectation with respect to a sub-sigma-algebra `m` in three steps:
+We build the conditional expectation of a function `f` with value in a Banach space with respect to
+a measure `μ` (defined on a measurable space structure `m0`) and a measurable space structure `m`
+with `hm : m ≤ m0` (a sub-sigma-algebra). This is an `m`-measurable function `μ[f|hm]` which is
+integrable and verifies `∫ x in s, μ[f|hm] x ∂μ = ∫ x in s, f x ∂μ` for any `m`-measurable sets `s`.
+It is unique as an element of `L¹`.
+
+The construction is done in four steps:
 * Define the conditional expectation of an `L²` function, as an element of `L²`. This is the
   orthogonal projection on the subspace of almost everywhere `m`-measurable functions.
 * 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 `(α →₁[μ] E) →L[𝕜] (α →₁[μ] E)`. This is done using the same construction as
-  the Bochner integral. TODO.
+* 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`).
+* Define the conditional expectation of a function `f : α → E`, which is an integrable function
+  `α → E` equal to 0 if `f` is not integrable, and equal to an `m`-measurable representative of
+  `condexp_L1_clm` applied to `[f]`, the equivalence class of `f` in `L¹`.
+
+## Main results
+
+The conditional expectation and its properties
+
+* `condexp (hm : m ≤ m0) (μ : measure α) (f : α → E)`: conditional expectation of `f` with respect
+  to `m`.
+* `integrable_condexp` : `condexp` is integrable.
+* `measurable_condexp` : `condexp` is `m`-measurable.
+* `set_integral_condexp (hf : integrable f μ) (hs : measurable_set[m] s)` : the conditional
+  expectation verifies `∫ x in s, condexp hm μ f x ∂μ = ∫ x in s, f x ∂μ` for any `m`-measurable
+  set `s`.
+
+While `condexp` is function-valued, we also define `condexp_L1` with value in `L1` and a continuous
+linear map `condexp_L1_clm` from `L1` to `L1`. `condexp` should be used in most cases.
+
+Uniqueness of the conditional expectation
+
+* `Lp.ae_eq_of_forall_set_integral_eq'`: two `Lp` functions verifying the equality of integrals
+  defining the conditional expectation are equal everywhere.
+* `ae_eq_of_forall_set_integral_eq_of_sigma_finite'`: two functions verifying the equality of
+  integrals defining the conditional expectation are equal everywhere.
+  Requires `[sigma_finite (μ.trim hm)]`.
+* `ae_eq_condexp_of_forall_set_integral_eq`: an a.e. `m`-measurable function which verifies the
+  equality of integrals is a.e. equal to `condexp`.
+
+## Notations
+
+For a measure `μ` defined on a measurable space structure `m0`, another measurable space structure
+`m` with `hm : m ≤ m0` (a sub-sigma-algebra) and a function `f`, we define the notation
+* `μ[f|hm] = condexp hm μ f`.
+
+## Implementation notes
+
+Most of the results in this file are valid for a second countable, borel, real normed space `F`.
+However, some lemmas also use `𝕜 : is_R_or_C`:
+* `condexp_L2` is defined only for an `inner_product_space` for now, and we use `𝕜` for its field.
+* results about scalar multiplication are stated not only for `ℝ` but also for `𝕜` if we happen to
+  have `normed_space 𝕜 F` and `is_scalar_tower ℝ 𝕜 F'`.
+
+## Tags
+
+conditional expectation, conditional expected value
 
 -/
 
@@ -260,12 +312,24 @@ def Lp_meas_subgroup_to_Lp_trim (hm : m ≤ m0) (f : Lp_meas_subgroup F m p μ)
 mem_ℒp.to_Lp (mem_Lp_meas_subgroup_iff_ae_measurable'.mp f.mem).some
   (mem_ℒp_trim_of_mem_Lp_meas_subgroup hm f f.mem)
 
+variables (𝕜)
+/-- Map from `Lp_meas` to `Lp F p (μ.trim hm)`. -/
+def Lp_meas_to_Lp_trim (hm : m ≤ m0) (f : Lp_meas F 𝕜 m p μ) : Lp F p (μ.trim hm) :=
+mem_ℒp.to_Lp (mem_Lp_meas_iff_ae_measurable'.mp f.mem).some
+  (mem_ℒp_trim_of_mem_Lp_meas_subgroup hm f f.mem)
+variables {𝕜}
+
 /-- Map from `Lp F p (μ.trim hm)` to `Lp_meas_subgroup`, inverse of
 `Lp_meas_subgroup_to_Lp_trim`. -/
 def Lp_trim_to_Lp_meas_subgroup (hm : m ≤ m0) (f : Lp F p (μ.trim hm)) : Lp_meas_subgroup F m p μ :=
 ⟨(mem_ℒp_of_mem_ℒp_trim hm (Lp.mem_ℒp f)).to_Lp f, mem_Lp_meas_subgroup_to_Lp_of_trim hm f⟩
 
-variables {F p μ}
+variables (𝕜)
+/-- Map from `Lp F p (μ.trim hm)` to `Lp_meas`, inverse of `Lp_meas_to_Lp_trim`. -/
+def Lp_trim_to_Lp_meas (hm : m ≤ m0) (f : Lp F p (μ.trim hm)) : Lp_meas F 𝕜 m p μ :=
+⟨(mem_ℒp_of_mem_ℒp_trim hm (Lp.mem_ℒp f)).to_Lp f, mem_Lp_meas_subgroup_to_Lp_of_trim hm f⟩
+
+variables {F 𝕜 p μ}
 
 lemma Lp_meas_subgroup_to_Lp_trim_ae_eq (hm : m ≤ m0) (f : Lp_meas_subgroup F m p μ) :
   Lp_meas_subgroup_to_Lp_trim F p μ hm f =ᵐ[μ] f :=
@@ -276,6 +340,15 @@ lemma Lp_trim_to_Lp_meas_subgroup_ae_eq (hm : m ≤ m0) (f : Lp F p (μ.trim hm)
   Lp_trim_to_Lp_meas_subgroup F p μ hm f =ᵐ[μ] f :=
 mem_ℒp.coe_fn_to_Lp _
 
+lemma Lp_meas_to_Lp_trim_ae_eq (hm : m ≤ m0) (f : Lp_meas F 𝕜 m p μ) :
+  Lp_meas_to_Lp_trim F 𝕜 p μ hm f =ᵐ[μ] f :=
+(ae_eq_of_ae_eq_trim (mem_ℒp.coe_fn_to_Lp (mem_ℒp_trim_of_mem_Lp_meas_subgroup hm ↑f f.mem))).trans
+  (mem_Lp_meas_subgroup_iff_ae_measurable'.mp f.mem).some_spec.2.symm
+
+lemma Lp_trim_to_Lp_meas_ae_eq (hm : m ≤ m0) (f : Lp F p (μ.trim hm)) :
+  Lp_trim_to_Lp_meas F 𝕜 p μ hm f =ᵐ[μ] f :=
+mem_ℒp.coe_fn_to_Lp _
+
 /-- `Lp_trim_to_Lp_meas_subgroup` is a right inverse of `Lp_meas_subgroup_to_Lp_trim`. -/
 lemma Lp_meas_subgroup_to_Lp_trim_right_inv (hm : m ≤ m0) :
   function.right_inverse (Lp_trim_to_Lp_meas_subgroup F p μ hm)
@@ -338,6 +411,20 @@ lemma Lp_meas_subgroup_to_Lp_trim_sub (hm : m ≤ m0) (f g : Lp_meas_subgroup F
 by rw [sub_eq_add_neg, sub_eq_add_neg, Lp_meas_subgroup_to_Lp_trim_add,
   Lp_meas_subgroup_to_Lp_trim_neg]
 
+lemma Lp_meas_to_Lp_trim_smul (hm : m ≤ m0) (c : 𝕜) (f : Lp_meas F 𝕜 m p μ) :
+  Lp_meas_to_Lp_trim F 𝕜 p μ hm (c • f) = c • Lp_meas_to_Lp_trim F 𝕜 p μ hm f :=
+begin
+  ext1,
+  refine eventually_eq.trans _ (Lp.coe_fn_smul _ _).symm,
+  refine ae_eq_trim_of_measurable hm (Lp.measurable _) _ _,
+  { exact @measurable.const_smul _ _ α _ _ _ m _ _ (Lp.measurable _) c, },
+  refine (Lp_meas_to_Lp_trim_ae_eq hm _).trans _,
+  refine (Lp.coe_fn_smul _ _).trans _,
+  refine (Lp_meas_to_Lp_trim_ae_eq hm f).mono (λ x hx, _),
+  rw [pi.smul_apply, pi.smul_apply, hx],
+  refl,
+end
+
 /-- `Lp_meas_subgroup_to_Lp_trim` preserves the norm. -/
 lemma Lp_meas_subgroup_to_Lp_trim_norm_map [hp : fact (1 ≤ p)] (hm : m ≤ m0)
   (f : Lp_meas_subgroup F m p μ) :
@@ -373,6 +460,17 @@ variables (𝕜)
 def Lp_meas_subgroup_to_Lp_meas_iso [hp : fact (1 ≤ p)] :
   Lp_meas_subgroup F m p μ ≃ᵢ Lp_meas F 𝕜 m p μ :=
 isometric.refl (Lp_meas_subgroup F m p μ)
+
+/-- `Lp_meas` and `Lp F p (μ.trim hm)` are isometric, with a linear equivalence. -/
+def Lp_meas_to_Lp_trim_lie [hp : fact (1 ≤ p)] (hm : m ≤ m0) :
+  Lp_meas F 𝕜 m p μ ≃ₗᵢ[𝕜] Lp F p (μ.trim hm) :=
+{ to_fun    := Lp_meas_to_Lp_trim F 𝕜 p μ hm,
+  inv_fun   := Lp_trim_to_Lp_meas F 𝕜 p μ hm,
+  left_inv  := Lp_meas_subgroup_to_Lp_trim_left_inv hm,
+  right_inv := Lp_meas_subgroup_to_Lp_trim_right_inv hm,
+  map_add'  := Lp_meas_subgroup_to_Lp_trim_add hm,
+  map_smul' := Lp_meas_to_Lp_trim_smul hm,
+  norm_map' := Lp_meas_subgroup_to_Lp_trim_norm_map hm, }
 variables {F 𝕜 p μ}
 
 instance [hm : fact (m ≤ m0)] [complete_space F] [hp : fact (1 ≤ p)] :
@@ -1003,6 +1101,20 @@ begin
   simp only [coe_fn_coe_base, submodule.coe_zero, continuous_linear_map.map_zero],
 end
 
+lemma set_integral_condexp_ind_smul (hs : measurable_set[m] s) (ht : measurable_set t)
+  (hμs : μ s ≠ ∞) (hμt : μ t ≠ ∞) (x : G') :
+  ∫ a in s, (condexp_ind_smul hm ht hμt x) a ∂μ = (μ (t ∩ s)).to_real • x :=
+calc ∫ a in s, (condexp_ind_smul hm ht hμt x) a ∂μ
+    = (∫ a in s, (condexp_L2 ℝ hm (indicator_const_Lp 2 ht hμt (1 : ℝ)) a • x) ∂μ) :
+  set_integral_congr_ae (hm s hs) ((condexp_ind_smul_ae_eq_smul hm ht hμt x).mono (λ x hx hxs, hx))
+... = (∫ a in s, condexp_L2 ℝ hm (indicator_const_Lp 2 ht hμt (1 : ℝ)) a ∂μ) • x :
+  by rw integral_smul_const _ x
+... = (∫ a in s, indicator_const_Lp 2 ht hμt (1 : ℝ) a ∂μ) • x :
+  by rw @integral_condexp_L2_eq α _ ℝ _ _ _ _ _ _ _ _ _ _ _ _ _ _ hm
+    (indicator_const_Lp 2 ht hμt (1 : ℝ)) hs hμs
+... = (μ (t ∩ s)).to_real • x :
+  by rw [set_integral_indicator_const_Lp (hm s hs), smul_assoc, one_smul]
+
 end condexp_ind_smul
 
 end condexp_L2
@@ -1266,6 +1378,423 @@ lemma condexp_ind_disjoint_union (hs : measurable_set s) (ht : measurable_set t)
   (condexp_ind hm μ (s ∪ t) : G →L[ℝ] α →₁[μ] G) = condexp_ind hm μ s + condexp_ind hm μ t :=
 by { ext1, push_cast, exact condexp_ind_disjoint_union_apply hs ht hμs hμt hst x, }
 
+variables (G)
+
+lemma dominated_fin_meas_additive_condexp_ind (hm : m ≤ m0) (μ : measure α)
+  [sigma_finite (μ.trim hm)] :
+  dominated_fin_meas_additive μ (condexp_ind hm μ : set α → G →L[ℝ] α →₁[μ] G) 1 :=
+⟨λ s t, condexp_ind_disjoint_union, λ s, norm_condexp_ind_le.trans (one_mul _).symm.le⟩
+
+variables {G}
+
+lemma set_integral_condexp_ind (hs : measurable_set[m] s) (ht : measurable_set t) (hμs : μ s ≠ ∞)
+  (hμt : μ t ≠ ∞) (x : G') :
+  ∫ a in s, condexp_ind hm μ t x a ∂μ = (μ (t ∩ s)).to_real • x :=
+calc
+∫ a in s, condexp_ind hm μ t x a ∂μ = ∫ a in s, condexp_ind_smul hm ht hμt x a ∂μ :
+  set_integral_congr_ae (hm s hs)
+    ((condexp_ind_ae_eq_condexp_ind_smul hm ht hμt x).mono (λ x hx hxs, hx))
+... = (μ (t ∩ s)).to_real • x : set_integral_condexp_ind_smul hs ht hμs hμt x
+
+lemma condexp_ind_of_measurable (hs : measurable_set[m] s) (hμs : μ s ≠ ∞) (c : G) :
+  condexp_ind hm μ s c = indicator_const_Lp 1 (hm s hs) hμs c :=
+begin
+  ext1,
+  refine eventually_eq.trans _ indicator_const_Lp_coe_fn.symm,
+  refine (condexp_ind_ae_eq_condexp_ind_smul hm (hm s hs) hμs c).trans _,
+  refine (condexp_ind_smul_ae_eq_smul hm (hm s hs) hμs c).trans _,
+  rw [Lp_meas_coe, condexp_L2_indicator_of_measurable hm hs hμs (1 : ℝ)],
+  refine (@indicator_const_Lp_coe_fn α _ _ 2 μ _ _ s (hm s hs) hμs (1 : ℝ) _ _).mono (λ x hx, _),
+  dsimp only,
+  rw hx,
+  by_cases hx_mem : x ∈ s; simp [hx_mem],
+end
+
 end condexp_ind
 
+section condexp_L1
+
+local attribute [instance] fact_one_le_one_ennreal
+
+variables {m m0 : measurable_space α} {μ : measure α} [borel_space 𝕜] [is_scalar_tower ℝ 𝕜 F']
+  {hm : m ≤ m0} [sigma_finite (μ.trim hm)] {f g : α → F'} {s : set α}
+
+/-- Conditional expectation of a function as a linear map from `α →₁[μ] F'` to itself. -/
+def condexp_L1_clm (hm : m ≤ m0) (μ : measure α) [sigma_finite (μ.trim hm)] :
+  (α →₁[μ] F') →L[ℝ] α →₁[μ] F' :=
+L1.set_to_L1 (dominated_fin_meas_additive_condexp_ind F' hm μ)
+
+lemma condexp_L1_clm_smul (c : 𝕜) (f : α →₁[μ] F') :
+  condexp_L1_clm hm μ (c • f) = c • condexp_L1_clm hm μ f :=
+L1.set_to_L1_smul (dominated_fin_meas_additive_condexp_ind F' hm μ)
+  (λ c s x, condexp_ind_smul' c x) c f
+
+lemma condexp_L1_clm_indicator_const_Lp (hs : measurable_set s) (hμs : μ s ≠ ∞) (x : F') :
+  (condexp_L1_clm hm μ) (indicator_const_Lp 1 hs hμs x) = condexp_ind hm μ s x :=
+L1.set_to_L1_indicator_const_Lp (dominated_fin_meas_additive_condexp_ind F' hm μ) hs hμs x
+
+lemma condexp_L1_clm_indicator_const (hs : measurable_set s) (hμs : μ s ≠ ∞) (x : F') :
+  (condexp_L1_clm hm μ) ↑(simple_func.indicator_const 1 hs hμs x) = condexp_ind hm μ s x :=
+by { rw Lp.simple_func.coe_indicator_const, exact condexp_L1_clm_indicator_const_Lp hs hμs x, }
+
+/-- Auxiliary lemma used in the proof of `set_integral_condexp_L1_clm`. -/
+lemma set_integral_condexp_L1_clm_of_measure_ne_top (f : α →₁[μ] F') (hs : measurable_set[m] s)
+  (hμs : μ s ≠ ∞) :
+  ∫ x in s, condexp_L1_clm hm μ f x ∂μ = ∫ x in s, f x ∂μ :=
+begin
+  refine Lp.induction ennreal.one_ne_top
+    (λ f : α →₁[μ] F', ∫ x in s, condexp_L1_clm hm μ f x ∂μ = ∫ x in s, f x ∂μ)
+  _ _ (is_closed_eq _ _) f,
+  { intros x t ht hμt,
+    simp_rw condexp_L1_clm_indicator_const ht hμt.ne x,
+    rw [Lp.simple_func.coe_indicator_const, set_integral_indicator_const_Lp (hm _ hs)],
+    exact set_integral_condexp_ind hs ht hμs hμt.ne x, },
+  { intros f g hf_Lp hg_Lp hfg_disj hf hg,
+    simp_rw (condexp_L1_clm hm μ).map_add,
+    rw set_integral_congr_ae (hm s hs) ((Lp.coe_fn_add (condexp_L1_clm hm μ (hf_Lp.to_Lp f))
+      (condexp_L1_clm hm μ (hg_Lp.to_Lp g))).mono (λ x hx hxs, hx)),
+    rw set_integral_congr_ae (hm s hs) ((Lp.coe_fn_add (hf_Lp.to_Lp f) (hg_Lp.to_Lp g)).mono
+      (λ x hx hxs, hx)),
+    simp_rw pi.add_apply,
+    rw [integral_add (L1.integrable_coe_fn _).integrable_on (L1.integrable_coe_fn _).integrable_on,
+      integral_add (L1.integrable_coe_fn _).integrable_on (L1.integrable_coe_fn _).integrable_on,
+      hf, hg], },
+  { exact (continuous_set_integral s).comp (condexp_L1_clm hm μ).continuous, },
+  { exact continuous_set_integral s, },
+end
+
+/-- 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`. -/
+lemma set_integral_condexp_L1_clm (f : α →₁[μ] F') (hs : measurable_set[m] s) :
+  ∫ x in s, condexp_L1_clm hm μ f x ∂μ = ∫ x in s, f x ∂μ :=
+begin
+  let S := spanning_sets (μ.trim hm),
+  have hS_meas : ∀ i, measurable_set[m] (S i) := measurable_spanning_sets (μ.trim hm),
+  have hS_meas0 : ∀ i, measurable_set (S i) := λ i, hm _ (hS_meas i),
+  have hs_eq : s = ⋃ i, S i ∩ s,
+  { simp_rw set.inter_comm,
+    rw [← set.inter_Union, (Union_spanning_sets (μ.trim hm)), set.inter_univ], },
+  have hS_finite : ∀ i, μ (S i ∩ s) < ∞,
+  { refine λ i, (measure_mono (set.inter_subset_left _ _)).trans_lt _,
+    have hS_finite_trim := measure_spanning_sets_lt_top (μ.trim hm) i,
+    rwa trim_measurable_set_eq hm (hS_meas i) at hS_finite_trim, },
+  have h_mono : monotone (λ i, (S i) ∩ s),
+  { intros i j hij x,
+    simp_rw set.mem_inter_iff,
+    exact λ h, ⟨monotone_spanning_sets (μ.trim hm) hij h.1, h.2⟩, },
+  have h_eq_forall : (λ i, ∫ x in (S i) ∩ s, condexp_L1_clm hm μ f x ∂μ)
+      = λ i, ∫ x in (S i) ∩ s, f x ∂μ,
+    from funext (λ i, set_integral_condexp_L1_clm_of_measure_ne_top f
+      (@measurable_set.inter α m _ _ (hS_meas i) hs) (hS_finite i).ne),
+  have h_right : tendsto (λ i, ∫ x in (S i) ∩ s, f x ∂μ) at_top (𝓝 (∫ x in s, f x ∂μ)),
+  { have h := tendsto_set_integral_of_monotone (λ i, (hS_meas0 i).inter (hm s hs)) h_mono
+      (L1.integrable_coe_fn f).integrable_on,
+    rwa ← hs_eq at h, },
+  have h_left : tendsto (λ i, ∫ x in (S i) ∩ s, condexp_L1_clm hm μ f x ∂μ) at_top
+    (𝓝 (∫ x in s, condexp_L1_clm hm μ f x ∂μ)),
+  { have h := tendsto_set_integral_of_monotone (λ i, (hS_meas0 i).inter (hm s hs))
+      h_mono (L1.integrable_coe_fn (condexp_L1_clm hm μ f)).integrable_on,
+    rwa ← hs_eq at h, },
+  rw h_eq_forall at h_left,
+  exact tendsto_nhds_unique h_left h_right,
+end
+
+lemma ae_measurable'_condexp_L1_clm (f : α →₁[μ] F') : ae_measurable' m (condexp_L1_clm hm μ f) μ :=
+begin
+  refine Lp.induction ennreal.one_ne_top
+    (λ f : α →₁[μ] F', ae_measurable' m (condexp_L1_clm hm μ f) μ)
+    _ _ _ f,
+  { intros c s hs hμs,
+    rw condexp_L1_clm_indicator_const hs hμs.ne c,
+    exact ae_measurable'_condexp_ind hs hμs.ne c, },
+  { intros f g hf hg h_disj hfm hgm,
+    rw (condexp_L1_clm hm μ).map_add,
+    refine ae_measurable'.congr _ (coe_fn_add _ _).symm,
+    exact ae_measurable'.add hfm hgm, },
+  { have : {f : Lp F' 1 μ | ae_measurable' m (condexp_L1_clm hm μ f) μ}
+        = (condexp_L1_clm hm μ) ⁻¹' {f | ae_measurable' m f μ},
+      by refl,
+    rw this,
+    refine is_closed.preimage (condexp_L1_clm hm μ).continuous _,
+    exact is_closed_ae_measurable' hm, },
+end
+
+lemma Lp_meas_to_Lp_trim_lie_symm_indicator [normed_space ℝ F] {μ : measure α}
+  (hs : measurable_set[m] s) (hμs : μ.trim hm s ≠ ∞) (c : F) :
+  ((Lp_meas_to_Lp_trim_lie F ℝ 1 μ hm).symm
+      (indicator_const_Lp 1 hs hμs c) : α →₁[μ] F)
+    = indicator_const_Lp 1 (hm s hs) ((le_trim hm).trans_lt hμs.lt_top).ne c :=
+begin
+  ext1,
+  rw ← Lp_meas_coe,
+  change Lp_trim_to_Lp_meas F ℝ 1 μ hm (indicator_const_Lp 1 hs hμs c)
+    =ᵐ[μ] (indicator_const_Lp 1 _ _ c : α → F),
+  refine (Lp_trim_to_Lp_meas_ae_eq hm _).trans _,
+  exact (ae_eq_of_ae_eq_trim indicator_const_Lp_coe_fn).trans indicator_const_Lp_coe_fn.symm,
+end
+
+lemma condexp_L1_clm_Lp_meas (f : Lp_meas F' ℝ m 1 μ) :
+  condexp_L1_clm hm μ (f : α →₁[μ] F') = ↑f :=
+begin
+  let g := Lp_meas_to_Lp_trim_lie F' ℝ 1 μ hm f,
+  have hfg : f = (Lp_meas_to_Lp_trim_lie F' ℝ 1 μ hm).symm g,
+    by simp only [linear_isometry_equiv.symm_apply_apply],
+  rw hfg,
+  refine @Lp.induction α F' m _ _ _ _ 1 (μ.trim hm) _ ennreal.coe_ne_top
+    (λ g : α →₁[μ.trim hm] F',
+      condexp_L1_clm hm μ ((Lp_meas_to_Lp_trim_lie F' ℝ 1 μ hm).symm g : α →₁[μ] F')
+        = ↑((Lp_meas_to_Lp_trim_lie F' ℝ 1 μ hm).symm g)) _ _ _ g,
+  { intros c s hs hμs,
+    rw [Lp.simple_func.coe_indicator_const, Lp_meas_to_Lp_trim_lie_symm_indicator hs hμs.ne c,
+      condexp_L1_clm_indicator_const_Lp],
+    exact condexp_ind_of_measurable hs ((le_trim hm).trans_lt hμs).ne c, },
+  { intros f g hf hg hfg_disj hf_eq hg_eq,
+    rw linear_isometry_equiv.map_add,
+    push_cast,
+    rw [map_add, hf_eq, hg_eq], },
+  { refine is_closed_eq _ _,
+    { refine (condexp_L1_clm hm μ).continuous.comp (continuous_induced_dom.comp _),
+      exact linear_isometry_equiv.continuous _, },
+    { refine continuous_induced_dom.comp _,
+      exact linear_isometry_equiv.continuous _, }, },
+end
+
+lemma condexp_L1_clm_of_ae_measurable' (f : α →₁[μ] F') (hfm : ae_measurable' m f μ) :
+  condexp_L1_clm hm μ f = f :=
+condexp_L1_clm_Lp_meas (⟨f, hfm⟩ : Lp_meas F' ℝ m 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. -/
+def condexp_L1 (hm : m ≤ m0) (μ : measure α) [sigma_finite (μ.trim hm)] (f : α → F') : α →₁[μ] F' :=
+set_to_fun (dominated_fin_meas_additive_condexp_ind F' hm μ) f
+
+lemma condexp_L1_undef (hf : ¬ integrable f μ) : condexp_L1 hm μ f = 0 :=
+set_to_fun_undef (dominated_fin_meas_additive_condexp_ind F' hm μ) hf
+
+lemma condexp_L1_eq (hf : integrable f μ) :
+  condexp_L1 hm μ f = condexp_L1_clm hm μ (hf.to_L1 f) :=
+set_to_fun_eq (dominated_fin_meas_additive_condexp_ind F' hm μ) hf
+
+lemma condexp_L1_zero : condexp_L1 hm μ (0 : α → F') = 0 :=
+begin
+  refine (condexp_L1_eq (integrable_zero _ _ _)).trans _,
+  change (condexp_L1_clm hm μ) (integrable.to_L1 0 _) = 0,
+  rw [integrable.to_L1_zero, continuous_linear_map.map_zero],
+end
+
+lemma ae_measurable'_condexp_L1 {f : α → F'} : ae_measurable' m (condexp_L1 hm μ f) μ :=
+begin
+  by_cases hf : integrable f μ,
+  { rw condexp_L1_eq hf,
+    exact ae_measurable'_condexp_L1_clm _, },
+  { rw condexp_L1_undef hf,
+    refine ae_measurable'.congr _ (coe_fn_zero _ _ _).symm,
+    exact measurable.ae_measurable' (@measurable_zero _ _ _ m _), },
+end
+
+lemma integrable_condexp_L1 (f : α → F') : integrable (condexp_L1 hm μ f) μ :=
+L1.integrable_coe_fn _
+
+/-- 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`. -/
+lemma set_integral_condexp_L1 (hf : integrable f μ) (hs : measurable_set[m] s) :
+  ∫ x in s, condexp_L1 hm μ f x ∂μ = ∫ x in s, f x ∂μ :=
+begin
+  simp_rw condexp_L1_eq hf,
+  rw set_integral_condexp_L1_clm (hf.to_L1 f) hs,
+  exact set_integral_congr_ae (hm s hs) ((hf.coe_fn_to_L1).mono (λ x hx hxs, hx)),
+end
+
+lemma condexp_L1_add (hf : integrable f μ) (hg : integrable g μ) :
+  condexp_L1 hm μ (f + g) = condexp_L1 hm μ f + condexp_L1 hm μ g :=
+calc condexp_L1 hm μ (f + g) = condexp_L1_clm hm μ ((hf.add hg).to_L1 (f + g)) :
+  condexp_L1_eq (hf.add hg)
+... = condexp_L1_clm hm μ (hf.to_L1 f + hg.to_L1 g) : by rw integrable.to_L1_add _ _ hf hg
+... = condexp_L1_clm hm μ (hf.to_L1 f) + condexp_L1_clm hm μ (hg.to_L1 g) :
+  (condexp_L1_clm hm μ).map_add _ _
+... = condexp_L1 hm μ f + condexp_L1 hm μ g :
+  by rw [condexp_L1_eq hf, condexp_L1_eq hg]
+
+lemma condexp_L1_neg (f : α → F') :
+  condexp_L1 hm μ (-f) = - condexp_L1 hm μ f :=
+begin
+  by_cases hf : integrable f μ,
+  { calc condexp_L1 hm μ (-f) = condexp_L1_clm hm μ (hf.neg.to_L1 (-f)) : condexp_L1_eq hf.neg
+    ... = condexp_L1_clm hm μ (- hf.to_L1 f) : by rw integrable.to_L1_neg _ hf
+    ... = - condexp_L1_clm hm μ (hf.to_L1 f) : (condexp_L1_clm hm μ).map_neg _
+    ... = - condexp_L1 hm μ f : by rw condexp_L1_eq hf, },
+  { rw [condexp_L1_undef hf, condexp_L1_undef (mt integrable_neg_iff.mp hf), neg_zero], },
+end
+
+lemma condexp_L1_smul (c : 𝕜) (f : α → F') :
+  condexp_L1 hm μ (c • f) = c • condexp_L1 hm μ f :=
+begin
+  by_cases hf : integrable f μ,
+  { calc condexp_L1 hm μ (c • f) = condexp_L1_clm hm μ ((hf.smul c).to_L1 (c • f)) :
+      condexp_L1_eq (hf.smul c)
+    ... = condexp_L1_clm hm μ (c • hf.to_L1 f) : by rw integrable.to_L1_smul' _ hf c
+    ... = c • condexp_L1_clm hm μ (hf.to_L1 f) : condexp_L1_clm_smul c (hf.to_L1 f)
+    ... = c • condexp_L1 hm μ f : by rw condexp_L1_eq hf, },
+  { by_cases hc : c = 0,
+    { rw [hc, zero_smul, zero_smul, condexp_L1_zero], },
+    rw [condexp_L1_undef hf, condexp_L1_undef (mt (integrable_smul_iff hc f).mp hf), smul_zero], },
+end
+
+lemma condexp_L1_sub (hf : integrable f μ) (hg : integrable g μ) :
+  condexp_L1 hm μ (f - g) = condexp_L1 hm μ f - condexp_L1 hm μ g :=
+by rw [sub_eq_add_neg, sub_eq_add_neg, condexp_L1_add hf hg.neg, condexp_L1_neg g]
+
+lemma condexp_L1_of_ae_measurable' (hfm : ae_measurable' m f μ) (hfi : integrable f μ) :
+  condexp_L1 hm μ f =ᵐ[μ] f :=
+begin
+  rw condexp_L1_eq hfi,
+  refine eventually_eq.trans _ (integrable.coe_fn_to_L1 hfi),
+  rw condexp_L1_clm_of_ae_measurable',
+  exact ae_measurable'.congr hfm (integrable.coe_fn_to_L1 hfi).symm,
+end
+
+end condexp_L1
+
+section condexp
+
+/-! ### Conditional expectation of a function -/
+
+open_locale classical
+
+local attribute [instance] fact_one_le_one_ennreal
+
+variables {𝕜} {m m0 : measurable_space α} {μ : measure α} [borel_space 𝕜] [is_scalar_tower ℝ 𝕜 F']
+  {hm : m ≤ m0} [sigma_finite (μ.trim hm)] {f g : α → F'} {s : set α}
+
+/-- Conditional expectation of a function. Its value is 0 if the function is not integrable. -/
+@[irreducible] def condexp (hm : m ≤ m0) (μ : measure α) [sigma_finite (μ.trim hm)] (f : α → F') :
+  α → F' :=
+if (measurable[m] f ∧ integrable f μ) then f else ae_measurable'_condexp_L1.mk (condexp_L1 hm μ f)
+
+localized "notation  μ `[` f `|` hm `]` := measure_theory.condexp hm μ f" in measure_theory
+
+lemma condexp_of_measurable {f : α → F'} (hf : measurable[m] f) (hfi : integrable f μ) :
+  μ[f|hm] = f :=
+by rw [condexp, if_pos (⟨hf, hfi⟩ : measurable[m] f ∧ integrable f μ)]
+
+lemma condexp_const (c : F') [is_finite_measure μ] : μ[(λ x : α, c)|hm] = λ _, c :=
+condexp_of_measurable (@measurable_const _ _ _ m _) (integrable_const c)
+
+lemma condexp_ae_eq_condexp_L1 (f : α → F') : μ[f|hm] =ᵐ[μ] condexp_L1 hm μ f :=
+begin
+  unfold condexp,
+  by_cases hfm : measurable[m] f,
+  { by_cases hfi : integrable f μ,
+    { rw if_pos (⟨hfm, hfi⟩ : measurable[m] f ∧ integrable f μ),
+      exact (condexp_L1_of_ae_measurable' (measurable.ae_measurable' hfm) hfi).symm, },
+    { simp only [hfi, if_false, and_false],
+      exact (ae_measurable'.ae_eq_mk ae_measurable'_condexp_L1).symm, }, },
+  simp only [hfm, if_false, false_and],
+  exact (ae_measurable'.ae_eq_mk ae_measurable'_condexp_L1).symm,
+end
+
+lemma condexp_ae_eq_condexp_L1_clm (hf : integrable f μ) :
+  μ[f|hm] =ᵐ[μ] condexp_L1_clm hm μ (hf.to_L1 f) :=
+begin
+  refine (condexp_ae_eq_condexp_L1 f).trans (eventually_of_forall (λ x, _)),
+  rw condexp_L1_eq hf,
+end
+
+lemma condexp_undef (hf : ¬ integrable f μ) : μ[f|hm] =ᵐ[μ] 0 :=
+begin
+  refine (condexp_ae_eq_condexp_L1 f).trans (eventually_eq.trans _ (coe_fn_zero _ 1 _)),
+  rw condexp_L1_undef hf,
+end
+
+@[simp] lemma condexp_zero : μ[(0 : α → F')|hm] = 0 :=
+condexp_of_measurable (@measurable_zero _ _ _ m _) (integrable_zero _ _ _)
+
+lemma measurable_condexp : measurable[m] (μ[f|hm]) :=
+begin
+  unfold condexp,
+  by_cases hfm : measurable[m] f,
+  { by_cases hfi : integrable f μ,
+    { rwa if_pos (⟨hfm, hfi⟩ : measurable[m] f ∧ integrable f μ), },
+    { simp only [hfi, if_false, and_false],
+      exact ae_measurable'.measurable_mk _, }, },
+  simp only [hfm, if_false, false_and],
+  exact ae_measurable'.measurable_mk _,
+end
+
+lemma integrable_condexp : integrable (μ[f|hm]) μ :=
+(integrable_condexp_L1 f).congr (condexp_ae_eq_condexp_L1 f).symm
+
+/-- The integral of the conditional expectation `μ[f|hm]` over an `m`-measurable set is equal to
+the integral of `f` on that set. -/
+lemma set_integral_condexp (hf : integrable f μ) (hs : measurable_set[m] s) :
+  ∫ x in s, μ[f|hm] x ∂μ = ∫ x in s, f x ∂μ :=
+begin
+  rw set_integral_congr_ae (hm s hs) ((condexp_ae_eq_condexp_L1 f).mono (λ x hx _, hx)),
+  exact set_integral_condexp_L1 hf hs,
+end
+
+lemma integral_condexp (hf : integrable f μ) : ∫ x, μ[f|hm] x ∂μ = ∫ x, f x ∂μ :=
+begin
+  suffices : ∫ x in set.univ, μ[f|hm] x ∂μ = ∫ x in set.univ, f x ∂μ,
+    by { simp_rw integral_univ at this, exact this, },
+  exact set_integral_condexp hf (@measurable_set.univ _ m),
+end
+
+/-- **Uniqueness of the conditional expectation**
+If a function is a.e. `m`-measurable, verifies an integrability condition and has same integral
+as `f` on all `m`-measurable sets, then it is a.e. equal to `μ[f|hm]`. -/
+lemma ae_eq_condexp_of_forall_set_integral_eq (hm : m ≤ m0) [sigma_finite (μ.trim hm)]
+  {f g : α → F'} (hf : integrable f μ)
+  (hg_int_finite : ∀ s, measurable_set[m] s → μ s < ∞ → integrable_on g s μ)
+  (hg_eq : ∀ s : set α, measurable_set[m] s → μ s < ∞ → ∫ x in s, g x ∂μ = ∫ x in s, f x ∂μ)
+  (hgm : ae_measurable' m g μ) :
+  g =ᵐ[μ] μ[f|hm] :=
+begin
+  refine ae_eq_of_forall_set_integral_eq_of_sigma_finite' hm hg_int_finite
+    (λ s hs hμs, integrable_condexp.integrable_on) (λ s hs hμs, _) hgm
+    (measurable.ae_measurable' measurable_condexp),
+  rw [hg_eq s hs hμs, set_integral_condexp hf hs],
+end
+
+lemma condexp_add (hf : integrable f μ) (hg : integrable g μ) :
+  μ[f + g | hm] =ᵐ[μ] μ[f|hm] + μ[g|hm] :=
+begin
+  refine (condexp_ae_eq_condexp_L1 _).trans _,
+  rw condexp_L1_add hf hg,
+  exact (coe_fn_add _ _).trans
+    ((condexp_ae_eq_condexp_L1 _).symm.add (condexp_ae_eq_condexp_L1 _).symm),
+end
+
+lemma condexp_smul (c : 𝕜) (f : α → F') : μ[c • f | hm] =ᵐ[μ] c • μ[f|hm] :=
+begin
+  by_cases hf : integrable f μ,
+  { refine (condexp_ae_eq_condexp_L1 _).trans _,
+    rw condexp_L1_smul c f,
+    refine (@condexp_ae_eq_condexp_L1 _ _ _ _ _ _ _ _ m _ _ hm _ f).mp _,
+    refine (coe_fn_smul c (condexp_L1 hm μ f)).mono (λ x hx1 hx2, _),
+    rw [hx1, pi.smul_apply, pi.smul_apply, hx2], },
+  { by_cases hc : c = 0,
+    { rw [hc, zero_smul, zero_smul, condexp_zero], },
+    refine (condexp_undef (mt (integrable_smul_iff hc f).mp hf)).trans _,
+    refine (@condexp_undef _ _ _ _ _ _ _ _ _ _ _ hm _ _ hf).mono (λ x hx, _),
+    rw [pi.zero_apply, pi.smul_apply, hx, pi.zero_apply, smul_zero], },
+end
+
+lemma condexp_neg (f : α → F') : μ[-f|hm] =ᵐ[μ] - μ[f|hm] :=
+by letI : module ℝ (α → F') := @pi.module α (λ _, F') ℝ _ _ (λ _, infer_instance);
+calc μ[-f|hm] = μ[(-1 : ℝ) • f|hm] : by rw neg_one_smul ℝ f
+... =ᵐ[μ] (-1 : ℝ) • μ[f|hm] : condexp_smul (-1) f
+... = -μ[f|hm] : neg_one_smul ℝ (μ[f|hm])
+
+lemma condexp_sub (hf : integrable f μ) (hg : integrable g μ) :
+  μ[f - g | hm] =ᵐ[μ] μ[f|hm] - μ[g|hm] :=
+begin
+  simp_rw sub_eq_add_neg,
+  exact (condexp_add hf hg.neg).trans (eventually_eq.rfl.add (condexp_neg g)),
+end
+
+end condexp
+
 end measure_theory
diff --git a/src/measure_theory/integral/set_integral.lean b/src/measure_theory/integral/set_integral.lean
index ca83e86ed53fc..440a5e067e39c 100644
--- a/src/measure_theory/integral/set_integral.lean
+++ b/src/measure_theory/integral/set_integral.lean
@@ -283,6 +283,21 @@ lemma integral_indicator_const (e : E) ⦃s : set α⦄ (s_meas : measurable_set
   ∫ (a : α), s.indicator (λ (x : α), e) a ∂μ = (μ s).to_real • e :=
 by rw [integral_indicator s_meas, ← set_integral_const]
 
+lemma set_integral_indicator_const_Lp {p : ℝ≥0∞} (hs : measurable_set s) (ht : measurable_set t)
+  (hμt : μ t ≠ ∞) (x : E) :
+  ∫ a in s, indicator_const_Lp p ht hμt x a ∂μ = (μ (t ∩ s)).to_real • x :=
+calc ∫ a in s, indicator_const_Lp p ht hμt x a ∂μ
+    = (∫ a in s, t.indicator (λ _, x) a ∂μ) :
+  by rw set_integral_congr_ae hs (indicator_const_Lp_coe_fn.mono (λ x hx hxs, hx))
+... = (μ (t ∩ s)).to_real • x : by rw [integral_indicator_const _ ht, measure.restrict_apply ht]
+
+lemma integral_indicator_const_Lp {p : ℝ≥0∞} (ht : measurable_set t) (hμt : μ t ≠ ∞) (x : E) :
+  ∫ a, indicator_const_Lp p ht hμt x a ∂μ = (μ t).to_real • x :=
+calc ∫ a, indicator_const_Lp p ht hμt x a ∂μ
+    = ∫ a in univ, indicator_const_Lp p ht hμt x a ∂μ : by rw integral_univ
+... = (μ (t ∩ univ)).to_real • x : set_integral_indicator_const_Lp measurable_set.univ ht hμt x
+... = (μ t).to_real • x : by rw inter_univ
+
 lemma set_integral_map {β} [measurable_space β] {g : α → β} {f : β → E} {s : set β}
   (hs : measurable_set s) (hf : ae_measurable f (measure.map g μ)) (hg : measurable g) :
   ∫ y in s, f y ∂(measure.map g μ) = ∫ x in g ⁻¹' s, f (g x) ∂μ :=