[Merged by Bors] - feat(measure_theory/function/uniform_integrable): Equivalent condition for uniformly integrable in the probability sense

src/data/real/nnreal.lean

@@ -642,6 +642,12 @@ lemma half_lt_self {a : ℝ≥0} (h : a ≠ 0) : a / 2 < a :=
 by rw [← nnreal.coe_lt_coe, nnreal.coe_div]; exact
 half_lt_self (bot_lt_iff_ne_bot.2 h)
 
+lemma lt_mul_two_self {a : ℝ≥0} (ha : a ≠ 0) : a < 2 * a :=
+begin
+  rw ← nnreal.div_lt_iff' two_ne_zero,
+  exact nnreal.half_lt_self ha,
+end
+
 lemma two_inv_lt_one : (2⁻¹:ℝ≥0) < 1 :=
 by simpa using half_lt_self zero_ne_one.symm
 

src/measure_theory/function/lp_space.lean

@@ -1248,6 +1248,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 : α → 𝕜}
 

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,55 @@ 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,
+  replace hM : ∀ (i : ι), snorm (f i) p μ ≤ max M 1 := λ i, le_trans (hM i) (le_max_left _ _),
+  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 hM (ℐ (2 * (max M 1) * (δ⁻¹ ^ (1 / p.to_real)))),
+    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 hM (lt_of_lt_of_le _ this)).ne rfl,
+    rw [← ennreal.coe_one, ← with_top.coe_max, ← ennreal.coe_mul, ennreal.coe_lt_coe],
+    exact nnreal.lt_mul_two_self (ne.symm $ ne_of_lt $ 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

src/measure_theory/measure/measure_space.lean

@@ -3424,6 +3424,15 @@ piecewise_ae_eq_of_ae_eq_set hst
 lemma indicator_meas_zero (hs : μ s = 0) : indicator s f =ᵐ[μ] 0 :=
 (indicator_empty' f) ▸ indicator_ae_eq_of_ae_eq_set (ae_eq_empty.2 hs)
 
+lemma indicator_ae_eq_zero_of_ae_eq_zero (hf : f =ᵐ[μ] 0) : s.indicator f =ᵐ[μ] 0 :=
+begin
+  filter_upwards [hf] with x hx,
+  by_cases x ∈ s,
+  { rwa indicator_of_mem h },
+  { rw indicator_of_not_mem h,
+    refl }
+end
+
 variables [measurable_space β]
 
 lemma ae_measurable_indicator_iff {s} (hs : measurable_set s) :