feat(measure/bochner_integration): dominated convergence theorem (#1757)

* feat(measure/bochner_integration): dominated convergence theorem

This PR
* proves the dominated convergence theorem
* and some other lemmas including `integral_congr_ae`, `norm_integral_le_lintegral_norm`.
* adds several equivalent definitions of the predicate `integrable` and shortens some proofs.

* fix linting error

* Add some section doc strings

* Indentation is very wrong

* Remove useless assumptions; fix doc strings

* remove `private`; add a doc string for Lebesgue's dominated convergence theorem

* Update basic.lean

src/analysis/normed_space/basic.lean

@@ -207,6 +207,12 @@ nnreal.eq $ norm_neg g
 lemma nndist_nnnorm_nnnorm_le (g h : α) : nndist (nnnorm g) (nnnorm h) ≤ nnnorm (g - h) :=
 nnreal.coe_le.2 $ dist_norm_norm_le g h
 
+lemma of_real_norm_eq_coe_nnnorm (x : β) : ennreal.of_real ∥x∥ = (nnnorm x : ennreal) :=
+ennreal.of_real_eq_coe_nnreal _
+
+lemma edist_eq_coe_nnnorm (x : β) : edist x 0 = (nnnorm x : ennreal) :=
+by { rw [edist_dist, dist_eq_norm, _root_.sub_zero, of_real_norm_eq_coe_nnnorm] }
+
 end nnnorm
 
 /-- A submodule of a normed group is also a normed group, with the restriction of the norm.

src/measure_theory/bochner_integration.lean

@@ -61,7 +61,7 @@ Bochner integral, simple function, function space
 -/
 
 noncomputable theory
-open_locale classical
+open_locale classical topological_space
 
 set_option class.instance_max_depth 100
 
@@ -76,6 +76,11 @@ local infixr ` →ₛ `:25 := simple_func
 namespace simple_func
 
 section bintegral
+/-! ### The Bochner integral of simple functions
+
+Define the Bochner integral of simple functions of the type `α →ₛ β` where `β` is a normed group,
+and prove basic property of this integral.
+-/
 open finset
 
 variables [normed_group β] [normed_group γ]
@@ -294,6 +299,7 @@ infixr ` →₁ₛ `:25 := measure_theory.l1.simple_func
 namespace simple_func
 
 section instances
+/-! Simple functions in L1 space form a `normed_space`. -/
 
 instance : has_coe (α →₁ₛ β) (α →₁ β) := ⟨subtype.val⟩
 
@@ -593,6 +599,7 @@ end
 end to_simple_func
 
 section coe_to_l1
+/-! The embedding of integrable simple functions `α →₁ₛ β` into L1 is a uniform and dense embedding. -/
 
 lemma exists_simple_func_near (f : α →₁ β) {ε : ℝ} (ε0 : 0 < ε) :
   ∃ s : α →₁ₛ β, dist f s < ε :=
@@ -651,6 +658,7 @@ variables {α β 𝕜}
 end coe_to_l1
 
 section simple_func_integral
+/-! Define the Bochner integral on `α →₁ₛ β` and prove basic properties of this integral. -/
 
 variables [normed_space ℝ β]
 
@@ -715,6 +723,8 @@ open simple_func
 
 variables [normed_space ℝ β] [normed_space ℝ γ] [complete_space β]
 
+section integration_in_l1
+
 local notation `to_l1` := coe_to_l1 α β ℝ
 local attribute [instance] simple_func.normed_group simple_func.normed_space
 
@@ -746,6 +756,23 @@ map_sub integral_clm f g
 lemma integral_smul (r : ℝ) (f : α →₁ β) : integral (r • f) = r • integral f :=
 map_smul r integral_clm f
 
+local notation `Integral` := @integral_clm α _ β _ _ _ _
+local notation `sIntegral` := @simple_func.integral_clm α _ β _ _ _
+
+lemma norm_Integral_le_one : ∥Integral∥ ≤ 1 :=
+calc ∥Integral∥ ≤ 1 * ∥sIntegral∥ :
+  op_norm_extend_le _ _ _ $ λs, by {rw one_mul, refl}
+  ... = ∥sIntegral∥ : one_mul _
+  ... ≤ 1 : norm_Integral_le_one
+
+lemma norm_integral_le (f : α →₁ β) : ∥integral f∥ ≤ ∥f∥ :=
+calc ∥integral f∥ = ∥Integral f∥ : rfl
+  ... ≤ ∥Integral∥ * ∥f∥ : le_op_norm _ _
+  ... ≤ 1 * ∥f∥ : mul_le_mul_of_nonneg_right norm_Integral_le_one $ norm_nonneg _
+  ... = ∥f∥ : one_mul _
+
+end integration_in_l1
+
 end l1
 
 variables [normed_group β] [second_countable_topology β] [normed_space ℝ β] [complete_space β]
@@ -757,6 +784,8 @@ if hf : measurable f ∧ integrable f
 then (l1.of_fun f hf.1 hf.2).integral
 else 0
 
+notation `∫` binders `, ` r:(scoped f, integral f) := r
+
 section properties
 
 open continuous_linear_map measure_theory.simple_func
@@ -819,7 +848,7 @@ begin
   { exact ⟨measurable_sub hfm hgm, integrable_sub hfm hgm hfi hgi⟩ }
 end
 
-lemma integral_smul (r : ℝ) (f : α → β) : integral (λx, r • (f x)) = r • integral f :=
+lemma integral_smul (r : ℝ) (f : α → β) : (∫ x, r • (f x)) = r • integral f :=
 begin
   by_cases r0 : r = 0,
   { have : (λx, r • (f x)) = 0, { funext, rw [r0, zero_smul, pi.zero_apply] },
@@ -842,6 +871,94 @@ begin
     { rw not_and_distrib, rw [measurable_smul_iff r0], exact or.inl hfm, apply_instance } },
 end
 
+lemma integral_congr_ae (hfm : measurable f) (hgm : measurable g) (h : ∀ₘ a, f a = g a) :
+   integral f = integral g :=
+begin
+  by_cases hfi : integrable f,
+  { have hgi : integrable g := integrable_of_ae_eq hfi h,
+    simp only [integral],
+    repeat { rw dif_pos },
+    rotate, { exact ⟨hgm, hgi⟩ }, { exact ⟨hfm, hfi⟩ },
+    rw ← l1.of_fun_eq_of_fun f g hfm hfi hgm hgi at h,
+    rw h },
+  { have hgi : ¬ integrable g, { rw integrable_iff_of_ae_eq h at hfi, exact hfi },
+    rw [integral_eq_zero_of_non_integrable hfi, integral_eq_zero_of_non_integrable hgi] },
+end
+
+lemma of_real_norm_integral_le_lintegral_norm (f : α → β) :
+  ennreal.of_real ∥integral f∥ ≤ ∫⁻ a, ennreal.of_real ∥f a∥ :=
+begin
+  by_cases hfm : measurable f,
+  by_cases hfi : integrable f,
+  rotate,
+  { rw [integral_eq_zero_of_non_integrable hfi, _root_.norm_zero, of_real_zero], exact zero_le _ },
+  { rw [integral_eq_zero_of_non_measurable hfm, _root_.norm_zero, of_real_zero], exact zero_le _ },
+  rw [integral, dif_pos],
+  rotate, { exact ⟨hfm, hfi⟩ },
+  calc ennreal.of_real ∥l1.integral (l1.of_fun f hfm hfi)∥ ≤ (ennreal.of_real ∥l1.of_fun f hfm hfi∥) :
+    of_real_le_of_real $ l1.norm_integral_le _
+    ... = (ennreal.of_real $ ennreal.to_real $ ∫⁻ a, ennreal.of_real $ ∥(l1.of_fun f hfm hfi).to_fun a∥) :
+    by { rw l1.norm_eq_norm_to_fun }
+    ... = (ennreal.of_real $ ennreal.to_real $ ∫⁻ a, ennreal.of_real ∥f a∥) :
+    begin
+      congr' 2,
+      apply lintegral_congr_ae,
+      filter_upwards [l1.to_fun_of_fun f hfm hfi],
+      simp only [mem_set_of_eq],
+      assume a h,
+      rw h
+    end
+    ... = (∫⁻ a, ennreal.of_real ∥f a∥) :
+    by { rw of_real_to_real, rw ← lt_top_iff_ne_top, rwa ← integrable_iff_norm }
+end
+
+lemma norm_integral_le_lintegral_norm (f : α → β) :
+  ∥integral f∥ ≤ ennreal.to_real (∫⁻ a, ennreal.of_real ∥f a∥) :=
+begin
+  by_cases hfi : integrable f,
+  rotate,
+  { rw [integral_eq_zero_of_non_integrable hfi, _root_.norm_zero], exact to_real_nonneg },
+  have := (to_real_le_to_real _ _).2 (of_real_norm_integral_le_lintegral_norm f),
+  { rwa to_real_of_real (norm_nonneg _) at this },
+  { exact of_real_ne_top },
+  { rw ← lt_top_iff_ne_top, rwa ← integrable_iff_norm }
+end
+
+/-- Lebesgue dominated convergence theorem provides sufficient conditions under which almost
+  everywhere convergence of a sequence of functions implies the convergence of their integrals. -/
+theorem tendsto_integral_of_dominated_convergence {F : ℕ → α → β} {f : α → β} {bound : α → ℝ}
+  (F_measurable : ∀ n, measurable (F n))
+  (f_measurable : measurable f)
+  (bound_integrable : integrable bound)
+  (h_bound : ∀ n, ∀ₘ a, ∥F n a∥ ≤ bound a)
+  (h_lim : ∀ₘ a, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
+  tendsto (λn, ∫ a, F n a) at_top (𝓝 $ integral f) :=
+begin
+  /- To show `(∫ a, F n a) --> (∫ f)`, suffices to show `∥∫ a, F n a - ∫ f∥ --> 0` -/
+  rw tendsto_iff_norm_tendsto_zero,
+  /- But `0 ≤ ∥∫ a, F n a - ∫ f∥ = ∥∫ a, (F n a - f a) ∥ ≤ ∫ a, ∥F n a - f a∥, and thus we apply the
+    sandwich theorem and prove that `∫ a, ∥F n a - f a∥ --> 0` -/
+  have zero_tendsto_zero : tendsto (λn:ℕ, (0 : ℝ)) at_top (𝓝 0) := tendsto_const_nhds,
+  have lintegral_norm_tendsto_zero :
+    tendsto (λn, ennreal.to_real $ ∫⁻ a, ennreal.of_real ∥F n a - f a∥) at_top (𝓝 0) :=
+  tendsto.comp (tendsto_to_real (zero_ne_top))
+    (tendsto_lintegral_norm_of_dominated_convergence
+      F_measurable f_measurable bound_integrable h_bound h_lim),
+  -- Use the sandwich theorem
+  refine tendsto_of_tendsto_of_tendsto_of_le_of_le zero_tendsto_zero lintegral_norm_tendsto_zero _ _,
+  -- Show `0 ≤ ∥∫ a, F n a - ∫ f∥` for all `n`
+  { simp only [filter.mem_at_top_sets, norm_nonneg, set.mem_set_of_eq, forall_true_iff,
+      exists_const] },
+  -- Show `∥∫ a, F n a - ∫ f∥ ≤ ∫ a, ∥F n a - f a∥` for all `n`
+  { simp only [mem_at_top_sets, mem_set_of_eq],
+    use 0,
+    assume n hn,
+    have h₁ : integrable (F n) := integrable_of_integrable_bound bound_integrable (h_bound _),
+    have h₂ : integrable f := integrable_of_dominated_convergence bound_integrable h_bound h_lim,
+    rw ← integral_sub (F_measurable _) h₁ f_measurable h₂,
+    exact norm_integral_le_lintegral_norm _ }
+end
+
 end properties
 
 run_cmd mk_simp_attr `integral_simps

src/measure_theory/integration.lean

@@ -1139,7 +1139,7 @@ calc
     lintegral_congr_ae $ all_ae_of_all $ assume a, limsup_eq_infi_supr_of_nat.symm
 
 /-- Dominated convergence theorem for nonnegative functions -/
-lemma dominated_convergence_nn
+lemma tendsto_lintegral_of_dominated_convergence
   {F : ℕ → α → ennreal} {f : α → ennreal} {g : α → ennreal}
   (hF_meas : ∀n, measurable (F n)) (h_bound : ∀n, ∀ₘ a, F n a ≤ g a)
   (h_fin : lintegral g < ⊤)