refactor(measure_theory/integral/bochner): remove superfluous hypothe…

…sis (#10181)

* Remove hypothesis from `tendsto_integral_of_dominated_convergence` that was superfluous
* This results in simplifying some proofs, and removing some hypotheses from other lemmas
* Also remove some `ae_measurable` hypotheses for functions that were also assumed to be `integrable`.

src/analysis/calculus/parametric_integral.lean

@@ -111,7 +111,6 @@ begin
     intros x x_in,
     apply ae_measurable.const_smul,
     exact ((hF_meas _ x_in).sub (hF_meas _ x₀_in)).sub (hF'_meas.apply_continuous_linear_map _) },
-  { simp [measurable_const] },
   { apply mem_of_superset h_ball,
     intros x hx,
     apply (h_diff.and h_lipsch).mono,

src/measure_theory/constructions/prod.lean

@@ -277,7 +277,7 @@ begin
       simp only [f', hfx, simple_func.integral_eq_integral _ (this _), indicator_of_mem,
         mem_set_of_eq],
       refine tendsto_integral_of_dominated_convergence (λ y, ∥f x y∥ + ∥f x y∥)
-        (λ n, (s' n x).ae_measurable) hf.of_uncurry_left.ae_measurable (hfx.norm.add hfx.norm) _ _,
+        (λ n, (s' n x).ae_measurable) (hfx.norm.add hfx.norm) _ _,
       { exact λ n, eventually_of_forall (λ y, simple_func.norm_approx_on_zero_le _ _ (x, y) n) },
       { exact eventually_of_forall (λ y, simple_func.tendsto_approx_on _ _ (by simp)) } },
     { simpa [f', hfx, integral_undef] using @tendsto_const_nhds _ _ _ (0 : E) _, } },

src/measure_theory/integral/bochner.lean

@@ -832,12 +832,13 @@ end
   everywhere convergence of a sequence of functions implies the convergence of their integrals. -/
 theorem tendsto_integral_of_dominated_convergence {F : ℕ → α → E} {f : α → E} (bound : α → ℝ)
   (F_measurable : ∀ n, ae_measurable (F n) μ)
-  (f_measurable : ae_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 (𝓝 $ ∫ a, f a ∂μ) :=
 begin
+  /- `f` is a.e.-measurable, since it is the a.e.-pointwise limit of a.e.-measurable functions. -/
+  have f_measurable : ae_measurable f μ := ae_measurable_of_tendsto_metric_ae F_measurable h_lim,
   /- 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
@@ -864,7 +865,6 @@ lemma tendsto_integral_filter_of_dominated_convergence {ι} {l : filter ι}
   [l.is_countably_generated]
   {F : ι → α → E} {f : α → E} (bound : α → ℝ)
   (hF_meas : ∀ᶠ n in l, ae_measurable (F n) μ)
-  (f_measurable : ae_measurable f μ)
   (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, ∥F n a∥ ≤ bound a)
   (bound_integrable : integrable bound μ)
   (h_lim : ∀ᵐ a ∂μ, tendsto (λ n, F n a) l (𝓝 (f a))) :
@@ -877,12 +877,9 @@ begin
   replace h := hxl _ h,
   rcases h with ⟨k, h⟩,
   rw ← tendsto_add_at_top_iff_nat k,
-  refine tendsto_integral_of_dominated_convergence _ _ _ _ _ _,
-  { exact bound },
-  { intro, refine (h _ _).1, exact nat.le_add_left _ _ },
-  { assumption },
-  { assumption },
-  { intro, refine (h _ _).2, exact nat.le_add_left _ _ },
+  refine tendsto_integral_of_dominated_convergence bound _ bound_integrable _ _,
+  { intro, refine (h _ _).1, apply self_le_add_left },
+  { intro, refine (h _ _).2, apply self_le_add_left },
   { filter_upwards [h_lim],
     assume a h_lim,
     apply @tendsto.comp _ _ _ (λn, x (n + k)) (λn, F n a),
@@ -898,7 +895,7 @@ lemma continuous_at_of_dominated {F : X → α → E} {x₀ : X} {bound : α →
   (h_bound : ∀ᶠ x in 𝓝 x₀, ∀ᵐ a ∂μ, ∥F x a∥ ≤ bound a)
   (bound_integrable : integrable bound μ) (h_cont : ∀ᵐ a ∂μ, continuous_at (λ x, F x a) x₀) :
   continuous_at (λ x, ∫ a, F x a ∂μ) x₀ :=
-tendsto_integral_filter_of_dominated_convergence bound ‹_› (mem_of_mem_nhds hF_meas : _) ‹_› ‹_› ‹_›
+tendsto_integral_filter_of_dominated_convergence bound ‹_› ‹_› ‹_› ‹_›
 
 lemma continuous_of_dominated {F : X → α → E} {bound : α → ℝ}
   (hF_meas : ∀ x, ae_measurable (F x) μ) (h_bound : ∀ x, ∀ᵐ a ∂μ, ∥F x a∥ ≤ bound a)

src/measure_theory/integral/integral_eq_improper.lean

@@ -324,24 +324,23 @@ variables {α ι E : Type*} [measurable_space α] {μ : measure α} {l : filter
   [complete_space E] [second_countable_topology E]
 
 lemma ae_cover.integral_tendsto_of_countably_generated [l.is_countably_generated]
-  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E} (hfm : ae_measurable f μ)
-  (hfi : integrable f μ) :
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E} (hfi : integrable f μ) :
   tendsto (λ i, ∫ x in φ i, f x ∂μ) l (𝓝 $ ∫ x, f x ∂μ) :=
 suffices h : tendsto (λ i, ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ)),
 by { convert h, ext n, rw integral_indicator (hφ.measurable n) },
 tendsto_integral_filter_of_dominated_convergence (λ x, ∥f x∥)
-  (eventually_of_forall $ λ i, hfm.indicator $ hφ.measurable i) hfm
+  (eventually_of_forall $ λ i, hfi.ae_measurable.indicator $ hφ.measurable i)
   (eventually_of_forall $ λ i, ae_of_all _ $ λ x, norm_indicator_le_norm_self _ _)
   hfi.norm hφ.ae_tendsto_indicator
 
 /-- Slight reformulation of
     `measure_theory.ae_cover.integral_tendsto_of_countably_generated`. -/
 lemma ae_cover.integral_eq_of_tendsto [l.ne_bot] [l.is_countably_generated]
   {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E}
-  (I : E) (hfm : ae_measurable f μ) (hfi : integrable f μ)
+  (I : E) (hfi : integrable f μ)
   (h : tendsto (λ n, ∫ x in φ n, f x ∂μ) l (𝓝 I)) :
   ∫ x, f x ∂μ = I :=
-tendsto_nhds_unique (hφ.integral_tendsto_of_countably_generated hfm hfi) h
+tendsto_nhds_unique (hφ.integral_tendsto_of_countably_generated hfi) h
 
 lemma ae_cover.integral_eq_of_tendsto_of_nonneg_ae [l.ne_bot] [l.is_countably_generated]
   {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → ℝ} (I : ℝ)
@@ -350,7 +349,7 @@ lemma ae_cover.integral_eq_of_tendsto_of_nonneg_ae [l.ne_bot] [l.is_countably_ge
   ∫ x, f x ∂μ = I :=
 have hfi' : integrable f μ,
   from hφ.integrable_of_integral_tendsto_of_nonneg_ae I hfm hfi hnng htendsto,
-hφ.integral_eq_of_tendsto I hfm hfi' htendsto
+hφ.integral_eq_of_tendsto I hfi' htendsto
 
 end integral
 
@@ -427,9 +426,7 @@ variables {α ι E : Type*}
           {l : filter ι} [is_countably_generated l]
           [measurable_space E] [normed_group E] [normed_space ℝ E] [borel_space E]
           [complete_space E] [second_countable_topology E]
-          {a b : ι → α} {f : α → E} (hfm : ae_measurable f μ)
-
-include hfm
+          {a b : ι → α} {f : α → E}
 
 lemma interval_integral_tendsto_integral [no_bot_order α] [nonempty α]
   (hfi : integrable f μ) (ha : tendsto a l at_bot) (hb : tendsto b l at_top) :
@@ -438,7 +435,7 @@ begin
   let φ := λ i, Ioc (a i) (b i),
   let c : α := classical.choice ‹_›,
   have hφ : ae_cover μ l φ := ae_cover_Ioc ha hb,
-  refine (hφ.integral_tendsto_of_countably_generated hfm hfi).congr' _,
+  refine (hφ.integral_tendsto_of_countably_generated hfi).congr' _,
   filter_upwards [ha.eventually (eventually_le_at_bot c), hb.eventually (eventually_ge_at_top c)],
   intros i hai hbi,
   exact (interval_integral.integral_of_le (hai.trans hbi)).symm
@@ -450,7 +447,7 @@ lemma interval_integral_tendsto_integral_Iic [no_bot_order α] (b : α)
 begin
   let φ := λ i, Ioi (a i),
   have hφ : ae_cover (μ.restrict $ Iic b) l φ := ae_cover_Ioi ha,
-  refine (hφ.integral_tendsto_of_countably_generated hfm.restrict hfi).congr' _,
+  refine (hφ.integral_tendsto_of_countably_generated hfi).congr' _,
   filter_upwards [ha.eventually (eventually_le_at_bot $ b)],
   intros i hai,
   rw [interval_integral.integral_of_le hai, measure.restrict_restrict (hφ.measurable i)],
@@ -463,7 +460,7 @@ lemma interval_integral_tendsto_integral_Ioi (a : α)
 begin
   let φ := λ i, Iic (b i),
   have hφ : ae_cover (μ.restrict $ Ioi a) l φ := ae_cover_Iic hb,
-  refine (hφ.integral_tendsto_of_countably_generated hfm.restrict hfi).congr' _,
+  refine (hφ.integral_tendsto_of_countably_generated hfi).congr' _,
   filter_upwards [hb.eventually (eventually_ge_at_top $ a)],
   intros i hbi,
   rw [interval_integral.integral_of_le hbi, measure.restrict_restrict (hφ.measurable i),

src/measure_theory/integral/interval_integral.lean

@@ -884,7 +884,6 @@ variables {μ : measure α}
 lemma continuous_within_at_of_dominated_interval
   {F : X → α → E} {x₀ : X} {bound : α → ℝ} {a b : α} {s : set X}
   (hF_meas : ∀ᶠ x in 𝓝[s] x₀, ae_measurable (F x) (μ.restrict $ Ι a b))
-  (hF_meas₀ : ae_measurable (F x₀) (μ.restrict $ Ι a b))
   (h_bound : ∀ᶠ x in 𝓝[s] x₀, ∀ᵐ t ∂(μ.restrict $ Ι a b), ∥F x t∥ ≤ bound t)
   (bound_integrable : interval_integrable bound μ a b)
   (h_cont : ∀ᵐ t ∂(μ.restrict $ Ι a b), continuous_within_at (λ x, F x t) s x₀) :
@@ -897,7 +896,7 @@ begin
    { rw interval_oc_of_lt hab at *,
      simp_rw interval_integral.integral_of_ge hab.le,
      refine tendsto.neg _ }];
-  apply tendsto_integral_filter_of_dominated_convergence bound hF_meas hF_meas₀ h_bound,
+  apply tendsto_integral_filter_of_dominated_convergence bound hF_meas h_bound,
   exacts [bound_integrable_left, h_cont, bound_integrable_right, h_cont]
 end
 
@@ -917,7 +916,7 @@ lemma continuous_at_of_dominated_interval
 begin
   rw ←  continuous_within_at_univ,
   apply continuous_within_at_of_dominated_interval ; try { rw nhds_within_univ},
-  exacts [hF_meas, (mem_of_mem_nhds hF_meas : _), h_bound, bound_integrable,
+  exacts [hF_meas, h_bound, bound_integrable,
           h_cont.mono (λ a, (continuous_within_at_univ (λ x, F x a) x₀).mpr)]
 end
 
@@ -977,20 +976,14 @@ begin
     apply continuous_within_at.congr_of_eventually_eq _ this (integral_indicator h₀).symm,
     have : interval_integrable (λ x, ∥f x∥) μ b₁ b₂,
       from interval_integrable.norm (h_int' $ right_mem_Icc.mpr h₁₂),
-    refine continuous_within_at_of_dominated_interval _ _ _ this _ ; clear this,
+    refine continuous_within_at_of_dominated_interval _ _ this _ ; clear this,
     { apply eventually.mono (self_mem_nhds_within),
       intros x hx,
       erw [ae_measurable_indicator_iff, measure.restrict_restrict, Iic_inter_Ioc_of_le],
       { rw min₁₂,
         exact (h_int' hx).1.ae_measurable },
       { exact le_max_of_le_right hx.2 },
       exacts [measurable_set_Iic, measurable_set_Iic] },
-    { erw [ae_measurable_indicator_iff, measure.restrict_restrict, Iic_inter_Ioc_of_le],
-      { rw min₁₂,
-        exact (h_int' h₀).1.ae_measurable },
-      { exact le_max_of_le_right h₀.2 },
-      exact measurable_set_Iic,
-      exact measurable_set_Iic },
     { refine eventually_of_forall (λ (x : α), eventually_of_forall (λ (t : α), _)),
       dsimp [indicator],
       split_ifs ; simp },

src/measure_theory/integral/set_integral.lean

@@ -489,12 +489,10 @@ begin
     from funext (λ i, (integral_indicator (hsm i)).symm),
   rw h_int_eq,
   rw ← integral_indicator (measurable_set.Inter hsm),
-  refine tendsto_integral_of_dominated_convergence bound _ _ _ _ _,
+  refine tendsto_integral_of_dominated_convergence bound _ _ _ _,
   { intro n,
     rw ae_measurable_indicator_iff (hsm n),
     exact (integrable_on.mono_set hfi (h_anti (zero_le n))).1 },
-  { rw ae_measurable_indicator_iff (measurable_set.Inter hsm),
-    exact (integrable_on.mono_set hfi (set.Inter_subset s 0)).1, },
   { rw integrable_indicator_iff (hsm 0),
     exact hfi.norm, },
   { simp_rw norm_indicator_eq_indicator_norm,