From dcb6c8656c85e3980f971970824f6615c8bc081c Mon Sep 17 00:00:00 2001
From: Kexing Ying <kexing.ying19@imperial.ac.uk>
Date: Mon, 11 Apr 2022 16:38:55 +0000
Subject: [PATCH] feat(measure_theory/function/uniform_integrable): Equivalent
 condition for uniformly integrable in the probability sense (#12955)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

A sequence of functions is uniformly integrable in the probability sense if and only if `∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0, ∀ i, snorm ({x | C ≤ ∥f i x∥₊}.indicator (f i)) p μ ≤ ennreal.of_real ε`.
---
 src/algebra/order/ring.lean                   |  3 ++
 src/measure_theory/function/lp_space.lean     | 19 +++++++
 .../function/uniform_integrable.lean          | 49 ++++++++++++++++++-
 src/order/filter/indicator_function.lean      | 18 +++++++
 4 files changed, 88 insertions(+), 1 deletion(-)

diff --git a/src/algebra/order/ring.lean b/src/algebra/order/ring.lean
index 56dee3a0dd8b4..92e36678c07a1 100644
--- a/src/algebra/order/ring.lean
+++ b/src/algebra/order/ring.lean
@@ -359,6 +359,9 @@ decidable.mul_lt_mul h le_rfl hb (zero_le_one.trans h.le)
 lemma lt_mul_of_one_lt_left : 0 < b → 1 < a → b < a * b :=
 by classical; exact decidable.lt_mul_of_one_lt_left
 
+lemma lt_two_mul_self [nontrivial α] (ha : 0 < a) : a < 2 * a :=
+lt_mul_of_one_lt_left ha one_lt_two
+
 -- See Note [decidable namespace]
 protected lemma decidable.add_le_mul_two_add [@decidable_rel α (≤)] {a b : α}
   (a2 : 2 ≤ a) (b0 : 0 ≤ b) : a + (2 + b) ≤ a * (2 + b) :=
diff --git a/src/measure_theory/function/lp_space.lean b/src/measure_theory/function/lp_space.lean
index bbd2059e9c0ae..8a94331a24b37 100644
--- a/src/measure_theory/function/lp_space.lean
+++ b/src/measure_theory/function/lp_space.lean
@@ -1249,6 +1249,25 @@ end
 
 end monotonicity
 
+lemma snorm_indicator_ge_of_bdd_below (hp : p ≠ 0) (hp' : p ≠ ∞)
+  {f : α → F} (C : ℝ≥0) {s : set α} (hs : measurable_set s)
+  (hf : ∀ᵐ x ∂μ, x ∈ s → C ≤ ∥s.indicator f x∥₊) :
+  C • μ s ^ (1 / p.to_real) ≤ snorm (s.indicator f) p μ :=
+begin
+  rw [ennreal.smul_def, smul_eq_mul, snorm_eq_lintegral_rpow_nnnorm hp hp',
+    ennreal.le_rpow_one_div_iff (ennreal.to_real_pos hp hp'),
+    ennreal.mul_rpow_of_nonneg _ _ ennreal.to_real_nonneg,
+    ← ennreal.rpow_mul, one_div_mul_cancel (ennreal.to_real_pos hp hp').ne.symm, ennreal.rpow_one,
+    ← set_lintegral_const, ← lintegral_indicator _ hs],
+  refine lintegral_mono_ae _,
+  filter_upwards [hf] with x hx,
+  rw nnnorm_indicator_eq_indicator_nnnorm,
+  by_cases hxs : x ∈ s,
+  { simp only [set.indicator_of_mem hxs] at ⊢ hx,
+    exact ennreal.rpow_le_rpow (ennreal.coe_le_coe.2 (hx hxs)) ennreal.to_real_nonneg },
+  { simp [set.indicator_of_not_mem hxs] },
+end
+
 section is_R_or_C
 variables {𝕜 : Type*} [is_R_or_C 𝕜] {f : α → 𝕜}
 
diff --git a/src/measure_theory/function/uniform_integrable.lean b/src/measure_theory/function/uniform_integrable.lean
index abc407de3d12b..9b43b165933d4 100644
--- a/src/measure_theory/function/uniform_integrable.lean
+++ b/src/measure_theory/function/uniform_integrable.lean
@@ -731,7 +731,6 @@ of function `(fₙ)` satisfies for all `ε > 0`, there exists some `C ≥ 0` suc
 
 In this section, we will develope some API for `uniform_integrable` and prove that
 `uniform_integrable` is equivalent to this definition of uniform integrability.
-(Currently we only have the forward direction.)
 -/
 
 variables {p : ℝ≥0∞} {f : ι → α → β}
@@ -834,6 +833,54 @@ begin
   end
 end
 
+lemma uniform_integrable.spec (hp : p ≠ 0) (hp' : p ≠ ∞)
+  (hfu : uniform_integrable f p μ) {ε : ℝ} (hε : 0 < ε) :
+  ∃ C : ℝ≥0, ∀ i, snorm ({x | C ≤ ∥f i x∥₊}.indicator (f i)) p μ ≤ ennreal.of_real ε :=
+begin
+  obtain ⟨hf₀, hfu, M, hM⟩ := hfu,
+  obtain ⟨δ, hδpos, hδ⟩ := hfu hε,
+  obtain ⟨C, hC⟩ : ∃ C : ℝ≥0, ∀ i, μ {x | C ≤ ∥f i x∥₊} ≤ ennreal.of_real δ,
+  { by_contra hcon, push_neg at hcon,
+    choose ℐ hℐ using hcon,
+    lift δ to ℝ≥0 using hδpos.le,
+    have : ∀ C : ℝ≥0, C • (δ : ℝ≥0∞) ^ (1 / p.to_real) ≤ snorm (f (ℐ C)) p μ,
+    { intros C,
+      calc C • (δ : ℝ≥0∞) ^ (1 / p.to_real) ≤ C • μ {x | C ≤ ∥f (ℐ C) x∥₊} ^ (1 / p.to_real):
+      begin
+        rw [ennreal.smul_def, ennreal.smul_def, smul_eq_mul, smul_eq_mul],
+        simp_rw ennreal.of_real_coe_nnreal at hℐ,
+        refine ennreal.mul_le_mul le_rfl (ennreal.rpow_le_rpow (hℐ C).le
+          (one_div_nonneg.2 ennreal.to_real_nonneg)),
+      end
+      ... ≤ snorm ({x | C ≤ ∥f (ℐ C) x∥₊}.indicator (f (ℐ C))) p μ :
+      begin
+        refine snorm_indicator_ge_of_bdd_below hp hp' _
+          (measurable_set_le measurable_const (hf₀ _).nnnorm.measurable)
+          (eventually_of_forall $ λ x hx, _),
+        rwa [nnnorm_indicator_eq_indicator_nnnorm, indicator_of_mem hx],
+      end
+      ... ≤ snorm (f (ℐ C)) p μ : snorm_indicator_le _ },
+    specialize this ((2 * (max M 1) * (δ⁻¹ ^ (1 / p.to_real)))),
+    rw [ennreal.coe_rpow_of_nonneg _ (one_div_nonneg.2 ennreal.to_real_nonneg),
+      ← ennreal.coe_smul, smul_eq_mul, mul_assoc, nnreal.inv_rpow,
+      inv_mul_cancel (nnreal.rpow_pos (nnreal.coe_pos.1 hδpos)).ne.symm, mul_one,
+      ennreal.coe_mul, ← nnreal.inv_rpow] at this,
+    refine (lt_of_le_of_lt (le_trans (hM $ ℐ $ 2 * (max M 1) * (δ⁻¹ ^ (1 / p.to_real)))
+      (le_max_left M 1)) (lt_of_lt_of_le _ this)).ne rfl,
+    rw [← ennreal.coe_one, ← with_top.coe_max, ← ennreal.coe_mul, ennreal.coe_lt_coe],
+    exact lt_two_mul_self (lt_max_of_lt_right one_pos) },
+  exact ⟨C, λ i, hδ i _ (measurable_set_le measurable_const (hf₀ i).nnnorm.measurable) (hC i)⟩,
+end
+
+/-- The definition of uniform integrable in mathlib is equivalent to the definition commonly
+found in literature. -/
+lemma uniform_integrable_iff [is_finite_measure μ] (hp : 1 ≤ p) (hp' : p ≠ ∞) :
+  uniform_integrable f p μ ↔ (∀ i, strongly_measurable (f i)) ∧
+  ∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0,
+    ∀ i, snorm ({x | C ≤ ∥f i x∥₊}.indicator (f i)) p μ ≤ ennreal.of_real ε  :=
+⟨λ h, ⟨h.1, λ ε, h.spec (lt_of_lt_of_le ennreal.zero_lt_one hp).ne.symm hp'⟩,
+ λ h, uniform_integrable_of hp hp' h.1 h.2⟩
+
 end uniform_integrable
 
 end measure_theory
diff --git a/src/order/filter/indicator_function.lean b/src/order/filter/indicator_function.lean
index 63824c511ac9e..38ff66600c619 100644
--- a/src/order/filter/indicator_function.lean
+++ b/src/order/filter/indicator_function.lean
@@ -86,3 +86,21 @@ begin
   refine monotone.tendsto_indicator (λ n : finset ι, ⋃ i ∈ n, s i) _ f a,
   exact λ t₁ t₂, bUnion_subset_bUnion_left
 end
+
+lemma filter.eventually_eq.indicator [has_zero β] {l : filter α} {f g : α → β} {s : set α}
+  (hfg : f =ᶠ[l] g) :
+  s.indicator f =ᶠ[l] s.indicator g :=
+begin
+  filter_upwards [hfg] with x hx,
+  by_cases x ∈ s,
+  { rwa [indicator_of_mem h, indicator_of_mem h] },
+  { rw [indicator_of_not_mem h, indicator_of_not_mem h] }
+end
+
+lemma filter.eventually_eq.indicator_zero [has_zero β] {l : filter α}
+  {f : α → β} {s : set α} (hf : f =ᶠ[l] 0) :
+  s.indicator f =ᶠ[l] 0 :=
+begin
+  refine hf.indicator.trans _,
+  rw indicator_zero'
+end