chore(measure_theory/function/conditional_expectation): change the de…

…finition of `condexp` (#16325)

Change the definition of `condexp` slightly to have `μ[f|m] = 0` when `f` is not integrable, instead of `μ[f|m] =ᵐ[μ] 0`.

src/measure_theory/function/conditional_expectation/basic.lean

@@ -1827,9 +1827,12 @@ 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 :=
+@[simp] lemma condexp_L1_zero : condexp_L1 hm μ (0 : α → F') = 0 :=
 set_to_fun_zero _
 
+@[simp] lemma condexp_L1_measure_zero (hm : m ≤ m0) : condexp_L1 hm (0 : measure α) f = 0 :=
+set_to_fun_measure_zero _ rfl
+
 lemma ae_strongly_measurable'_condexp_L1 {f : α → F'} :
   ae_strongly_measurable' m (condexp_L1 hm μ f) μ :=
 begin
@@ -1904,17 +1907,20 @@ open_locale classical
 
 variables {𝕜} {m m0 : measurable_space α} {μ : measure α} {f g : α → F'} {s : set α}
 
-/-- Conditional expectation of a function. Its value is 0 if the function is not integrable, if
-the σ-algebra is not a sub-σ-algebra or if the measure is not σ-finite on that σ-algebra. -/
+/-- Conditional expectation of a function. It is defined as 0 if any one of the following conditions
+is true:
+- `m` is not a sub-σ-algebra of `m0`,
+- `μ` is not σ-finite with respect to `m`,
+- `f` is not integrable. -/
 @[irreducible]
 def condexp (m : measurable_space α) {m0 : measurable_space α} (μ : measure α) (f : α → F') :
   α → F' :=
 if hm : m ≤ m0
-  then if hμ : sigma_finite (μ.trim hm)
-    then if (strongly_measurable[m] f ∧ integrable f μ)
+  then if h : sigma_finite (μ.trim hm) ∧ integrable f μ
+    then if strongly_measurable[m] f
       then f
-      else (@ae_strongly_measurable'_condexp_L1 _ _ _ _ _ m m0 μ hm hμ _).mk
-        (@condexp_L1 _ _ _ _ _ _ _ hm μ hμ f)
+      else (@ae_strongly_measurable'_condexp_L1 _ _ _ _ _ m m0 μ hm h.1 _).mk
+        (@condexp_L1 _ _ _ _ _ _ _ hm μ h.1 f)
     else 0
   else 0
 
@@ -1926,19 +1932,26 @@ lemma condexp_of_not_le (hm_not : ¬ m ≤ m0) : μ[f|m] = 0 := by rw [condexp,
 
 lemma condexp_of_not_sigma_finite (hm : m ≤ m0) (hμm_not : ¬ sigma_finite (μ.trim hm)) :
   μ[f|m] = 0 :=
-by rw [condexp, dif_pos hm, dif_neg hμm_not]
+by { rw [condexp, dif_pos hm, dif_neg], push_neg, exact λ h, absurd h hμm_not, }
 
 lemma condexp_of_sigma_finite (hm : m ≤ m0) [hμm : sigma_finite (μ.trim hm)] :
   μ[f|m] =
-  if (strongly_measurable[m] f ∧ integrable f μ)
-    then f else ae_strongly_measurable'_condexp_L1.mk (condexp_L1 hm μ f) :=
-by rw [condexp, dif_pos hm, dif_pos hμm]
+  if integrable f μ
+    then if strongly_measurable[m] f
+      then f else ae_strongly_measurable'_condexp_L1.mk (condexp_L1 hm μ f)
+    else 0 :=
+begin
+  rw [condexp, dif_pos hm],
+  simp only [hμm, ne.def, true_and],
+  by_cases hf : integrable f μ,
+  { rw [dif_pos hf, if_pos hf], },
+  { rw [dif_neg hf, if_neg hf], },
+end
 
 lemma condexp_of_strongly_measurable (hm : m ≤ m0) [hμm : sigma_finite (μ.trim hm)]
   {f : α → F'} (hf : strongly_measurable[m] f) (hfi : integrable f μ) :
   μ[f|m] = f :=
-by { rw [condexp_of_sigma_finite hm,
-  if_pos (⟨hf, hfi⟩ : strongly_measurable[m] f ∧ integrable f μ)], apply_instance,  }
+by { rw [condexp_of_sigma_finite hm, if_pos hfi, if_pos hf], apply_instance, }
 
 lemma condexp_const (hm : m ≤ m0) (c : F') [is_finite_measure μ] : μ[(λ x : α, c)|m] = λ _, c :=
 condexp_of_strongly_measurable hm (@strongly_measurable_const _ _ m _ _) (integrable_const c)
@@ -1947,15 +1960,16 @@ lemma condexp_ae_eq_condexp_L1 (hm : m ≤ m0) [hμm : sigma_finite (μ.trim hm)
   (f : α → F') : μ[f|m] =ᵐ[μ] condexp_L1 hm μ f :=
 begin
   rw condexp_of_sigma_finite hm,
-  by_cases hfm : strongly_measurable[m] f,
-  { by_cases hfi : integrable f μ,
-    { rw if_pos (⟨hfm, hfi⟩ : strongly_measurable[m] f ∧ integrable f μ),
+  by_cases hfi : integrable f μ,
+  { rw if_pos hfi,
+    by_cases hfm : strongly_measurable[m] f,
+    { rw if_pos hfm,
       exact (condexp_L1_of_ae_strongly_measurable'
         (strongly_measurable.ae_strongly_measurable' hfm) hfi).symm, },
-    { simp only [hfi, if_false, and_false],
+    { rw if_neg hfm,
       exact (ae_strongly_measurable'.ae_eq_mk ae_strongly_measurable'_condexp_L1).symm, }, },
-  simp only [hfm, if_false, false_and],
-  exact (ae_strongly_measurable'.ae_eq_mk ae_strongly_measurable'_condexp_L1).symm,
+  rw [if_neg hfi, condexp_L1_undef hfi],
+  exact (coe_fn_zero _ _ _).symm,
 end
 
 lemma condexp_ae_eq_condexp_L1_clm (hm : m ≤ m0) [sigma_finite (μ.trim hm)] (hf : integrable f μ) :
@@ -1965,15 +1979,14 @@ begin
   rw condexp_L1_eq hf,
 end
 
-lemma condexp_undef (hf : ¬ integrable f μ) : μ[f|m] =ᵐ[μ] 0 :=
+lemma condexp_undef (hf : ¬ integrable f μ) : μ[f|m] = 0 :=
 begin
   by_cases hm : m ≤ m0,
   swap, { rw condexp_of_not_le hm, },
   by_cases hμm : sigma_finite (μ.trim hm),
   swap, { rw condexp_of_not_sigma_finite hm hμm, },
   haveI : sigma_finite (μ.trim hm) := hμm,
-  refine (condexp_ae_eq_condexp_L1 hm f).trans (eventually_eq.trans _ (coe_fn_zero _ 1 _)),
-  rw condexp_L1_undef hf,
+  rw [condexp_of_sigma_finite, if_neg hf],
 end
 
 @[simp] lemma condexp_zero : μ[(0 : α → F')|m] = 0 :=
@@ -1996,13 +2009,10 @@ begin
   haveI : sigma_finite (μ.trim hm) := hμm,
   rw condexp_of_sigma_finite hm,
   swap, { apply_instance, },
-  by_cases hfm : strongly_measurable[m] f,
-  { by_cases hfi : integrable f μ,
-    { rwa if_pos (⟨hfm, hfi⟩ : strongly_measurable[m] f ∧ integrable f μ), },
-    { simp only [hfi, if_false, and_false],
-      exact ae_strongly_measurable'.strongly_measurable_mk _, }, },
-  simp only [hfm, if_false, false_and],
-  exact ae_strongly_measurable'.strongly_measurable_mk _,
+  split_ifs with hfi hfm,
+  { exact hfm, },
+  { exact ae_strongly_measurable'.strongly_measurable_mk _, },
+  { exact strongly_measurable_zero, },
 end
 
 lemma condexp_congr_ae (h : f =ᵐ[μ] g) : μ[f | m] =ᵐ[μ] μ[g | m] :=
@@ -2130,16 +2140,16 @@ begin
   by_cases hμm₁ : sigma_finite (μ.trim (hm₁₂.trans hm₂)),
   swap, { simp_rw condexp_of_not_sigma_finite (hm₁₂.trans hm₂) hμm₁, },
   haveI : sigma_finite (μ.trim (hm₁₂.trans hm₂)) := hμm₁,
+  by_cases hf : integrable f μ,
+  swap, { simp_rw [condexp_undef hf, condexp_zero], },
   refine ae_eq_of_forall_set_integral_eq_of_sigma_finite' (hm₁₂.trans hm₂)
     (λ s hs hμs, integrable_condexp.integrable_on) (λ s hs hμs, integrable_condexp.integrable_on)
     _ (strongly_measurable.ae_strongly_measurable' strongly_measurable_condexp)
       (strongly_measurable.ae_strongly_measurable' strongly_measurable_condexp),
   intros s hs hμs,
   rw set_integral_condexp (hm₁₂.trans hm₂) integrable_condexp hs,
   swap, { apply_instance, },
-  by_cases hf : integrable f μ,
-  { rw [set_integral_condexp (hm₁₂.trans hm₂) hf hs, set_integral_condexp hm₂ hf (hm₁₂ s hs)], },
-  { simp_rw integral_congr_ae (ae_restrict_of_ae (condexp_undef hf)), },
+  rw [set_integral_condexp (hm₁₂.trans hm₂) hf hs, set_integral_condexp hm₂ hf (hm₁₂ s hs)],
 end
 
 lemma condexp_mono {E} [normed_lattice_add_comm_group E] [complete_space E] [normed_space ℝ E]
@@ -2162,7 +2172,7 @@ begin
   by_cases hfint : integrable f μ,
   { rw (condexp_zero.symm : (0 : α → E) = μ[0 | m]),
     exact condexp_mono (integrable_zero _ _ _) hfint hf },
-  { exact eventually_eq.le (condexp_undef hfint).symm }
+  { rw condexp_undef hfint, }
 end
 
 lemma condexp_nonpos {E} [normed_lattice_add_comm_group E] [complete_space E] [normed_space ℝ E]
@@ -2172,7 +2182,7 @@ begin
   by_cases hfint : integrable f μ,
   { rw (condexp_zero.symm : (0 : α → E) = μ[0 | m]),
     exact condexp_mono hfint (integrable_zero _ _ _) hf },
-  { exact eventually_eq.le (condexp_undef hfint) }
+  { rw condexp_undef hfint, }
 end
 
 /-- **Lebesgue dominated convergence theorem**: sufficient conditions under which almost

src/measure_theory/function/conditional_expectation/indicator.lean

@@ -44,7 +44,7 @@ begin
   { rw ← restrict_trim hm _ hs,
     exact restrict.sigma_finite _ s, },
   by_cases hf_int : integrable f μ,
-  swap, { exact ae_restrict_of_ae (condexp_undef hf_int), },
+  swap, { rw condexp_undef hf_int, },
   refine ae_eq_of_forall_set_integral_eq_of_sigma_finite' hm _ _ _ _ _,
   { exact λ t ht hμt, integrable_condexp.integrable_on.integrable_on, },
   { exact λ t ht hμt, (integrable_zero _ _ _).integrable_on, },
@@ -159,11 +159,7 @@ begin
   have hs_m₂ : measurable_set[m₂] s,
   { rwa [← set.inter_univ s, ← hs set.univ, set.inter_univ], },
   by_cases hf_int : integrable f μ,
-  swap,
-  { filter_upwards [@condexp_undef _ _ _ _ _ m _ μ _ hf_int,
-      @condexp_undef _ _ _ _ _ m₂ _ μ _ hf_int] with x hxm hxm₂,
-    rw pi.zero_apply at hxm hxm₂,
-    rw [set.indicator_apply_eq_zero.2 (λ _, hxm), set.indicator_apply_eq_zero.2 (λ _, hxm₂)] },
+  swap, { simp_rw condexp_undef hf_int, },
   refine ((condexp_indicator hf_int hs_m).symm.trans _).trans (condexp_indicator hf_int hs_m₂),
   refine ae_eq_of_forall_set_integral_eq_of_sigma_finite' hm₂
     (λ s hs hμs, integrable_condexp.integrable_on)

src/measure_theory/function/conditional_expectation/real.lean

@@ -56,7 +56,7 @@ lemma snorm_one_condexp_le_snorm (f : α → ℝ) :
   snorm (μ[f | m]) 1 μ ≤ snorm f 1 μ :=
 begin
   by_cases hf : integrable f μ,
-  swap, { rw [snorm_congr_ae (condexp_undef hf), snorm_zero], exact zero_le _ },
+  swap, { rw [condexp_undef hf, snorm_zero], exact zero_le _ },
   by_cases hm : m ≤ m0,
   swap, { rw [condexp_of_not_le hm, snorm_zero], exact zero_le _ },
   by_cases hsig : sigma_finite (μ.trim hm),

src/probability/conditional_expectation.lean

@@ -38,7 +38,7 @@ lemma condexp_indep_eq
   μ[f | m₂] =ᵐ[μ] λ x, μ[f] :=
 begin
   by_cases hfint : integrable f μ,
-  swap, { exact (integral_undef hfint).symm ▸ condexp_undef hfint },
+  swap, { rw [condexp_undef hfint, integral_undef hfint], refl, },
   have hfint₁ := hfint.trim hle₁ hf,
   refine (ae_eq_condexp_of_forall_set_integral_eq hle₂ hfint
     (λ s _ hs, integrable_on_const.2 (or.inr hs)) (λ s hms hs, _)