feat(measure_theory/function/conditional_expectation): conditional ex…

…pectation with respect to the bot sigma algebra (#16342)

Prove that for a probability measure, `μ[f|⊥] = λ _, ∫ x, f x ∂μ`.



Co-authored-by: RemyDegenne <remydegenne@gmail.com>

src/measure_theory/function/conditional_expectation/basic.lean

@@ -2056,7 +2056,7 @@ begin
   exact set_integral_condexp_L1 hf hs,
 end
 
-lemma integral_condexp {hm : m ≤ m0} [hμm : sigma_finite (μ.trim hm)]
+lemma integral_condexp (hm : m ≤ m0) [hμm : sigma_finite (μ.trim hm)]
   (hf : integrable f μ) : ∫ x, μ[f|m] x ∂μ = ∫ x, f x ∂μ :=
 begin
   suffices : ∫ x in set.univ, μ[f|m] x ∂μ = ∫ x in set.univ, f x ∂μ,
@@ -2080,6 +2080,46 @@ begin
   rw [hg_eq s hs hμs, set_integral_condexp hm hf hs],
 end
 
+lemma condexp_bot' [hμ : μ.ae.ne_bot] (f : α → F') :
+  μ[f|⊥] = λ _, (μ set.univ).to_real⁻¹ • ∫ x, f x ∂μ :=
+begin
+  by_cases hμ_finite : is_finite_measure μ,
+  swap,
+  { have h : ¬ sigma_finite (μ.trim bot_le),
+    { rwa sigma_finite_trim_bot_iff, },
+    rw not_is_finite_measure_iff at hμ_finite,
+    rw [condexp_of_not_sigma_finite bot_le h],
+    simp only [hμ_finite, ennreal.top_to_real, inv_zero, zero_smul],
+    refl, },
+  haveI : is_finite_measure μ := hμ_finite,
+  by_cases hf : integrable f μ,
+  swap, { rw [integral_undef hf, smul_zero, condexp_undef hf], refl, },
+  have h_meas : strongly_measurable[⊥] (μ[f|⊥]) := strongly_measurable_condexp,
+  obtain ⟨c, h_eq⟩ := strongly_measurable_bot_iff.mp h_meas,
+  rw h_eq,
+  have h_integral : ∫ x, μ[f|⊥] x ∂μ = ∫ x, f x ∂μ := integral_condexp bot_le hf,
+  simp_rw [h_eq, integral_const] at h_integral,
+  rw [← h_integral, ← smul_assoc, smul_eq_mul, inv_mul_cancel, one_smul],
+  rw [ne.def, ennreal.to_real_eq_zero_iff, auto.not_or_eq, measure.measure_univ_eq_zero,
+    ← ae_eq_bot, ← ne.def, ← ne_bot_iff],
+  exact ⟨hμ, measure_ne_top μ set.univ⟩,
+end
+
+lemma condexp_bot_ae_eq (f : α → F') :
+  μ[f|⊥] =ᵐ[μ] λ _, (μ set.univ).to_real⁻¹ • ∫ x, f x ∂μ :=
+begin
+  by_cases μ.ae.ne_bot,
+  { refine eventually_of_forall (λ x, _),
+    rw condexp_bot' f,
+    exact h, },
+  { rw [ne_bot_iff, not_not, ae_eq_bot] at h,
+    simp only [h, ae_zero], },
+end
+
+lemma condexp_bot [is_probability_measure μ] (f : α → F') :
+  μ[f|⊥] = λ _, ∫ x, f x ∂μ :=
+by { refine (condexp_bot' f).trans _, rw [measure_univ, ennreal.one_to_real, inv_one, one_smul], }
+
 lemma condexp_add (hf : integrable f μ) (hg : integrable g μ) :
   μ[f + g | m] =ᵐ[μ] μ[f|m] + μ[g|m] :=
 begin

src/measure_theory/function/strongly_measurable.lean

@@ -250,6 +250,26 @@ begin
     { rwa div_le_one (lt_of_le_of_ne (norm_nonneg _) (ne.symm h0)), }, },
 end
 
+lemma _root_.strongly_measurable_bot_iff [nonempty β] [t2_space β] :
+  strongly_measurable[⊥] f ↔ ∃ c, f = λ _, c :=
+begin
+  casesI is_empty_or_nonempty α with hα hα,
+  { simp only [subsingleton.strongly_measurable', eq_iff_true_of_subsingleton, exists_const], },
+  refine ⟨λ hf, _, λ hf_eq, _⟩,
+  { refine ⟨f hα.some, _⟩,
+    let fs := hf.approx,
+    have h_fs_tendsto : ∀ x, tendsto (λ n, fs n x) at_top (𝓝 (f x)) := hf.tendsto_approx,
+    have : ∀ n, ∃ c, ∀ x, fs n x = c := λ n, simple_func.simple_func_bot (fs n),
+    let cs := λ n, (this n).some,
+    have h_cs_eq : ∀ n, ⇑(fs n) = (λ x, cs n) := λ n, funext (this n).some_spec,
+    simp_rw h_cs_eq at h_fs_tendsto,
+    have h_tendsto : tendsto cs at_top (𝓝 (f hα.some)) := h_fs_tendsto hα.some,
+    ext1 x,
+    exact tendsto_nhds_unique (h_fs_tendsto x) h_tendsto, },
+  { obtain ⟨c, rfl⟩ := hf_eq,
+    exact strongly_measurable_const, },
+end
+
 end basic_properties_in_any_topological_space
 
 lemma fin_strongly_measurable_of_set_sigma_finite [topological_space β] [has_zero β]

src/measure_theory/integral/lebesgue.lean

@@ -126,6 +126,33 @@ lemma range_const_subset (α) [measurable_space α] (b : β) :
   (const α b).range ⊆ {b} :=
 finset.coe_subset.1 $ by simp
 
+lemma simple_func_bot {α} (f : @simple_func α ⊥ β) [nonempty β] : ∃ c, ∀ x, f x = c :=
+begin
+  have hf_meas := @simple_func.measurable_set_fiber α _ ⊥ f,
+  simp_rw measurable_space.measurable_set_bot_iff at hf_meas,
+  casesI is_empty_or_nonempty α,
+  { simp only [is_empty.forall_iff, exists_const], },
+  { specialize hf_meas (f h.some),
+    cases hf_meas,
+    { exfalso,
+      refine set.not_mem_empty h.some _,
+      rw [← hf_meas, set.mem_preimage],
+      exact set.mem_singleton _, },
+    { refine ⟨f h.some, λ x, _⟩,
+      have : x ∈ f ⁻¹' {f h.some},
+      { rw hf_meas, exact set.mem_univ x, },
+      rwa [set.mem_preimage, set.mem_singleton_iff] at this, }, },
+end
+
+lemma simple_func_bot' {α} [nonempty β] (f : @simple_func α ⊥ β) :
+  ∃ c, f = @simple_func.const α _ ⊥ c :=
+begin
+  obtain ⟨c, h_eq⟩ := simple_func_bot f,
+  refine ⟨c, _⟩,
+  ext1 x,
+  rw [h_eq x, simple_func.coe_const],
+end
+
 lemma measurable_set_cut (r : α → β → Prop) (f : α →ₛ β)
   (h : ∀b, measurable_set {a | r a b}) : measurable_set {a | r a (f a)} :=
 begin

src/measure_theory/measure/measure_space.lean

@@ -2219,6 +2219,13 @@ include m0
 /-- A measure `μ` is called finite if `μ univ < ∞`. -/
 class is_finite_measure (μ : measure α) : Prop := (measure_univ_lt_top : μ univ < ∞)
 
+lemma not_is_finite_measure_iff : ¬ is_finite_measure μ ↔ μ set.univ = ∞ :=
+begin
+  refine ⟨λ h, _, λ h, λ h', h'.measure_univ_lt_top.ne h⟩,
+  by_contra h',
+  exact h ⟨lt_top_iff_ne_top.mpr h'⟩,
+end
+
 instance restrict.is_finite_measure (μ : measure α) [hs : fact (μ s < ∞)] :
   is_finite_measure (μ.restrict s) :=
 ⟨by simp [hs.elim]⟩
@@ -2753,14 +2760,35 @@ lemma sigma_finite_of_le (μ : measure α) [hs : sigma_finite μ]
 
 end measure
 
-include m0
-
 /-- Every finite measure is σ-finite. -/
 @[priority 100]
-instance is_finite_measure.to_sigma_finite (μ : measure α) [is_finite_measure μ] :
+instance is_finite_measure.to_sigma_finite {m0 : measurable_space α} (μ : measure α)
+  [is_finite_measure μ] :
   sigma_finite μ :=
 ⟨⟨⟨λ _, univ, λ _, trivial, λ _, measure_lt_top μ _, Union_const _⟩⟩⟩
 
+lemma sigma_finite_bot_iff (μ : @measure α ⊥) : sigma_finite μ ↔ is_finite_measure μ :=
+begin
+  refine ⟨λ h, ⟨_⟩, λ h, by { haveI := h, apply_instance, }⟩,
+  haveI : sigma_finite μ := h,
+  let s := spanning_sets μ,
+  have hs_univ : (⋃ i, s i) = set.univ := Union_spanning_sets μ,
+  have hs_meas : ∀ i, measurable_set[⊥] (s i) := measurable_spanning_sets μ,
+  simp_rw measurable_space.measurable_set_bot_iff at hs_meas,
+  by_cases h_univ_empty : set.univ = ∅,
+  { rw [h_univ_empty, measure_empty], exact ennreal.zero_ne_top.lt_top, },
+  obtain ⟨i, hsi⟩ : ∃ i, s i = set.univ,
+  { by_contra h_not_univ,
+    push_neg at h_not_univ,
+    have h_empty : ∀ i, s i = ∅, by simpa [h_not_univ] using hs_meas,
+    simp [h_empty] at hs_univ,
+    exact h_univ_empty hs_univ.symm, },
+  rw ← hsi,
+  exact measure_spanning_sets_lt_top μ i,
+end
+
+include m0
+
 instance restrict.sigma_finite (μ : measure α) [sigma_finite μ] (s : set α) :
   sigma_finite (μ.restrict s) :=
 begin
@@ -3314,6 +3342,14 @@ begin
     ... < ∞ : measure_spanning_sets_lt_top _ _, },
 end
 
+lemma sigma_finite_trim_bot_iff : sigma_finite (μ.trim bot_le) ↔ is_finite_measure μ :=
+begin
+  rw sigma_finite_bot_iff,
+  refine ⟨λ h, ⟨_⟩, λ h, ⟨_⟩⟩; have h_univ := h.measure_univ_lt_top,
+  { rwa trim_measurable_set_eq bot_le measurable_set.univ at h_univ, },
+  { rwa trim_measurable_set_eq bot_le measurable_set.univ, },
+end
+
 end trim
 
 end measure_theory