feat(measure_theory/function/uniform_integrable): conditional expectations form a uniformly integrable class (#15378)

Useful for the L1 martingale convergence theorem.



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

Author: kex-y

src/measure_theory/function/conditional_expectation.lean

@@ -7,6 +7,7 @@ Authors: Rémy Degenne
 import analysis.inner_product_space.projection
 import measure_theory.function.l2_space
 import measure_theory.decomposition.radon_nikodym
+import measure_theory.function.uniform_integrable
 
 /-! # Conditional expectation
 
@@ -68,6 +69,9 @@ However, some lemmas also use `𝕜 : is_R_or_C`:
 * results about scalar multiplication are stated not only for `ℝ` but also for `𝕜` if we happen to
   have `normed_space 𝕜 F`.
 
+TODO: split this file in two with one containing constructions and the other with basic
+properties.
+
 ## Tags
 
 conditional expectation, conditional expected value
@@ -2145,29 +2149,6 @@ begin
     ((condexp_L1_mono hf hg hfg).trans_eq (condexp_ae_eq_condexp_L1 hm _).symm),
 end
 
-section real
-
-lemma rn_deriv_ae_eq_condexp {hm : m ≤ m0} [hμm : sigma_finite (μ.trim hm)] {f : α → ℝ}
-  (hf : integrable f μ) :
-  signed_measure.rn_deriv ((μ.with_densityᵥ f).trim hm) (μ.trim hm) =ᵐ[μ] μ[f | m] :=
-begin
-  refine ae_eq_condexp_of_forall_set_integral_eq hm hf _ _ _,
-  { exact λ _ _ _, (integrable_of_integrable_trim hm (signed_measure.integrable_rn_deriv
-      ((μ.with_densityᵥ f).trim hm) (μ.trim hm))).integrable_on },
-  { intros s hs hlt,
-    conv_rhs { rw [← hf.with_densityᵥ_trim_eq_integral hm hs,
-      ← signed_measure.with_densityᵥ_rn_deriv_eq ((μ.with_densityᵥ f).trim hm) (μ.trim hm)
-        (hf.with_densityᵥ_trim_absolutely_continuous hm)], },
-    rw [with_densityᵥ_apply
-        (signed_measure.integrable_rn_deriv ((μ.with_densityᵥ f).trim hm) (μ.trim hm)) hs,
-      ← set_integral_trim hm _ hs],
-    exact (signed_measure.measurable_rn_deriv _ _).strongly_measurable },
-  { exact strongly_measurable.ae_strongly_measurable'
-      (signed_measure.measurable_rn_deriv _ _).strongly_measurable },
-end
-
-end real
-
 section indicator
 
 lemma condexp_ae_eq_restrict_zero (hs : measurable_set[m] s) (hf : f =ᵐ[μ.restrict s] 0) :
@@ -2336,6 +2317,115 @@ end
 
 end indicator
 
+section real
+
+lemma rn_deriv_ae_eq_condexp {hm : m ≤ m0} [hμm : sigma_finite (μ.trim hm)] {f : α → ℝ}
+  (hf : integrable f μ) :
+  signed_measure.rn_deriv ((μ.with_densityᵥ f).trim hm) (μ.trim hm) =ᵐ[μ] μ[f | m] :=
+begin
+  refine ae_eq_condexp_of_forall_set_integral_eq hm hf _ _ _,
+  { exact λ _ _ _, (integrable_of_integrable_trim hm (signed_measure.integrable_rn_deriv
+      ((μ.with_densityᵥ f).trim hm) (μ.trim hm))).integrable_on },
+  { intros s hs hlt,
+    conv_rhs { rw [← hf.with_densityᵥ_trim_eq_integral hm hs,
+      ← signed_measure.with_densityᵥ_rn_deriv_eq ((μ.with_densityᵥ f).trim hm) (μ.trim hm)
+        (hf.with_densityᵥ_trim_absolutely_continuous hm)], },
+    rw [with_densityᵥ_apply
+        (signed_measure.integrable_rn_deriv ((μ.with_densityᵥ f).trim hm) (μ.trim hm)) hs,
+      ← set_integral_trim hm _ hs],
+    exact (signed_measure.measurable_rn_deriv _ _).strongly_measurable },
+  { exact strongly_measurable.ae_strongly_measurable'
+      (signed_measure.measurable_rn_deriv _ _).strongly_measurable },
+end
+
+/-- TODO: this should be generalized and proved using Jensen's inequality
+for the conditional expectation (not in mathlib yet) .-/
+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 _ },
+  by_cases hm : m ≤ m0,
+  swap, { rw [condexp_of_not_le hm, snorm_zero], exact zero_le _ },
+  by_cases hsig : sigma_finite (μ.trim hm),
+  swap, { rw [condexp_of_not_sigma_finite hm hsig, snorm_zero], exact zero_le _ },
+  calc snorm (μ[f | m]) 1 μ ≤ snorm (μ[|f| | m]) 1 μ :
+  begin
+    refine snorm_mono_ae _,
+    filter_upwards [@condexp_mono _ m m0 _ _ _ _ _ _ _ _ hf hf.abs
+        (@ae_of_all _ m0 _ μ (λ x, le_abs_self (f x) : ∀ x, f x ≤ |f x|)),
+      eventually_le.trans (condexp_neg f).symm.le
+        (@condexp_mono _ m m0 _ _ _ _ _ _ _  _ hf.neg hf.abs
+        (@ae_of_all _ m0 _ μ (λ x, neg_le_abs_self (f x) : ∀ x, -f x ≤ |f x|)))] with x hx₁ hx₂,
+    exact abs_le_abs hx₁ hx₂,
+  end
+    ... = snorm f 1 μ :
+  begin
+    rw [snorm_one_eq_lintegral_nnnorm, snorm_one_eq_lintegral_nnnorm,
+      ← ennreal.to_real_eq_to_real (ne_of_lt integrable_condexp.2) (ne_of_lt hf.2),
+      ← integral_norm_eq_lintegral_nnnorm
+        (strongly_measurable_condexp.mono hm).ae_strongly_measurable,
+      ← integral_norm_eq_lintegral_nnnorm hf.1],
+    simp_rw [real.norm_eq_abs],
+    rw ← @integral_condexp _ _ _ _ _ m m0 μ _ hm hsig hf.abs,
+    refine integral_congr_ae _,
+    have : 0 ≤ᵐ[μ] μ[|f| | m],
+    { rw ← @condexp_zero α ℝ _ _ _ m m0 μ,
+      exact condexp_mono (integrable_zero _ _ _) hf.abs
+        (@ae_of_all _ m0 _ μ (λ x, abs_nonneg (f x) : ∀ x, 0 ≤ |f x|)) },
+    filter_upwards [this] with x hx,
+    exact abs_eq_self.2 hx
+  end
+end
+
+/-- Given a integrable function `g`, the conditional expectations of `g` with respect to
+a sequence of sub-σ-algebras is uniformly integrable. -/
+lemma integrable.uniform_integrable_condexp {ι : Type*} [is_finite_measure μ]
+  {g : α → ℝ} (hint : integrable g μ) {ℱ : ι → measurable_space α} (hℱ : ∀ i, ℱ i ≤ m0) :
+  uniform_integrable (λ i, μ[g | ℱ i]) 1 μ :=
+begin
+  have hmeas : ∀ n, ∀ C, measurable_set {x | C ≤ ∥μ[g | ℱ n] x∥₊} :=
+    λ n C, measurable_set_le measurable_const
+      (strongly_measurable_condexp.mono (hℱ n)).measurable.nnnorm,
+  have hg : mem_ℒp g 1 μ := mem_ℒp_one_iff_integrable.2 hint,
+  refine uniform_integrable_of le_rfl ennreal.one_ne_top
+    (λ n, strongly_measurable_condexp.mono (hℱ n)) (λ ε hε, _),
+  by_cases hne : snorm g 1 μ = 0,
+  { rw snorm_eq_zero_iff hg.1 one_ne_zero at hne,
+    refine ⟨0, λ n, (le_of_eq $ (snorm_eq_zero_iff
+      ((strongly_measurable_condexp.mono (hℱ n)).ae_strongly_measurable.indicator (hmeas n 0))
+      one_ne_zero).2 _).trans (zero_le _)⟩,
+    filter_upwards [@condexp_congr_ae _ _ _ _ _ (ℱ n) m0 μ _ _ hne] with x hx,
+    simp only [zero_le', set.set_of_true, set.indicator_univ, pi.zero_apply, hx, condexp_zero] },
+  obtain ⟨δ, hδ, h⟩ := hg.snorm_indicator_le μ le_rfl ennreal.one_ne_top hε,
+  set C : ℝ≥0 := ⟨δ, hδ.le⟩⁻¹ * (snorm g 1 μ).to_nnreal with hC,
+  have hCpos : 0 < C :=
+    mul_pos (nnreal.inv_pos.2 hδ) (ennreal.to_nnreal_pos hne hg.snorm_lt_top.ne),
+  have : ∀ n, μ {x : α | C ≤ ∥μ[g | ℱ n] x∥₊} ≤ ennreal.of_real δ,
+  { intro n,
+    have := mul_meas_ge_le_pow_snorm' μ one_ne_zero ennreal.one_ne_top
+      ((@strongly_measurable_condexp _ _ _ _ _ (ℱ n) _ μ g).mono
+        (hℱ n)).ae_strongly_measurable C,
+    rw [ennreal.one_to_real, ennreal.rpow_one, ennreal.rpow_one, mul_comm,
+      ← ennreal.le_div_iff_mul_le (or.inl (ennreal.coe_ne_zero.2 hCpos.ne.symm))
+        (or.inl ennreal.coe_lt_top.ne)] at this,
+    simp_rw [ennreal.coe_le_coe] at this,
+    refine this.trans _,
+    rw [ennreal.div_le_iff_le_mul (or.inl (ennreal.coe_ne_zero.2 hCpos.ne.symm))
+        (or.inl ennreal.coe_lt_top.ne), hC, nonneg.inv_mk, ennreal.coe_mul,
+      ennreal.coe_to_nnreal hg.snorm_lt_top.ne, ← mul_assoc, ← ennreal.of_real_eq_coe_nnreal,
+      ← ennreal.of_real_mul hδ.le, mul_inv_cancel hδ.ne.symm, ennreal.of_real_one, one_mul],
+    exact snorm_one_condexp_le_snorm _ },
+  refine ⟨C, λ n, le_trans _ (h {x : α | C ≤ ∥μ[g | ℱ n] x∥₊} (hmeas n C) (this n))⟩,
+  have hmeasℱ : measurable_set[ℱ n] {x : α | C ≤ ∥μ[g | ℱ n] x∥₊} :=
+    @measurable_set_le _ _ _ _ _ (ℱ n) _ _ _ _ _ measurable_const
+      (@measurable.nnnorm _ _ _ _ _ (ℱ n) _ strongly_measurable_condexp.measurable),
+  rw ← snorm_congr_ae (condexp_indicator hint hmeasℱ),
+  exact snorm_one_condexp_le_snorm _,
+end
+
+end real
+
 end condexp
 
 end measure_theory

src/probability/stopping.lean

@@ -3,9 +3,7 @@ Copyright (c) 2021 Kexing Ying. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying
 -/
-import measure_theory.constructions.borel_space
-import measure_theory.function.l1_space
-import measure_theory.function.strongly_measurable
+import measure_theory.function.conditional_expectation
 import topology.instances.discrete
 
 /-!
@@ -220,6 +218,14 @@ instance is_finite_measure.sigma_finite_filtration [preorder ι] (μ : measure 
   sigma_finite_filtration μ f :=
 ⟨λ n, by apply_instance⟩
 
+/-- Given a integrable function `g`, the conditional expectations of `g` with respect to a
+filtration is uniformly integrable. -/
+lemma integrable.uniform_integrable_condexp_filtration
+  [preorder ι] {μ : measure α} [is_finite_measure μ] {f : filtration ι m}
+  {g : α → ℝ} (hg : integrable g μ) :
+  uniform_integrable (λ i, μ[g | f i]) 1 μ :=
+hg.uniform_integrable_condexp f.le
+
 section adapted_process
 
 variables [topological_space β] [preorder ι]