From b4641efe629771968e0fe99000c3b708376f62f7 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Tue, 22 Sep 2020 08:41:20 +0000
Subject: [PATCH] feat(l1_space): add measurability to integrable (#4170)

This PR defines `integrable` such that `integrable` implies `measurable`. The old version is called `has_finite_integral`.

This allows us to drop *many* measurability conditions from lemmas that also require integrability.
There are some lemmas that have extra measurability conditions, if it has `integrable` as conclusion without corresponding `measurable` hypothesis.
There are many results that require an additional `[measurable_space E]` hypothesis, and some that require `[borel_space E]` or `[second_countable_space E]` (usually when using that addition is measurable).
---
 src/measure_theory/bochner_integration.lean | 234 ++++-----
 src/measure_theory/borel_space.lean         |   2 +-
 src/measure_theory/interval_integral.lean   | 286 +++++-----
 src/measure_theory/l1_space.lean            | 548 ++++++++++++--------
 src/measure_theory/set_integral.lean        | 198 ++++---
 src/measure_theory/simple_func_dense.lean   |  27 +-
 6 files changed, 684 insertions(+), 611 deletions(-)

diff --git a/src/measure_theory/bochner_integration.lean b/src/measure_theory/bochner_integration.lean
index 0bb1df5a981df..c68953e5951bf 100644
--- a/src/measure_theory/bochner_integration.lean
+++ b/src/measure_theory/bochner_integration.lean
@@ -179,13 +179,14 @@ and prove basic property of this integral.
 -/
 open finset
 
-variables [normed_group E] [normed_group F] {μ : measure α}
+variables [normed_group E] [measurable_space E] [normed_group F]
+variables {μ : measure α}
 
 /-- For simple functions with a `normed_group` as codomain, being integrable is the same as having
     finite volume support. -/
 lemma integrable_iff_fin_meas_supp {f : α →ₛ E} {μ : measure α} :
   integrable f μ ↔ f.fin_meas_supp μ :=
-calc integrable f μ ↔ ∫⁻ x, f.map (coe ∘ nnnorm : E → ennreal) x ∂μ < ⊤ : iff.rfl
+calc integrable f μ ↔ ∫⁻ x, f.map (coe ∘ nnnorm : E → ennreal) x ∂μ < ⊤ : and_iff_right f.measurable
 ... ↔ (f.map (coe ∘ nnnorm : E → ennreal)).lintegral μ < ⊤ : by rw lintegral_eq_lintegral
 ... ↔ (f.map (coe ∘ nnnorm : E → ennreal)).fin_meas_supp μ : iff.symm $
   fin_meas_supp.iff_lintegral_lt_top $ eventually_of_forall $ λ x, coe_lt_top
@@ -194,7 +195,7 @@ calc integrable f μ ↔ ∫⁻ x, f.map (coe ∘ nnnorm : E → ennreal) x ∂
 lemma fin_meas_supp.integrable {f : α →ₛ E} (h : f.fin_meas_supp μ) : integrable f μ :=
 integrable_iff_fin_meas_supp.2 h
 
-lemma integrable_pair {f : α →ₛ E} {g : α →ₛ F} :
+lemma integrable_pair [measurable_space F] {f : α →ₛ E} {g : α →ₛ F} :
   integrable f μ → integrable g μ → integrable (pair f g) μ :=
 by simpa only [integrable_iff_fin_meas_supp] using fin_meas_supp.pair
 
@@ -260,7 +261,7 @@ lemma integral_congr {f g : α →ₛ E} (hf : integrable f μ) (h : f =ᵐ[μ]
   f.integral μ = g.integral μ :=
 show ((pair f g).map prod.fst).integral μ = ((pair f g).map prod.snd).integral μ, from
 begin
-  have inte := integrable_pair hf (hf.congr h),
+  have inte := integrable_pair hf (hf.congr g.measurable h),
   rw [map_integral (pair f g) _ inte prod.fst_zero, map_integral (pair f g) _ inte prod.snd_zero],
   refine finset.sum_congr rfl (assume p hp, _),
   rcases mem_range.1 hp with ⟨a, rfl⟩,
@@ -321,7 +322,7 @@ calc integral μ (-f) = integral μ (f.map (has_neg.neg)) : rfl
     refine finset.sum_congr rfl (λx h, smul_neg _ _),
   end
 
-lemma integral_sub {f g : α →ₛ E} (hf : integrable f μ) (hg : integrable g μ) :
+lemma integral_sub [borel_space E] {f g : α →ₛ E} (hf : integrable f μ) (hg : integrable g μ) :
   integral μ (f - g) = integral μ f - integral μ g :=
 begin
   rw [sub_eq_add_neg, integral_add hf, integral_neg hg, sub_eq_add_neg],
@@ -362,8 +363,6 @@ begin
   exacts [hf.left_of_add_measure, hf.right_of_add_measure]
 end
 
-variables [second_countable_topology E] [measurable_space E] [borel_space E]
-
 end integral
 
 end simple_func
@@ -497,26 +496,24 @@ section of_simple_func
 
 /-- Construct the equivalence class `[f]` of an integrable simple function `f`. -/
 @[reducible] def of_simple_func (f : α →ₛ E) (hf : integrable f μ) : (α →₁ₛ[μ] E) :=
-⟨l1.of_fun f f.measurable hf, ⟨f, rfl⟩⟩
+⟨l1.of_fun f hf, ⟨f, rfl⟩⟩
 
 lemma of_simple_func_eq_of_fun (f : α →ₛ E) (hf : integrable f μ) :
-  (of_simple_func f hf : α →₁[μ] E) = l1.of_fun f f.measurable hf := rfl
+  (of_simple_func f hf : α →₁[μ] E) = l1.of_fun f hf := rfl
 
 lemma of_simple_func_eq_mk (f : α →ₛ E) (hf : integrable f μ) :
   (of_simple_func f hf : α →ₘ[μ] E) = ae_eq_fun.mk f f.measurable := rfl
 
-lemma of_simple_func_zero : of_simple_func (0 : α →ₛ E) (integrable_zero α μ E) = 0 := rfl
+lemma of_simple_func_zero : of_simple_func (0 : α →ₛ E) (integrable_zero α E μ) = 0 := rfl
 
-lemma of_simple_func_add (f g : α →ₛ E) (hf hg) :
-  (of_simple_func (f + g) (integrable.add f.measurable hf g.measurable hg) : α →₁ₛ[μ] E) =
-    of_simple_func f hf + of_simple_func g hg := rfl
+lemma of_simple_func_add (f g : α →ₛ E) (hf : integrable f μ) (hg : integrable g μ) :
+  of_simple_func (f + g) (hf.add hg) = of_simple_func f hf + of_simple_func g hg := rfl
 
 lemma of_simple_func_neg (f : α →ₛ E) (hf : integrable f μ) :
   of_simple_func (-f) hf.neg = -of_simple_func f hf := rfl
 
-lemma of_simple_func_sub (f g : α →ₛ E) (hf : integrable f μ) (hg) :
-  of_simple_func (f - g) (hf.sub f.measurable g.measurable hg) =
-    of_simple_func f hf - of_simple_func g hg := rfl
+lemma of_simple_func_sub (f g : α →ₛ E) (hf : integrable f μ) (hg : integrable g μ) :
+  of_simple_func (f - g) (hf.sub hg) = of_simple_func f hf - of_simple_func g hg := rfl
 
 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 E]
 
@@ -552,8 +549,7 @@ by { rw ← mk_eq_mk, exact classical.some_spec (of_simple_func f hfi).2 }
 
 lemma to_simple_func_eq_to_fun (f : α →₁ₛ[μ] E) : f.to_simple_func =ᵐ[μ] f :=
 begin
-  rw [← of_fun_eq_of_fun f.to_simple_func f f.measurable f.integrable
-    (f : α →₁[μ] E).measurable (f : α →₁[μ] E).integrable, ← l1.eq_iff],
+  rw [← of_fun_eq_of_fun f.to_simple_func f f.integrable (f : α →₁[μ] E).integrable, ← l1.eq_iff],
   simp only [of_fun_eq_mk, ← coe_coe, mk_to_fun],
   exact classical.some_spec f.coe_prop
 end
@@ -674,7 +670,7 @@ begin
   apply simple_func.uniform_embedding.dense_embedding,
   rintros ⟨⟨f, hfm⟩, hfi⟩,
   rw mem_closure_iff_seq_limit,
-  rcases simple_func_sequence_tendsto' hfm ((integrable_mk hfm).1 hfi) with ⟨F, hF⟩,
+  rcases simple_func_sequence_tendsto' ((integrable_mk hfm).1 hfi) with ⟨F, hF⟩,
   refine ⟨λ n, ↑(of_simple_func (F n) (hF.1 n)), λ n, mem_range_self _, _⟩,
   rw tendsto_iff_edist_tendsto_0,
   simpa [edist_mk_mk, ← edist_nndist] using hF.2
@@ -836,8 +832,8 @@ begin
     have := f.to_simple_func.pos_part_sub_neg_part,
     conv_lhs {rw ← this},
     refl },
-  { exact (integrable.max_zero f.integrable).congr ae_eq₁ },
-  { exact (integrable.max_zero f.integrable.neg).congr ae_eq₂ }
+  { exact f.integrable.max_zero.congr (measure_theory.simple_func.measurable _) ae_eq₁ },
+  { exact f.integrable.neg.max_zero.congr (measure_theory.simple_func.measurable _) ae_eq₂ }
 end
 
 end pos_part
@@ -938,9 +934,7 @@ variables [normed_group E] [second_countable_topology E] [normed_space ℝ E] [c
 
 /-- The Bochner integral -/
 def integral (μ : measure α) (f : α → E) : E :=
-if hf : measurable f ∧ integrable f μ
-then (l1.of_fun f hf.1 hf.2).integral
-else 0
+if hf : integrable f μ then (l1.of_fun f hf).integral else 0
 
 notation `∫` binders `, ` r:(scoped:60 f, f) ` ∂` μ:70 := integral μ r
 notation `∫` binders `, ` r:(scoped:60 f, integral volume f) := r
@@ -953,19 +947,16 @@ open continuous_linear_map measure_theory.simple_func
 
 variables {f g : α → E} {μ : measure α}
 
-lemma integral_eq (f : α → E) (h₁ : measurable f) (h₂ : integrable f μ) :
-  ∫ a, f a ∂μ = (l1.of_fun f h₁ h₂).integral :=
-dif_pos ⟨h₁, h₂⟩
+lemma integral_eq (f : α → E) (hf : integrable f μ) :
+  ∫ a, f a ∂μ = (l1.of_fun f hf).integral :=
+dif_pos hf
 
 lemma l1.integral_eq_integral (f : α →₁[μ] E) : f.integral = ∫ a, f a ∂μ :=
 by rw [integral_eq, l1.of_fun_to_fun]
 
-lemma integral_undef (h : ¬ (measurable f ∧ integrable f μ)) : ∫ a, f a ∂μ = 0 :=
+lemma integral_undef (h : ¬ integrable f μ) : ∫ a, f a ∂μ = 0 :=
 dif_neg h
 
-lemma integral_non_integrable (h : ¬ integrable f μ) : ∫ a, f a ∂μ = 0 :=
-integral_undef $ not_and_of_not_right _ h
-
 lemma integral_non_measurable (h : ¬ measurable f) : ∫ a, f a ∂μ = 0 :=
 integral_undef $ not_and_of_not_left _ h
 
@@ -975,34 +966,31 @@ lemma integral_zero : ∫ a : α, (0:E) ∂μ = 0 :=
 by rw [integral_eq, l1.of_fun_zero, l1.integral_zero]
 variables {α E}
 
-lemma integral_add
-  (hfm : measurable f) (hfi : integrable f μ) (hgm : measurable g) (hgi : integrable g μ) :
+lemma integral_add (hf : integrable f μ) (hg : integrable g μ) :
   ∫ a, f a + g a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ :=
-by rw [integral_eq, integral_eq f hfm hfi, integral_eq g hgm hgi, ← l1.integral_add,
-  ← l1.of_fun_add]; refl
+by { rw [integral_eq, integral_eq f hf, integral_eq g hg, ← l1.integral_add, ← l1.of_fun_add],
+     refl }
 
 lemma integral_neg (f : α → E) : ∫ a, -f a ∂μ = - ∫ a, f a ∂μ :=
 begin
-  by_cases hf : measurable f ∧ integrable f μ,
-  { rw [integral_eq f hf.1 hf.2, integral_eq (λa, - f a) hf.1.neg hf.2.neg,
-      ← l1.integral_neg, ← l1.of_fun_neg], refl },
-  { rw [integral_undef hf, integral_undef, neg_zero],
-    exact mt (and.imp measurable.of_neg integrable_neg_iff.1) hf }
+  by_cases hf : integrable f μ,
+  { rw [integral_eq f hf, integral_eq (λa, - f a) hf.neg, ← l1.integral_neg, ← l1.of_fun_neg],
+    refl },
+  { rw [integral_undef hf, integral_undef, neg_zero], rwa [← integrable_neg_iff] at hf }
 end
 
-lemma integral_sub
-  (hfm : measurable f) (hfi : integrable f μ) (hgm : measurable g) (hgi : integrable g μ) :
+lemma integral_sub (hf : integrable f μ) (hg : integrable g μ) :
   ∫ a, f a - g a ∂μ = ∫ a, f a ∂μ - ∫ a, g a ∂μ :=
-by { rw [sub_eq_add_neg, ← integral_neg], exact integral_add hfm hfi hgm.neg hgi.neg }
+by { rw [sub_eq_add_neg, ← integral_neg], exact integral_add hf hg.neg }
 
 lemma integral_smul (r : ℝ) (f : α → E) : ∫ a, r • (f a) ∂μ = r • ∫ a, f a ∂μ :=
 begin
-  by_cases hf : measurable f ∧ integrable f μ,
-  { rw [integral_eq f hf.1 hf.2, integral_eq (λa, r • (f a)), l1.of_fun_smul, l1.integral_smul] },
+  by_cases hf : integrable f μ,
+  { rw [integral_eq f hf, integral_eq (λa, r • (f a)), l1.of_fun_smul, l1.integral_smul] },
   { by_cases hr : r = 0,
     { simp only [hr, measure_theory.integral_zero, zero_smul] },
-    have hf' : ¬(measurable (λa, r • f a) ∧ integrable (r • f) μ),
-    { rwa [measurable_const_smul_iff hr, integrable_smul_iff hr f]; apply_instance },
+    have hf' : ¬ integrable (λ x, r • f x) μ,
+    { change ¬ integrable (r • f) μ, rwa [integrable_smul_iff hr f] },
     rw [integral_undef hf, integral_undef hf', smul_zero] }
 end
 
@@ -1019,15 +1007,15 @@ lemma integral_congr_ae (hfm : measurable f) (hgm : measurable g) (h : f =ᵐ[μ
    ∫ a, f a ∂μ = ∫ a, g a ∂μ :=
 begin
   by_cases hfi : integrable f μ,
-  { have hgi : integrable g μ := hfi.congr h,
-    rw [integral_eq f hfm hfi, integral_eq g hgm hgi, (l1.of_fun_eq_of_fun f g hfm hfi hgm hgi).2 h] },
-  { have hgi : ¬ integrable g μ, { rw integrable_congr h at hfi, exact hfi },
-    rw [integral_non_integrable hfi, integral_non_integrable hgi] },
+  { have hgi : integrable g μ := hfi.congr hgm h,
+    rw [integral_eq f hfi, integral_eq g hgi, (l1.of_fun_eq_of_fun f g hfi hgi).2 h] },
+  { have hgi : ¬ integrable g μ, { rw integrable_congr hfm hgm h at hfi, exact hfi },
+    rw [integral_undef hfi, integral_undef hgi] },
 end
 
-@[simp] lemma l1.integral_of_fun_eq_integral {f : α → E} (f_m : measurable f) (f_i : integrable f μ) :
-  ∫ a, (l1.of_fun f f_m f_i) a ∂μ = ∫ a, f a ∂μ :=
-integral_congr_ae (l1.measurable _) f_m (l1.to_fun_of_fun f f_m f_i)
+@[simp] lemma l1.integral_of_fun_eq_integral {f : α → E} (hf : integrable f μ) :
+  ∫ a, (l1.of_fun f hf) a ∂μ = ∫ a, f a ∂μ :=
+integral_congr_ae (l1.measurable _) hf.measurable (l1.to_fun_of_fun f hf)
 
 @[continuity]
 lemma continuous_integral : continuous (λ (f : α →₁[μ] E), ∫ a, f a ∂μ) :=
@@ -1040,11 +1028,9 @@ end
 lemma norm_integral_le_lintegral_norm (f : α → E) :
   ∥∫ a, f a ∂μ∥ ≤ ennreal.to_real (∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ) :=
 begin
-  by_cases hf : measurable f ∧ integrable f μ,
-  { rw [integral_eq f hf.1 hf.2, ← l1.norm_of_fun_eq_lintegral_norm f hf.1 hf.2],
-    exact l1.norm_integral_le _ },
-  { rw [integral_undef hf, norm_zero],
-    exact to_real_nonneg }
+  by_cases hf : integrable f μ,
+  { rw [integral_eq f hf, ← l1.norm_of_fun_eq_lintegral_norm f hf], exact l1.norm_integral_le _ },
+  { rw [integral_undef hf, norm_zero], exact to_real_nonneg }
 end
 
 lemma integral_eq_zero_of_ae {f : α → E} (hf : f =ᵐ[μ] 0) : ∫ a, f a ∂μ = 0 :=
@@ -1052,17 +1038,16 @@ if hfm : measurable f then by simp [integral_congr_ae hfm measurable_zero hf]
 else integral_non_measurable hfm
 
 /-- If `F i → f` in `L1`, then `∫ x, F i x ∂μ → ∫ x, f x∂μ`. -/
-lemma tendsto_integral_of_l1 {ι} (f : α → E) (hfm : measurable f) (hfi : integrable f μ)
-  {F : ι → α → E} {l : filter ι} (hFm : ∀ᶠ i in l, measurable (F i))
-  (hFi : ∀ᶠ i in l, integrable (F i) μ)
+lemma tendsto_integral_of_l1 {ι} (f : α → E) (hfi : integrable f μ)
+  {F : ι → α → E} {l : filter ι} (hFi : ∀ᶠ i in l, integrable (F i) μ)
   (hF : tendsto (λ i, ∫⁻ x, edist (F i x) (f x) ∂μ) l (𝓝 0)) :
   tendsto (λ i, ∫ x, F i x ∂μ) l (𝓝 $ ∫ x, f x ∂μ) :=
 begin
   rw [tendsto_iff_norm_tendsto_zero],
   replace hF : tendsto (λ i, ennreal.to_real $ ∫⁻ x, edist (F i x) (f x) ∂μ) l (𝓝 0) :=
     (ennreal.tendsto_to_real zero_ne_top).comp hF,
-  refine squeeze_zero_norm' (hFm.mp $ hFi.mono $ λ i hFi hFm, _) hF,
-  simp only [norm_norm, ← integral_sub hFm hFi hfm hfi, edist_dist, dist_eq_norm],
+  refine squeeze_zero_norm' (hFi.mp $ hFi.mono $ λ i hFi hFm, _) hF,
+  simp only [norm_norm, ← integral_sub hFi hfi, edist_dist, dist_eq_norm],
   apply norm_integral_le_lintegral_norm
 end
 
@@ -1084,14 +1069,16 @@ begin
     tendsto (λn, ennreal.to_real $ ∫⁻ a, (ennreal.of_real ∥F n a - f a∥) ∂μ) at_top (𝓝 0) :=
   (tendsto_to_real zero_ne_top).comp
     (tendsto_lintegral_norm_of_dominated_convergence
-      F_measurable f_measurable bound_integrable h_bound h_lim),
+      F_measurable f_measurable bound_integrable.has_finite_integral h_bound h_lim),
   -- Use the sandwich theorem
   refine squeeze_zero (λ n, norm_nonneg _) _ lintegral_norm_tendsto_zero,
   -- Show `∥∫ a, F n a - ∫ f∥ ≤ ∫ a, ∥F n a - f a∥` for all `n`
   { assume n,
-    have h₁ : integrable (F n) μ := bound_integrable.mono' (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₂,
+    have h₁ : integrable (F n) μ := bound_integrable.mono' (F_measurable n) (h_bound _),
+    have h₂ : integrable f μ :=
+    ⟨f_measurable, has_finite_integral_of_dominated_convergence
+      bound_integrable.has_finite_integral h_bound h_lim⟩,
+    rw ← integral_sub h₁ h₂,
     exact norm_integral_le_lintegral_norm _ }
 end
 
@@ -1130,18 +1117,18 @@ end
 
 /-- The Bochner integral of a real-valued function `f : α → ℝ` is the difference between the
   integral of the positive part of `f` and the integral of the negative part of `f`.  -/
-lemma integral_eq_lintegral_max_sub_lintegral_min {f : α → ℝ}
-  (hfm : measurable f) (hfi : integrable f μ) : ∫ a, f a ∂μ =
+lemma integral_eq_lintegral_max_sub_lintegral_min {f : α → ℝ} (hf : integrable f μ) :
+  ∫ a, f a ∂μ =
   ennreal.to_real (∫⁻ a, (ennreal.of_real $ max (f a) 0) ∂μ) -
   ennreal.to_real (∫⁻ a, (ennreal.of_real $ - min (f a) 0) ∂μ) :=
-let f₁ : α →₁[μ] ℝ := l1.of_fun f hfm hfi in
+let f₁ : α →₁[μ] ℝ := l1.of_fun f hf in
 -- Go to the `L¹` space
 have eq₁ : ennreal.to_real (∫⁻ a, (ennreal.of_real $ max (f a) 0) ∂μ) = ∥l1.pos_part f₁∥ :=
 begin
   rw l1.norm_eq_norm_to_fun,
   congr' 1,
   apply lintegral_congr_ae,
-  filter_upwards [l1.pos_part_to_fun f₁, l1.to_fun_of_fun f hfm hfi],
+  filter_upwards [l1.pos_part_to_fun f₁, l1.to_fun_of_fun f hf],
   simp only [mem_set_of_eq],
   assume a h₁ h₂,
   rw [h₁, h₂, real.norm_eq_abs, abs_of_nonneg],
@@ -1153,7 +1140,7 @@ begin
   rw l1.norm_eq_norm_to_fun,
   congr' 1,
   apply lintegral_congr_ae,
-  filter_upwards [l1.neg_part_to_fun_eq_min f₁, l1.to_fun_of_fun f hfm hfi],
+  filter_upwards [l1.neg_part_to_fun_eq_min f₁, l1.to_fun_of_fun f hf],
   simp only [mem_set_of_eq],
   assume a h₁ h₂,
   rw [h₁, h₂, real.norm_eq_abs, abs_of_nonneg],
@@ -1162,15 +1149,14 @@ begin
 end,
 begin
   rw [eq₁, eq₂, integral, dif_pos],
-  exact l1.integral_eq_norm_pos_part_sub _,
-  { exact ⟨hfm, hfi⟩ }
+  exact l1.integral_eq_norm_pos_part_sub _
 end
 
 lemma integral_eq_lintegral_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfm : measurable f) :
   ∫ a, f a ∂μ = ennreal.to_real (∫⁻ a, (ennreal.of_real $ f a) ∂μ) :=
 begin
   by_cases hfi : integrable f μ,
-  { rw integral_eq_lintegral_max_sub_lintegral_min hfm hfi,
+  { rw integral_eq_lintegral_max_sub_lintegral_min hfi,
     have h_min : ∫⁻ a, ennreal.of_real (-min (f a) 0) ∂μ = 0,
     { rw lintegral_eq_zero_iff,
       { refine hf.mono _,
@@ -1183,8 +1169,9 @@ begin
       rw [pi.zero_apply] at h,
       rw max_eq_left h },
     rw [h_min, h_max, zero_to_real, _root_.sub_zero] },
-  { rw integral_non_integrable hfi,
-    rw [integrable_iff_norm, lt_top_iff_ne_top, ne.def, not_not] at hfi,
+  { rw integral_undef hfi,
+    simp_rw [integrable, hfm, has_finite_integral_iff_norm, lt_top_iff_ne_top, ne.def, true_and,
+      not_not] at hfi,
     have : ∫⁻ (a : α), ennreal.of_real (f a) ∂μ = ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ,
     { refine lintegral_congr_ae (hf.mono $ assume a h, _),
       rw [real.norm_eq_abs, abs_of_nonneg h] },
@@ -1214,30 +1201,29 @@ by rw [l1.norm_eq_norm_to_fun,
        integral_eq_lintegral_of_nonneg_ae (eventually_of_forall $ by simp [norm_nonneg])
        (continuous_norm.measurable.comp f.measurable)]
 
-lemma l1.norm_of_fun_eq_integral_norm {f : α → H} (f_m : measurable f) (f_i : integrable f μ) :
-  ∥l1.of_fun f f_m f_i∥ = ∫ a, ∥f a∥ ∂μ :=
+lemma l1.norm_of_fun_eq_integral_norm {f : α → H} (hf : integrable f μ) :
+  ∥ l1.of_fun f hf ∥ = ∫ a, ∥f a∥ ∂μ :=
 begin
   rw l1.norm_eq_integral_norm,
-  refine integral_congr_ae (l1.measurable_norm _) f_m.norm _,
-  apply (l1.to_fun_of_fun f f_m f_i).mono,
+  refine integral_congr_ae (l1.measurable_norm _) hf.measurable.norm _,
+  apply (l1.to_fun_of_fun f hf).mono,
   intros a ha,
   simp [ha]
 end
 
 end normed_group
 
-lemma integral_mono {f g : α → ℝ} (hfm : measurable f) (hfi : integrable f μ)
-  (hgm : measurable g) (hgi : integrable g μ) (h : f ≤ᵐ[μ] g) : ∫ a, f a ∂μ ≤ ∫ a, g a ∂μ :=
-le_of_sub_nonneg $ integral_sub hgm hgi hfm hfi ▸
+lemma integral_mono {f g : α → ℝ} (hf : integrable f μ) (hg : integrable g μ) (h : f ≤ᵐ[μ] g) :
+  ∫ a, f a ∂μ ≤ ∫ a, g a ∂μ :=
+le_of_sub_nonneg $ integral_sub hg hf ▸
   integral_nonneg_of_ae $ h.mono (λ a, sub_nonneg_of_le)
 
-lemma integral_mono_of_nonneg {f g : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hgm : measurable g)
-  (hgi : integrable g μ) (h : f ≤ᵐ[μ] g) :
-  ∫ a, f a ∂μ ≤ ∫ a, g a ∂μ :=
+lemma integral_mono_of_nonneg {f g : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hgi : integrable g μ)
+  (h : f ≤ᵐ[μ] g) : ∫ a, f a ∂μ ≤ ∫ a, g a ∂μ :=
 begin
   by_cases hfm : measurable f,
-  { refine integral_mono hfm _ hgm hgi h,
-    refine (hgi.mono $ h.mp $ hf.mono $ λ x hf hfg, _),
+  { refine integral_mono ⟨hfm, _⟩ hgi h,
+    refine (hgi.has_finite_integral.mono $ h.mp $ hf.mono $ λ x hf hfg, _),
     simpa [real.norm_eq_abs, abs_of_nonneg hf, abs_of_nonneg (le_trans hf hfg)] },
   { rw [integral_non_measurable hfm],
     exact integral_nonneg_of_ae (hf.trans h) }
@@ -1255,29 +1241,26 @@ classical.by_cases
     exact integral_nonneg_of_ae le_ae
   end )
 
-lemma norm_integral_le_of_norm_le {f : α → E} {g : α → ℝ}
-  (hgm : measurable g) (hgi : integrable g μ) (h : ∀ᵐ x ∂μ, ∥f x∥ ≤ g x) :
-  ∥∫ x, f x ∂μ∥ ≤ ∫ x, g x ∂μ :=
+lemma norm_integral_le_of_norm_le {f : α → E} {g : α → ℝ} (hg : integrable g μ)
+  (h : ∀ᵐ x ∂μ, ∥f x∥ ≤ g x) : ∥∫ x, f x ∂μ∥ ≤ ∫ x, g x ∂μ :=
 calc ∥∫ x, f x ∂μ∥ ≤ ∫ x, ∥f x∥ ∂μ : norm_integral_le_integral_norm f
                ... ≤ ∫ x, g x ∂μ   :
-  integral_mono_of_nonneg (eventually_of_forall $ λ x, norm_nonneg _) hgm hgi h
+  integral_mono_of_nonneg (eventually_of_forall $ λ x, norm_nonneg _) hg h
 
-lemma integral_finset_sum {ι} (s : finset ι) {f : ι → α → E}
-  (hfm : ∀ i, measurable (f i)) (hfi : ∀ i, integrable (f i) μ) :
+lemma integral_finset_sum {ι} (s : finset ι) {f : ι → α → E} (hf : ∀ i, integrable (f i) μ) :
   ∫ a, ∑ i in s, f i a ∂μ = ∑ i in s, ∫ a, f i a ∂μ :=
 begin
   refine finset.induction_on s _ _,
   { simp only [integral_zero, finset.sum_empty] },
   { assume i s his ih,
     simp only [his, finset.sum_insert, not_false_iff],
-    rw [integral_add (hfm _) (hfi _) (s.measurable_sum hfm)
-        (integrable_finset_sum s hfm hfi), ih] }
+    rw [integral_add (hf _) (integrable_finset_sum s hf), ih] }
 end
 
 lemma simple_func.integral_eq_integral (f : α →ₛ E) (hfi : integrable f μ) :
   f.integral μ = ∫ x, f x ∂μ :=
 begin
-  rw [integral_eq f f.measurable hfi, ← l1.simple_func.of_simple_func_eq_of_fun,
+  rw [integral_eq f hfi, ← l1.simple_func.of_simple_func_eq_of_fun,
     l1.simple_func.integral_l1_eq_integral, l1.simple_func.integral_eq_integral],
   exact simple_func.integral_congr hfi (l1.simple_func.to_simple_func_of_simple_func _ _).symm
 end
@@ -1299,37 +1282,34 @@ begin
       { simp only [integrable_const_iff, not_or_distrib],
         exact ⟨hc, hμ⟩ },
       simp only [not_lt, top_le_iff] at hμ,
-      simp [integral_non_integrable, *] } }
+      simp [integral_undef, *] } }
 end
 
 lemma norm_integral_le_of_norm_le_const [finite_measure μ] {f : α → E} {C : ℝ}
   (h : ∀ᵐ x ∂μ, ∥f x∥ ≤ C) :
   ∥∫ x, f x ∂μ∥ ≤ C * (μ univ).to_real :=
-calc ∥∫ x, f x ∂μ∥ ≤ ∫ x, C ∂μ : norm_integral_le_of_norm_le measurable_const (integrable_const C) h
+calc ∥∫ x, f x ∂μ∥ ≤ ∫ x, C ∂μ : norm_integral_le_of_norm_le (integrable_const C) h
                ... = C * (μ univ).to_real : by rw [integral_const, smul_eq_mul, mul_comm]
 
 variable {ν : measure α}
 
-lemma integral_add_measure {f : α → E} (hμ : integrable f μ) (hν : integrable f ν) :
+lemma integral_add_measure' {f : α → E} (hμ : has_finite_integral f μ) (hν : has_finite_integral f ν) :
   ∫ x, f x ∂(μ + ν) = ∫ x, f x ∂μ + ∫ x, f x ∂ν :=
 begin
   by_cases hfm : measurable f; [skip, by simp only [integral_non_measurable hfm, zero_add]],
   have hfi := hμ.add_measure hν,
-  rcases simple_func_sequence_tendsto' hfm hfi with ⟨F, hFi, hFt⟩,
+  rcases simple_func_sequence_tendsto' ⟨hfm, hfi⟩ with ⟨F, hFi, hFt⟩,
   have hFiμ : ∀ i, integrable (F i) μ := λ i, (hFi i).left_of_add_measure,
   have hFiν : ∀ i, integrable (F i) ν := λ i, (hFi i).right_of_add_measure,
   simp only [← edist_nndist] at hFt,
   have hμν : tendsto (λ i, ∫ x, F i x ∂(μ + ν)) at_top (𝓝 ∫ x, f x ∂(μ + ν)) :=
-    tendsto_integral_of_l1 _ hfm hfi (eventually_of_forall $ λ i, (F i).measurable)
-      (eventually_of_forall hFi) hFt,
+    tendsto_integral_of_l1 _ ⟨hfm, hfi⟩ (eventually_of_forall hFi) hFt,
   have hμ : tendsto (λ i, ∫ x, F i x ∂μ) at_top (𝓝 ∫ x, f x ∂μ),
-  { refine tendsto_integral_of_l1 _ hfm hμ (eventually_of_forall $ λ i, (F i).measurable)
-      (eventually_of_forall hFiμ) _,
+  { refine tendsto_integral_of_l1 _ ⟨hfm, hμ⟩ (eventually_of_forall hFiμ) _,
     refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hFt (λ _, zero_le _) _,
     exact λ i, lintegral_mono' (measure.le_add_right $ le_refl μ) (le_refl _) },
   have hν : tendsto (λ i, ∫ x, F i x ∂ν) at_top (𝓝 ∫ x, f x ∂ν),
-  { refine tendsto_integral_of_l1 _ hfm hν (eventually_of_forall $ λ i, (F i).measurable)
-      (eventually_of_forall hFiν) _,
+  { refine tendsto_integral_of_l1 _ ⟨hfm, hν⟩ (eventually_of_forall hFiν) _,
     refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hFt (λ _, zero_le _) _,
     exact λ i, lintegral_mono' (measure.le_add_left $ le_refl ν) (le_refl _) },
   apply tendsto_nhds_unique hμν,
@@ -1337,6 +1317,10 @@ begin
     using hμ.add hν
 end
 
+lemma integral_add_measure {f : α → E} (hμ : integrable f μ) (hν : integrable f ν) :
+  ∫ x, f x ∂(μ + ν) = ∫ x, f x ∂μ + ∫ x, f x ∂ν :=
+integral_add_measure' hμ.has_finite_integral hν.has_finite_integral
+
 @[simp] lemma integral_zero_measure (f : α → E) : ∫ x, f x ∂0 = 0 :=
 norm_le_zero_iff.1 $ le_trans (norm_integral_le_lintegral_norm f) $ by simp
 
@@ -1354,31 +1338,30 @@ begin
     by_cases hf : f =ᵐ[μ] 0,
     { have : f =ᵐ[⊤ • μ] 0 := ae_smul_measure hf ⊤,
       exact integral_eq_zero_of_ae this },
-    { apply integral_non_integrable,
-      rw [integrable, lintegral_smul_measure, top_mul, if_neg],
+    { apply integral_undef,
+      rw [integrable, has_finite_integral, iff_true_intro hfm, true_and, lintegral_smul_measure,
+        top_mul, if_neg],
       { apply lt_irrefl },
       { rw [lintegral_eq_zero_iff hfm.ennnorm],
         refine λ h, hf (h.mono $ λ x, _),
         simp } } },
-  -- `f` is not integrable
+  -- `f` is not integrable and `0 < c < ⊤`
   by_cases hfi : integrable f μ, swap,
-  { rw [integral_non_integrable hfi, smul_zero],
-    refine integral_non_integrable (mt (λ h, _) hfi),
+  { rw [integral_undef hfi, smul_zero],
+    refine integral_undef (mt (λ h, _) hfi),
     convert h.smul_measure (ennreal.inv_lt_top.2 h0),
     rw [smul_smul, ennreal.inv_mul_cancel (ne_of_gt h0) (ne_of_lt hc), one_smul] },
-  -- Main case: `0 < c < ⊤`, `f` is measurable and integrable
-  rcases simple_func_sequence_tendsto' hfm hfi with ⟨F, hFi, hFt⟩,
+  -- Main case: `0 < c < ⊤`, `f` is integrable
+  rcases simple_func_sequence_tendsto' hfi with ⟨F, hFi, hFt⟩,
   have hFi' := λ n, (hFi n).smul_measure hc,
   simp only [← edist_nndist] at hFt,
   have hμ : tendsto (λ i, ∫ x, F i x ∂μ) at_top (𝓝 ∫ x, f x ∂μ) :=
-    tendsto_integral_of_l1 _ hfm hfi (eventually_of_forall $ λ i, (F i).measurable)
-      (eventually_of_forall hFi) hFt,
+    tendsto_integral_of_l1 _ hfi (eventually_of_forall hFi) hFt,
   refine tendsto_nhds_unique _ (tendsto_const_nhds.smul hμ),
   replace hFt := ennreal.tendsto.mul (tendsto_const_nhds : tendsto (λ _, c) _ _)
     (or.inr ennreal.zero_ne_top) hFt (or.inr $ ne_of_lt hc),
   simp only [mul_zero, ← lintegral_smul_measure] at hFt,
-  convert tendsto_integral_of_l1 _ hfm (hfi.smul_measure hc)
-    (eventually_of_forall $ λ i, (F i).measurable) (eventually_of_forall hFi') hFt,
+  convert tendsto_integral_of_l1 _ (hfi.smul_measure hc) (eventually_of_forall hFi') hFt,
   ext1 n,
   simp only [← (F n).integral_eq_integral, hFi, hFi', simple_func.integral,
     measure.smul_apply, finset.smul_sum, smul_smul, ennreal.to_real_mul_to_real]
@@ -1389,20 +1372,17 @@ lemma integral_map_measure {β} [measurable_space β] {φ : α → β} (hφ : me
   ∫ y, f y ∂(measure.map φ μ) = ∫ x, f (φ x) ∂μ :=
 begin
   by_cases hfi : integrable f (measure.map φ μ), swap,
-  { rw [integral_non_integrable hfi, integral_non_integrable],
+  { rw [integral_undef hfi, integral_undef],
     rwa [← integrable_map_measure hφ hfm] },
-  rcases simple_func_sequence_tendsto' hfm hfi with ⟨F, hFi, hFt⟩,
+  rcases simple_func_sequence_tendsto' hfi with ⟨F, hFi, hFt⟩,
   simp only [← edist_nndist] at hFt,
   have hF : tendsto (λ i, ∫ x, F i x ∂(measure.map φ μ)) at_top (𝓝 ∫ x, f x ∂(measure.map φ μ)) :=
-    tendsto_integral_of_l1 _ hfm hfi (eventually_of_forall $ λ i, (F i).measurable)
-      (eventually_of_forall hFi) hFt,
+    tendsto_integral_of_l1 _ hfi (eventually_of_forall hFi) hFt,
   refine tendsto_nhds_unique hF _, clear hF,
   simp only [lintegral_map ((F _).measurable.edist hfm) hφ] at hFt,
   have hFi' := hFi,
   simp only [integrable_map_measure, hφ, hfm, (F _).measurable] at hfi hFi',
-  refine (tendsto_integral_of_l1 _ (hfm.comp hφ) hfi
-    (eventually_of_forall $ λ i, (F i).measurable.comp hφ)
-    (eventually_of_forall $ hFi') hFt).congr (λ n, _),
+  refine (tendsto_integral_of_l1 _ hfi (eventually_of_forall $ hFi') hFt).congr (λ n, _),
   rw [← simple_func.integral_eq_integral _ (hFi n), ← simple_func.coe_comp _ hφ,
     ← simple_func.integral_eq_integral ((F n).comp φ hφ) (hFi' n)],
   simp only [simple_func.integral, measure.map_apply, *, simple_func.is_measurable_preimage],
diff --git a/src/measure_theory/borel_space.lean b/src/measure_theory/borel_space.lean
index e7c95cc502e0b..2fc94674bb2d7 100644
--- a/src/measure_theory/borel_space.lean
+++ b/src/measure_theory/borel_space.lean
@@ -741,7 +741,7 @@ namespace continuous_linear_map
 
 variables [measurable_space α]
 variables {𝕜 : Type*} [normed_field 𝕜]
-variables {E : Type*} [normed_group E] [normed_space 𝕜 E] [measurable_space E] [borel_space E]
+variables {E : Type*} [normed_group E] [normed_space 𝕜 E] [measurable_space E] [opens_measurable_space E]
 variables {F : Type*} [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F]
 
 protected lemma measurable (L : E →L[𝕜] F) : measurable L :=
diff --git a/src/measure_theory/interval_integral.lean b/src/measure_theory/interval_integral.lean
index 4ecb4747e467b..94b22c794708c 100644
--- a/src/measure_theory/interval_integral.lean
+++ b/src/measure_theory/interval_integral.lean
@@ -15,7 +15,7 @@ and `-∫ x in Ioc b a, f x ∂μ` if `b ≤ a`. We prove a few simple propertie
 of the first part of the
 [fundamental theorem of calculus](https://en.wikipedia.org/wiki/Fundamental_theorem_of_calculus).
 Recall that it states that the function `(u, v) ↦ ∫ x in u..v, f x` has derivative
-`(δu, δv) ↦ δv • f b - δu • f a` at `(a, b)` provided that `f` is continuous at `a` and `b`. 
+`(δu, δv) ↦ δv • f b - δu • f a` at `(a, b)` provided that `f` is continuous at `a` and `b`.
 
 ## Main statements
 
@@ -129,7 +129,8 @@ open measure_theory set classical filter
 
 open_locale classical topological_space filter
 
-variables {α β 𝕜 E F : Type*} [decidable_linear_order α] [measurable_space α] [normed_group E]
+variables {α β 𝕜 E F : Type*} [decidable_linear_order α] [measurable_space α]
+  [measurable_space E] [normed_group E]
 
 /-!
 ### Integrability at an interval
@@ -151,8 +152,8 @@ variables {f : α → E} {a b c : α} {μ : measure α}
 @[symm] lemma symm (h : interval_integrable f μ a b) : interval_integrable f μ b a :=
 h.symm
 
-@[refl] lemma refl : interval_integrable f μ a a :=
-by split; simp
+@[refl] lemma refl (hf : measurable f) : interval_integrable f μ a a :=
+by split; simp [hf]
 
 @[trans] lemma trans  (hab : interval_integrable f μ a b)
   (hbc : interval_integrable f μ b c) :
@@ -160,27 +161,28 @@ by split; simp
 ⟨(hab.1.union hbc.1).mono_set Ioc_subset_Ioc_union_Ioc,
   (hbc.2.union hab.2).mono_set Ioc_subset_Ioc_union_Ioc⟩
 
-lemma neg (h : interval_integrable f μ a b) : interval_integrable (-f) μ a b :=
+lemma neg [borel_space E] (h : interval_integrable f μ a b) : interval_integrable (-f) μ a b :=
 ⟨h.1.neg, h.2.neg⟩
 
+protected lemma measurable (h : interval_integrable f μ a b) : measurable f :=
+h.1.measurable
+
 end
 
+variables [borel_space E] {f g : α → E} {a b : α} {μ : measure α}
+
 lemma smul [normed_field 𝕜] [normed_space 𝕜 E] {f : α → E} {a b : α} {μ : measure α}
   (h : interval_integrable f μ a b) (r : 𝕜) :
   interval_integrable (r • f) μ a b :=
 ⟨h.1.smul r, h.2.smul r⟩
 
-variables [measurable_space E] [opens_measurable_space E] {f g : α → E} {a b : α} {μ : measure α}
-
-lemma add (hfm : measurable f) (hfi : interval_integrable f μ a b)
-  (hgm : measurable g) (hgi : interval_integrable g μ a b) :
-  interval_integrable (f + g) μ a b :=
-⟨hfi.1.add hfm hgm hgi.1, hfi.2.add hfm hgm hgi.2⟩
+lemma add [second_countable_topology E] (hf : interval_integrable f μ a b)
+  (hg : interval_integrable g μ a b) : interval_integrable (f + g) μ a b :=
+⟨hf.1.add hg.1, hf.2.add hg.2⟩
 
-lemma sub (hfm : measurable f) (hfi : interval_integrable f μ a b)
-  (hgm : measurable g) (hgi : interval_integrable g μ a b) :
-  interval_integrable (f - g) μ a b :=
-⟨hfi.1.sub hfm hgm hgi.1, hfi.2.sub hfm hgm hgi.2⟩
+lemma sub [second_countable_topology E] (hf : interval_integrable f μ a b)
+  (hg : interval_integrable g μ a b) : interval_integrable (f - g) μ a b :=
+⟨hf.1.sub hg.1, hf.2.sub hg.2⟩
 
 end interval_integrable
 
@@ -193,12 +195,12 @@ Suppose that `f : α → E` has a finite limit at `l' ⊓ μ.ae`. Then `f` is in
 Typeclass instances allow Lean to find `l'` based on `l` but not vice versa, so
 `apply tendsto.eventually_interval_integrable_ae` will generate goals `filter α` and
 `tendsto_Ixx_class Ioc ?m_1 l'`. -/
-lemma filter.tendsto.eventually_interval_integrable_ae {f : α → E} {μ : measure α}
-  {l l' : filter α} [tendsto_Ixx_class Ioc l l'] [is_measurably_generated l']
+lemma filter.tendsto.eventually_interval_integrable_ae {f : α → E} (hfm : measurable f)
+  {μ : measure α} {l l' : filter α} [tendsto_Ixx_class Ioc l l'] [is_measurably_generated l']
   (hμ : μ.finite_at_filter l') {c : E} (hf : tendsto f (l' ⊓ μ.ae) (𝓝 c))
   {u v : β → α} {lt : filter β} (hu : tendsto u lt l) (hv : tendsto v lt l) :
   ∀ᶠ t in lt, interval_integrable f μ (u t) (v t) :=
-have _ := (hf.integrable_at_filter_ae hμ).eventually,
+have _ := (hf.integrable_at_filter_ae hfm hμ).eventually,
 ((hu.Ioc hv).eventually this).and $ (hv.Ioc hu).eventually this
 
 /-- Let `l'` be a measurably generated filter; let `l` be a of filter such that each `s ∈ l'`
@@ -210,12 +212,12 @@ provided that both `u` and `v` tend to `l`.
 Typeclass instances allow Lean to find `l'` based on `l` but not vice versa, so
 `apply tendsto.eventually_interval_integrable_ae` will generate goals `filter α` and
 `tendsto_Ixx_class Ioc ?m_1 l'`. -/
-lemma filter.tendsto.eventually_interval_integrable {f : α → E} {μ : measure α}
-  {l l' : filter α} [tendsto_Ixx_class Ioc l l'] [is_measurably_generated l']
+lemma filter.tendsto.eventually_interval_integrable {f : α → E} (hfm : measurable f)
+  {μ : measure α} {l l' : filter α} [tendsto_Ixx_class Ioc l l'] [is_measurably_generated l']
   (hμ : μ.finite_at_filter l') {c : E} (hf : tendsto f l' (𝓝 c))
   {u v : β → α} {lt : filter β} (hu : tendsto u lt l) (hv : tendsto v lt l) :
   ∀ᶠ t in lt, interval_integrable f μ (u t) (v t) :=
-(hf.mono_left inf_le_left).eventually_interval_integrable_ae hμ hu hv
+(hf.mono_left inf_le_left).eventually_interval_integrable_ae hfm hμ hu hv
 
 /-!
 ### Interval integral: definition and basic properties
@@ -225,7 +227,7 @@ and prove some basic properties.
 -/
 
 variables [second_countable_topology E] [complete_space E] [normed_space ℝ E]
-  [measurable_space E] [borel_space E]
+  [borel_space E]
 
 /-- The interval integral `∫ x in a..b, f x ∂μ` is defined
 as `∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ`. If `a ≤ b`, then it equals
@@ -291,25 +293,16 @@ lemma norm_integral_le_of_norm_le_const {a b C : ℝ} {f : ℝ → E}
   ∥∫ x in a..b, f x∥ ≤ C * abs (b - a) :=
 norm_integral_le_of_norm_le_const_ae $ eventually_of_forall h
 
-lemma integral_add (hfm : measurable f) (hfi : interval_integrable f μ a b)
-  (hgm : measurable g) (hgi : interval_integrable g μ a b) :
+lemma integral_add (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) :
   ∫ x in a..b, f x + g x ∂μ = ∫ x in a..b, f x ∂μ + ∫ x in a..b, g x ∂μ :=
-begin
-  simp only [interval_integral, integral_add hfm hfi.1 hgm hgi.1,
-    integral_add hfm hfi.2 hgm hgi.2],
-  abel
-end
+by { simp only [interval_integral, integral_add hf.1 hg.1, integral_add hf.2 hg.2], abel }
 
 @[simp] lemma integral_neg : ∫ x in a..b, -f x ∂μ = -∫ x in a..b, f x ∂μ :=
-begin
-  simp only [interval_integral, integral_neg],
-  abel
-end
+by { simp only [interval_integral, integral_neg], abel }
 
-lemma integral_sub (hfm : measurable f) (hfi : interval_integrable f μ a b)
-  (hgm : measurable g) (hgi : interval_integrable g μ a b) :
+lemma integral_sub (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) :
   ∫ x in a..b, f x - g x ∂μ = ∫ x in a..b, f x ∂μ - ∫ x in a..b, g x ∂μ :=
-(integral_add hfm hfi hgm.neg hgi.neg).trans $ congr_arg _ integral_neg
+(integral_add hf hg.neg).trans $ congr_arg _ integral_neg
 
 lemma integral_smul (r : ℝ) : ∫ x in a..b, r • f x ∂μ = r • ∫ x in a..b, f x ∂μ :=
 by simp only [interval_integral, integral_smul, smul_sub]
@@ -403,8 +396,8 @@ by simp only [sub_eq_add_neg, ← integral_symm,
 lemma integral_interval_sub_interval_comm' (hab : interval_integrable f μ a b)
   (hcd : interval_integrable f μ c d) (hac : interval_integrable f μ a c) :
   ∫ x in a..b, f x ∂μ - ∫ x in c..d, f x ∂μ = ∫ x in d..b, f x ∂μ - ∫ x in c..a, f x ∂μ :=
-by rw [integral_interval_sub_interval_comm hab hcd hac, integral_symm b d, integral_symm a c,
-  sub_neg_eq_add, sub_eq_neg_add]
+by { rw [integral_interval_sub_interval_comm hab hcd hac, integral_symm b d, integral_symm a c,
+  sub_neg_eq_add, sub_eq_neg_add],  }
 
 lemma integral_Iic_sub_Iic (ha : integrable_on f (Iic a) μ) (hb : integrable_on f (Iic b) μ) :
   ∫ x in Iic b, f x ∂μ - ∫ x in Iic a, f x ∂μ = ∫ x in a..b, f x ∂μ :=
@@ -665,7 +658,7 @@ Then `∫ x in va..vb, f x ∂μ - ∫ x in ua..ub, f x ∂μ =
 as `ua` and `va` tend to `la` while `ub` and `vb` tend to `lb`.
 -/
 lemma measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae
-  (hfm : measurable f) (hab : interval_integrable f μ a b)
+  (hab : interval_integrable f μ a b)
   (ha_lim : tendsto f (la' ⊓ μ.ae) (𝓝 ca)) (hb_lim : tendsto f (lb' ⊓ μ.ae) (𝓝 cb))
   (hua : tendsto ua lt la) (hva : tendsto va lt la)
   (hub : tendsto ub lt lb) (hvb : tendsto vb lt lb) :
@@ -674,18 +667,18 @@ lemma measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae
     (λ t, ∥∫ x in ua t..va t, (1:ℝ) ∂μ∥ + ∥∫ x in ub t..vb t, (1:ℝ) ∂μ∥) lt :=
 begin
   refine
-    ((measure_integral_sub_linear_is_o_of_tendsto_ae hfm ha_lim hua hva).neg_left.add_add
-    (measure_integral_sub_linear_is_o_of_tendsto_ae hfm hb_lim hub hvb)).congr'
+    ((measure_integral_sub_linear_is_o_of_tendsto_ae hab.measurable ha_lim hua hva).neg_left.add_add
+    (measure_integral_sub_linear_is_o_of_tendsto_ae hab.measurable hb_lim hub hvb)).congr'
       _ (eventually_eq.refl _ _),
   have A : ∀ᶠ t in lt, interval_integrable f μ (ua t) (va t) :=
-    ha_lim.eventually_interval_integrable_ae (FTC_filter.finite_at_inner la) hua hva,
+    ha_lim.eventually_interval_integrable_ae hab.measurable (FTC_filter.finite_at_inner la) hua hva,
   have A' : ∀ᶠ t in lt, interval_integrable f μ a (ua t) :=
-    ha_lim.eventually_interval_integrable_ae (FTC_filter.finite_at_inner la)
+    ha_lim.eventually_interval_integrable_ae hab.measurable (FTC_filter.finite_at_inner la)
       (tendsto_const_pure.mono_right FTC_filter.pure_le) hua,
   have B : ∀ᶠ t in lt, interval_integrable f μ (ub t) (vb t) :=
-    hb_lim.eventually_interval_integrable_ae (FTC_filter.finite_at_inner lb) hub hvb,
+    hb_lim.eventually_interval_integrable_ae hab.measurable (FTC_filter.finite_at_inner lb) hub hvb,
   have B' : ∀ᶠ t in lt, interval_integrable f μ b (ub t) :=
-    hb_lim.eventually_interval_integrable_ae (FTC_filter.finite_at_inner lb)
+    hb_lim.eventually_interval_integrable_ae hab.measurable (FTC_filter.finite_at_inner lb)
       (tendsto_const_pure.mono_right FTC_filter.pure_le) hub,
   filter_upwards [A, A', B, B'], simp only [mem_set_of_eq],
   intros t ua_va a_ua ub_vb b_ub,
@@ -704,12 +697,12 @@ Then `∫ x in a..v, f x ∂μ - ∫ x in a..u, f x ∂μ = ∫ x in u..v, c ∂
 as `u` and `v` tend to `lb`.
 -/
 lemma measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right
-  (hfm : measurable f) (hab : interval_integrable f μ a b)
-  (hf : tendsto f (lb' ⊓ μ.ae) (𝓝 c)) (hu : tendsto u lt lb) (hv : tendsto v lt lb) :
+  (hab : interval_integrable f μ a b) (hf : tendsto f (lb' ⊓ μ.ae) (𝓝 c))
+  (hu : tendsto u lt lb) (hv : tendsto v lt lb) :
   is_o (λ t, ∫ x in a..v t, f x ∂μ - ∫ x in a..u t, f x ∂μ - ∫ x in u t..v t, c ∂μ)
     (λ t, ∫ x in u t..v t, (1:ℝ) ∂μ) lt :=
 by simpa using measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae
-  hfm hab ((tendsto_bot : tendsto _ ⊥ (𝓝 0)).mono_left inf_le_left)
+  hab ((tendsto_bot : tendsto _ ⊥ (𝓝 0)).mono_left inf_le_left)
   hf (tendsto_const_pure : tendsto _ _ (pure a)) tendsto_const_pure hu hv
 
 /-- Fundamental theorem of calculus-1, strict derivative in left endpoint for a locally finite
@@ -722,12 +715,12 @@ Then `∫ x in v..b, f x ∂μ - ∫ x in u..b, f x ∂μ = -∫ x in u..v, c 
 as `u` and `v` tend to `la`.
 -/
 lemma measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_left
-  (hfm : measurable f) (hab : interval_integrable f μ a b)
+  (hab : interval_integrable f μ a b)
   (hf : tendsto f (la' ⊓ μ.ae) (𝓝 c)) (hu : tendsto u lt la) (hv : tendsto v lt la) :
   is_o (λ t, ∫ x in v t..b, f x ∂μ - ∫ x in u t..b, f x ∂μ + ∫ x in u t..v t, c ∂μ)
     (λ t, ∫ x in u t..v t, (1:ℝ) ∂μ) lt :=
 by simpa using measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae
-  hfm hab hf ((tendsto_bot : tendsto _ ⊥ (𝓝 0)).mono_left inf_le_left)
+  hab hf ((tendsto_bot : tendsto _ ⊥ (𝓝 0)).mono_left inf_le_left)
   hu hv (tendsto_const_pure : tendsto _ _ (pure b)) tendsto_const_pure
 
 end
@@ -770,14 +763,14 @@ almost surely at `la'` and `lb'`, respectively, then
 This lemma could've been formulated using `has_strict_fderiv_at_filter` if we had this
 definition. -/
 lemma integral_sub_integral_sub_linear_is_o_of_tendsto_ae
-  (hfm : measurable f) (hab : interval_integrable f volume a b)
+  (hab : interval_integrable f volume a b)
   (ha_lim : tendsto f (la' ⊓ volume.ae) (𝓝 ca)) (hb_lim : tendsto f (lb' ⊓ volume.ae) (𝓝 cb))
   (hua : tendsto ua lt la) (hva : tendsto va lt la)
   (hub : tendsto ub lt lb) (hvb : tendsto vb lt lb) :
   is_o (λ t, (∫ x in va t..vb t, f x) - (∫ x in ua t..ub t, f x) -
     ((vb t - ub t) • cb - (va t - ua t) • ca)) (λ t, ∥va t - ua t∥ + ∥vb t - ub t∥) lt :=
 by simpa [integral_const] using
-measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae hfm hab ha_lim hb_lim hua hva hub hvb
+measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae hab ha_lim hb_lim hua hva hub hvb
 
 /-- Fundamental theorem of calculus-1, strict differentiability at filter in both endpoints.
 If `f` is a measurable function integrable on `a..b`, `(lb, lb')` is an `FTC_filter` pair
@@ -786,12 +779,11 @@ around `b`, and `f` has a finite limit `c` almost surely at `lb'`, then
 
 This lemma could've been formulated using `has_strict_deriv_at_filter` if we had this definition. -/
 lemma integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right
-  (hfm : measurable f) (hab : interval_integrable f volume a b)
-  (hf : tendsto f (lb' ⊓ volume.ae) (𝓝 c))
+  (hab : interval_integrable f volume a b) (hf : tendsto f (lb' ⊓ volume.ae) (𝓝 c))
   (hu : tendsto u lt lb) (hv : tendsto v lt lb) :
   is_o (λ t, (∫ x in a..v t, f x) - (∫ x in a..u t, f x) - (v t - u t) • c) (v - u) lt :=
 by simpa only [integral_const, smul_eq_mul, mul_one] using
-  measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right hfm hab hf hu hv
+  measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right hab hf hu hv
 
 /-- Fundamental theorem of calculus-1, strict differentiability at filter in both endpoints.
 If `f` is a measurable function integrable on `a..b`, `(la, la')` is an `FTC_filter` pair
@@ -800,12 +792,11 @@ around `a`, and `f` has a finite limit `c` almost surely at `la'`, then
 
 This lemma could've been formulated using `has_strict_deriv_at_filter` if we had this definition. -/
 lemma integral_sub_integral_sub_linear_is_o_of_tendsto_ae_left
-  (hfm : measurable f) (hab : interval_integrable f volume a b)
-  (hf : tendsto f (la' ⊓ volume.ae) (𝓝 c))
+  (hab : interval_integrable f volume a b) (hf : tendsto f (la' ⊓ volume.ae) (𝓝 c))
   (hu : tendsto u lt la) (hv : tendsto v lt la) :
   is_o (λ t, (∫ x in v t..b, f x) - (∫ x in u t..b, f x) + (v t - u t) • c) (v - u) lt :=
 by simpa only [integral_const, smul_eq_mul, mul_one] using
-  measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_left hfm hab hf hu hv
+  measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_left hab hf hu hv
 
 open continuous_linear_map (fst snd smul_right sub_apply smul_right_apply coe_fst' coe_snd' map_sub)
 
@@ -842,13 +833,12 @@ In this section we prove that for a measurable function `f` integrable on `a..b`
 limits `ca` and `cb` almost surely as `x` tends to `a` and `b`, respectively, then
 `(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)`
 in the sense of strict differentiability. -/
-lemma integral_has_strict_fderiv_at_of_tendsto_ae (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 ca))
-  (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 cb)) :
+lemma integral_has_strict_fderiv_at_of_tendsto_ae (hf : interval_integrable f volume a b)
+  (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 ca)) (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 cb)) :
   has_strict_fderiv_at (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x)
     ((snd ℝ ℝ ℝ).smul_right cb - (fst ℝ ℝ ℝ).smul_right ca) (a, b) :=
 begin
-  have := integral_sub_integral_sub_linear_is_o_of_tendsto_ae hfm hfi ha hb
+  have := integral_sub_integral_sub_linear_is_o_of_tendsto_ae hf ha hb
     ((continuous_fst.comp continuous_snd).tendsto ((a, b), (a, b)))
     ((continuous_fst.comp continuous_fst).tendsto ((a, b), (a, b)))
     ((continuous_snd.comp continuous_snd).tendsto ((a, b), (a, b)))
@@ -861,46 +851,42 @@ end
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous
 at `a` and `b`, then `(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca`
 at `(a, b)` in the sense of strict differentiability. -/
-lemma integral_has_strict_fderiv_at (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (ha : continuous_at f a) (hb : continuous_at f b) :
+lemma integral_has_strict_fderiv_at (hf : interval_integrable f volume a b)
+  (ha : continuous_at f a) (hb : continuous_at f b) :
   has_strict_fderiv_at (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x)
     ((snd ℝ ℝ ℝ).smul_right (f b) - (fst ℝ ℝ ℝ).smul_right (f a)) (a, b) :=
-integral_has_strict_fderiv_at_of_tendsto_ae hfm hfi
+integral_has_strict_fderiv_at_of_tendsto_ae hf
   (ha.mono_left inf_le_left) (hb.mono_left inf_le_left)
 
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
 limit `c` almost surely at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `c` at `b` in the sense
 of strict differentiability. -/
-lemma integral_has_strict_deriv_at_of_tendsto_ae_right (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 c)) :
-  has_strict_deriv_at (λ u, ∫ x in a..u, f x) c b :=
-integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right hfm hfi hb continuous_at_snd
+lemma integral_has_strict_deriv_at_of_tendsto_ae_right (hf : interval_integrable f volume a b)
+  (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 c)) : has_strict_deriv_at (λ u, ∫ x in a..u, f x) c b :=
+integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right hf hb continuous_at_snd
   continuous_at_fst
 
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous
 at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `f b` at `b` in the sense of strict
 differentiability. -/
-lemma integral_has_strict_deriv_at_right (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (hb : continuous_at f b) :
-  has_strict_deriv_at (λ u, ∫ x in a..u, f x) (f b) b :=
-integral_has_strict_deriv_at_of_tendsto_ae_right hfm hfi (hb.mono_left inf_le_left)
+lemma integral_has_strict_deriv_at_right (hf : interval_integrable f volume a b)
+  (hb : continuous_at f b) : has_strict_deriv_at (λ u, ∫ x in a..u, f x) (f b) b :=
+integral_has_strict_deriv_at_of_tendsto_ae_right hf (hb.mono_left inf_le_left)
 
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
 limit `c` almost surely at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-c` at `a` in the sense
 of strict differentiability. -/
-lemma integral_has_strict_deriv_at_of_tendsto_ae_left (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 c)) :
-  has_strict_deriv_at (λ u, ∫ x in u..b, f x) (-c) a :=
+lemma integral_has_strict_deriv_at_of_tendsto_ae_left (hf : interval_integrable f volume a b)
+  (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 c)) : has_strict_deriv_at (λ u, ∫ x in u..b, f x) (-c) a :=
 by simpa only [← integral_symm]
-  using (integral_has_strict_deriv_at_of_tendsto_ae_right hfm hfi.symm ha).neg
+  using (integral_has_strict_deriv_at_of_tendsto_ae_right hf.symm ha).neg
 
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous
 at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-f a` at `a` in the sense of strict
 differentiability. -/
-lemma integral_has_strict_deriv_at_left (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (ha : continuous_at f a) :
-  has_strict_deriv_at (λ u, ∫ x in u..b, f x) (-f a) a :=
-by simpa only [← integral_symm] using (integral_has_strict_deriv_at_right hfm hfi.symm ha).neg
+lemma integral_has_strict_deriv_at_left (hf : interval_integrable f volume a b)
+  (ha : continuous_at f a) : has_strict_deriv_at (λ u, ∫ x in u..b, f x) (-f a) a :=
+by simpa only [← integral_symm] using (integral_has_strict_deriv_at_right hf.symm ha).neg
 
 /-!
 #### Fréchet differentiability
@@ -912,96 +898,86 @@ In this subsection we restate results from the previous subsection in terms of `
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has finite
 limits `ca` and `cb` almost surely as `x` tends to `a` and `b`, respectively, then
 `(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)`. -/
-lemma integral_has_fderiv_at_of_tendsto_ae (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 ca))
-  (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 cb)) :
+lemma integral_has_fderiv_at_of_tendsto_ae (hf : interval_integrable f volume a b)
+  (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 ca)) (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 cb)) :
   has_fderiv_at (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x)
     ((snd ℝ ℝ ℝ).smul_right cb - (fst ℝ ℝ ℝ).smul_right ca) (a, b) :=
-(integral_has_strict_fderiv_at_of_tendsto_ae hfm hfi ha hb).has_fderiv_at
+(integral_has_strict_fderiv_at_of_tendsto_ae hf ha hb).has_fderiv_at
 
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous
 at `a` and `b`, then `(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca`
 at `(a, b)`. -/
-lemma integral_has_fderiv_at (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (ha : continuous_at f a) (hb : continuous_at f b) :
+lemma integral_has_fderiv_at (hf : interval_integrable f volume a b)
+  (ha : continuous_at f a) (hb : continuous_at f b) :
   has_fderiv_at (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x)
     ((snd ℝ ℝ ℝ).smul_right (f b) - (fst ℝ ℝ ℝ).smul_right (f a)) (a, b) :=
-(integral_has_strict_fderiv_at hfm hfi ha hb).has_fderiv_at
+(integral_has_strict_fderiv_at hf ha hb).has_fderiv_at
 
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has finite
 limits `ca` and `cb` almost surely as `x` tends to `a` and `b`, respectively, then `fderiv`
 derivative of `(u, v) ↦ ∫ x in u..v, f x` at `(a, b)` equals `(u, v) ↦ v • cb - u • ca`. -/
-lemma fderiv_integral_of_tendsto_ae (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 ca))
-  (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 cb)) :
+lemma fderiv_integral_of_tendsto_ae (hf : interval_integrable f volume a b)
+  (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 ca)) (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 cb)) :
   fderiv ℝ (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x) (a, b) =
     (snd ℝ ℝ ℝ).smul_right cb - (fst ℝ ℝ ℝ).smul_right ca :=
-(integral_has_fderiv_at_of_tendsto_ae hfm hfi ha hb).fderiv
+(integral_has_fderiv_at_of_tendsto_ae hf ha hb).fderiv
 
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous
 at `a` and `b`, then `fderiv` derivative of `(u, v) ↦ ∫ x in u..v, f x` at `(a, b)` equals `(u, v) ↦
 v • cb - u • ca`. -/
-lemma fderiv_integral (hfm : measurable f) (hfi : interval_integrable f volume a b)
+lemma fderiv_integral (hf : interval_integrable f volume a b)
   (ha : continuous_at f a) (hb : continuous_at f b) :
   fderiv ℝ (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x) (a, b) =
     (snd ℝ ℝ ℝ).smul_right (f b) - (fst ℝ ℝ ℝ).smul_right (f a) :=
-(integral_has_fderiv_at hfm hfi ha hb).fderiv
+(integral_has_fderiv_at hf ha hb).fderiv
 
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
 limit `c` almost surely at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `c` at `b`. -/
-lemma integral_has_deriv_at_of_tendsto_ae_right (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 c)) :
-  has_deriv_at (λ u, ∫ x in a..u, f x) c b :=
-(integral_has_strict_deriv_at_of_tendsto_ae_right hfm hfi hb).has_deriv_at
+lemma integral_has_deriv_at_of_tendsto_ae_right (hf : interval_integrable f volume a b)
+  (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 c)) : has_deriv_at (λ u, ∫ x in a..u, f x) c b :=
+(integral_has_strict_deriv_at_of_tendsto_ae_right hf hb).has_deriv_at
 
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous
 at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `f b` at `b`. -/
-lemma integral_has_deriv_at_right (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (hb : continuous_at f b) :
-  has_deriv_at (λ u, ∫ x in a..u, f x) (f b) b :=
-(integral_has_strict_deriv_at_right hfm hfi hb).has_deriv_at
+lemma integral_has_deriv_at_right (hf : interval_integrable f volume a b)
+  (hb : continuous_at f b) : has_deriv_at (λ u, ∫ x in a..u, f x) (f b) b :=
+(integral_has_strict_deriv_at_right hf hb).has_deriv_at
 
 /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` has a finite
 limit `c` almost surely at `b`, then the derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `c`. -/
-lemma deriv_integral_of_tendsto_ae_right (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 c)) :
-  deriv (λ u, ∫ x in a..u, f x) b = c :=
-(integral_has_deriv_at_of_tendsto_ae_right hfm hfi hb).deriv
+lemma deriv_integral_of_tendsto_ae_right (hf : interval_integrable f volume a b)
+  (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 c)) : deriv (λ u, ∫ x in a..u, f x) b = c :=
+(integral_has_deriv_at_of_tendsto_ae_right hf hb).deriv
 
 /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous
 at `b`, then the derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `f b`. -/
-lemma deriv_integral_right (hfm : measurable f) (hfi : interval_integrable f volume a b)
-  (hb : continuous_at f b) :
+lemma deriv_integral_right (hf : interval_integrable f volume a b) (hb : continuous_at f b) :
   deriv (λ u, ∫ x in a..u, f x) b = f b :=
-(integral_has_deriv_at_right hfm hfi hb).deriv
+(integral_has_deriv_at_right hf hb).deriv
 
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
 limit `c` almost surely at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-c` at `a`. -/
-lemma integral_has_deriv_at_of_tendsto_ae_left (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 c)) :
-  has_deriv_at (λ u, ∫ x in u..b, f x) (-c) a :=
-(integral_has_strict_deriv_at_of_tendsto_ae_left hfm hfi ha).has_deriv_at
+lemma integral_has_deriv_at_of_tendsto_ae_left (hf : interval_integrable f volume a b)
+  (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 c)) : has_deriv_at (λ u, ∫ x in u..b, f x) (-c) a :=
+(integral_has_strict_deriv_at_of_tendsto_ae_left hf ha).has_deriv_at
 
 /-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous
 at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-f a` at `a`. -/
-lemma integral_has_deriv_at_left (hfm : measurable f) (hfi : interval_integrable f volume a b)
-  (ha : continuous_at f a) :
+lemma integral_has_deriv_at_left (hf : interval_integrable f volume a b) (ha : continuous_at f a) :
   has_deriv_at (λ u, ∫ x in u..b, f x) (-f a) a :=
-(integral_has_strict_deriv_at_left hfm hfi ha).has_deriv_at
+(integral_has_strict_deriv_at_left hf ha).has_deriv_at
 
 /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` has a finite
 limit `c` almost surely at `a`, then the derivative of `u ↦ ∫ x in u..b, f x` at `a` equals `-c`. -/
-lemma deriv_integral_of_tendsto_ae_left (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) (hb : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 c)) :
-  deriv (λ u, ∫ x in u..b, f x) a = -c :=
-(integral_has_deriv_at_of_tendsto_ae_left hfm hfi hb).deriv
+lemma deriv_integral_of_tendsto_ae_left (hf : interval_integrable f volume a b)
+  (hb : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 c)) : deriv (λ u, ∫ x in u..b, f x) a = -c :=
+(integral_has_deriv_at_of_tendsto_ae_left hf hb).deriv
 
 /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous
 at `a`, then the derivative of `u ↦ ∫ x in u..b, f x` at `a` equals `-f a`. -/
-lemma deriv_integral_left (hfm : measurable f) (hfi : interval_integrable f volume a b)
-  (hb : continuous_at f a) :
+lemma deriv_integral_left (hf : interval_integrable f volume a b) (hb : continuous_at f a) :
   deriv (λ u, ∫ x in u..b, f x) a = -f a :=
-(integral_has_deriv_at_left hfm hfi hb).deriv
+(integral_has_deriv_at_left hf hb).deriv
 
 /-!
 #### One-sided derivatives
@@ -1019,15 +995,14 @@ and `cb` almost surely at the filters `la` and `lb` from the following table.
 | `{a}`   | `⊥`          | `{b}`   | `⊥`          |
 | `univ`  | `𝓝 a`        | `univ`  | `𝓝 b`        |
 -/
-lemma integral_has_fderiv_within_at_of_tendsto_ae (hfm : measurable f)
-  (hfi : interval_integrable f volume a b)
+lemma integral_has_fderiv_within_at_of_tendsto_ae (hf : interval_integrable f volume a b)
   {s t : set ℝ} [FTC_filter a (𝓝[s] a) la] [FTC_filter b (𝓝[t] b) lb]
   (ha : tendsto f (la ⊓ volume.ae) (𝓝 ca)) (hb : tendsto f (lb ⊓ volume.ae) (𝓝 cb)) :
   has_fderiv_within_at (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x)
     ((snd ℝ ℝ ℝ).smul_right cb - (fst ℝ ℝ ℝ).smul_right ca) (s.prod t) (a, b) :=
 begin
   rw [has_fderiv_within_at, nhds_within_prod_eq],
-  have := integral_sub_integral_sub_linear_is_o_of_tendsto_ae hfm hfi ha hb
+  have := integral_sub_integral_sub_linear_is_o_of_tendsto_ae hf ha hb
     (tendsto_const_pure.mono_right FTC_filter.pure_le : tendsto _ _ (𝓝[s] a)) tendsto_fst
     (tendsto_const_pure.mono_right FTC_filter.pure_le : tendsto _ _ (𝓝[t] b)) tendsto_snd,
   refine (this.congr_left _).trans_is_O _,
@@ -1048,12 +1023,12 @@ is definitionally equal `continuous_at f _` or `continuous_within_at f _ _`.
 | `{a}`   | `⊥`          | `{b}`   | `⊥`          |
 | `univ`  | `𝓝 a`        | `univ`  | `𝓝 b`        |
 -/
-lemma integral_has_fderiv_within_at (hfm : measurable f) (hfi : interval_integrable f volume a b)
+lemma integral_has_fderiv_within_at (hf : interval_integrable f volume a b)
   {s t : set ℝ} [FTC_filter a (𝓝[s] a) la] [FTC_filter b (𝓝[t] b) lb]
   (ha : tendsto f la (𝓝 $ f a)) (hb : tendsto f lb (𝓝 $ f b)) :
   has_fderiv_within_at (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x)
     ((snd ℝ ℝ ℝ).smul_right (f b) - (fst ℝ ℝ ℝ).smul_right (f a)) (s.prod t) (a, b) :=
-integral_has_fderiv_within_at_of_tendsto_ae hfm hfi (ha.mono_left inf_le_left)
+integral_has_fderiv_within_at_of_tendsto_ae hf (ha.mono_left inf_le_left)
   (hb.mono_left inf_le_left)
 
 /-- An auxiliary tactic closing goals `unique_diff_within_at ℝ s a` where
@@ -1074,90 +1049,83 @@ is equal to `(u, v) ↦ u • cb - v • ca`.
 | `univ`  | `𝓝 a`        | `univ`  | `𝓝 b`        |
 
 -/
-lemma fderiv_within_integral_of_tendsto_ae (hfm : measurable f)
-  (hfi : interval_integrable f volume a b)
+lemma fderiv_within_integral_of_tendsto_ae (hf : interval_integrable f volume a b)
   {s t : set ℝ} [FTC_filter a (𝓝[s] a) la] [FTC_filter b (𝓝[t] b) lb]
   (ha : tendsto f (la ⊓ volume.ae) (𝓝 ca)) (hb : tendsto f (lb ⊓ volume.ae) (𝓝 cb))
   (hs : unique_diff_within_at ℝ s a . unique_diff_within_at_Ici_Iic_univ)
   (ht : unique_diff_within_at ℝ t b . unique_diff_within_at_Ici_Iic_univ) :
   fderiv_within ℝ (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x) (s.prod t) (a, b) =
     ((snd ℝ ℝ ℝ).smul_right cb - (fst ℝ ℝ ℝ).smul_right ca) :=
-(integral_has_fderiv_within_at_of_tendsto_ae hfm hfi ha hb).fderiv_within $ hs.prod ht
+(integral_has_fderiv_within_at_of_tendsto_ae hf ha hb).fderiv_within $ hs.prod ht
 
 /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
 limit `c` almost surely as `x` tends to `b` from the right or from the left,
 then `u ↦ ∫ x in a..u, f x` has right (resp., left) derivative `c` at `b`. -/
-lemma integral_has_deriv_within_at_of_tendsto_ae_right (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) {s t : set ℝ} [FTC_filter b (𝓝[s] b) (𝓝[t] b)]
-  (hb : tendsto f (𝓝[t] b ⊓ volume.ae) (𝓝 c)) :
+lemma integral_has_deriv_within_at_of_tendsto_ae_right (hf : interval_integrable f volume a b)
+  {s t : set ℝ} [FTC_filter b (𝓝[s] b) (𝓝[t] b)] (hb : tendsto f (𝓝[t] b ⊓ volume.ae) (𝓝 c)) :
   has_deriv_within_at (λ u, ∫ x in a..u, f x) c s b :=
-integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right hfm hfi hb
+integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right hf hb
   (tendsto_const_pure.mono_right FTC_filter.pure_le) tendsto_id
 
 /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous
 from the left or from the right at `b`, then `u ↦ ∫ x in a..u, f x` has left (resp., right)
 derivative `f b` at `b`. -/
-lemma integral_has_deriv_within_at_right (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) {s t : set ℝ} [FTC_filter b (𝓝[s] b) (𝓝[t] b)]
-  (hb : continuous_within_at f t b) :
+lemma integral_has_deriv_within_at_right (hf : interval_integrable f volume a b)
+  {s t : set ℝ} [FTC_filter b (𝓝[s] b) (𝓝[t] b)] (hb : continuous_within_at f t b) :
   has_deriv_within_at (λ u, ∫ x in a..u, f x) (f b) s b :=
-integral_has_deriv_within_at_of_tendsto_ae_right hfm hfi (hb.mono_left inf_le_left)
+integral_has_deriv_within_at_of_tendsto_ae_right hf (hb.mono_left inf_le_left)
 
 /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
 limit `c` almost surely as `x` tends to `b` from the right or from the left, then the right
 (resp., left) derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `c`. -/
-lemma deriv_within_integral_of_tendsto_ae_right (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) {s t : set ℝ} [FTC_filter b (𝓝[s] b) (𝓝[t] b)]
-  (hb : tendsto f (𝓝[t] b ⊓ volume.ae) (𝓝 c))
+lemma deriv_within_integral_of_tendsto_ae_right (hf : interval_integrable f volume a b)
+  {s t : set ℝ} [FTC_filter b (𝓝[s] b) (𝓝[t] b)] (hb : tendsto f (𝓝[t] b ⊓ volume.ae) (𝓝 c))
   (hs : unique_diff_within_at ℝ s b . unique_diff_within_at_Ici_Iic_univ) :
   deriv_within (λ u, ∫ x in a..u, f x) s b = c :=
-(integral_has_deriv_within_at_of_tendsto_ae_right hfm hfi hb).deriv_within hs
+(integral_has_deriv_within_at_of_tendsto_ae_right hf hb).deriv_within hs
 
 /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous
 on the right or on the left at `b`, then the right (resp., left) derivative of
 `u ↦ ∫ x in a..u, f x` at `b` equals `f b`. -/
-lemma deriv_within_integral_right (hfm : measurable f) (hfi : interval_integrable f volume a b)
+lemma deriv_within_integral_right (hf : interval_integrable f volume a b)
   {s t : set ℝ} [FTC_filter b (𝓝[s] b) (𝓝[t] b)] (hb : continuous_within_at f t b)
   (hs : unique_diff_within_at ℝ s b . unique_diff_within_at_Ici_Iic_univ) :
   deriv_within (λ u, ∫ x in a..u, f x) s b = f b :=
-(integral_has_deriv_within_at_right hfm hfi hb).deriv_within hs
+(integral_has_deriv_within_at_right hf hb).deriv_within hs
 
 /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
 limit `c` almost surely as `x` tends to `a` from the right or from the left,
 then `u ↦ ∫ x in u..b, f x` has right (resp., left) derivative `-c` at `a`. -/
-lemma integral_has_deriv_within_at_of_tendsto_ae_left (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) {s t : set ℝ} [FTC_filter a (𝓝[s] a) (𝓝[t] a)]
-  (ha : tendsto f (𝓝[t] a ⊓ volume.ae) (𝓝 c)) :
+lemma integral_has_deriv_within_at_of_tendsto_ae_left (hf : interval_integrable f volume a b)
+  {s t : set ℝ} [FTC_filter a (𝓝[s] a) (𝓝[t] a)] (ha : tendsto f (𝓝[t] a ⊓ volume.ae) (𝓝 c)) :
   has_deriv_within_at (λ u, ∫ x in u..b, f x) (-c) s a :=
 by { simp only [integral_symm b],
-  exact (integral_has_deriv_within_at_of_tendsto_ae_right hfm hfi.symm ha).neg }
+  exact (integral_has_deriv_within_at_of_tendsto_ae_right hf.symm ha).neg }
 
 /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous
 from the left or from the right at `a`, then `u ↦ ∫ x in u..b, f x` has left (resp., right)
 derivative `-f a` at `a`. -/
-lemma integral_has_deriv_within_at_left (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) {s t : set ℝ} [FTC_filter a (𝓝[s] a) (𝓝[t] a)]
-  (ha : continuous_within_at f t a) :
+lemma integral_has_deriv_within_at_left (hf : interval_integrable f volume a b)
+  {s t : set ℝ} [FTC_filter a (𝓝[s] a) (𝓝[t] a)] (ha : continuous_within_at f t a) :
   has_deriv_within_at (λ u, ∫ x in u..b, f x) (-f a) s a :=
-integral_has_deriv_within_at_of_tendsto_ae_left hfm hfi (ha.mono_left inf_le_left)
+integral_has_deriv_within_at_of_tendsto_ae_left hf (ha.mono_left inf_le_left)
 
 /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
 limit `c` almost surely as `x` tends to `a` from the right or from the left, then the right
 (resp., left) derivative of `u ↦ ∫ x in u..b, f x` at `a` equals `-c`. -/
-lemma deriv_within_integral_of_tendsto_ae_left (hfm : measurable f)
-  (hfi : interval_integrable f volume a b) {s t : set ℝ} [FTC_filter a (𝓝[s] a) (𝓝[t] a)]
-  (ha : tendsto f (𝓝[t] a ⊓ volume.ae) (𝓝 c))
+lemma deriv_within_integral_of_tendsto_ae_left (hf : interval_integrable f volume a b)
+  {s t : set ℝ} [FTC_filter a (𝓝[s] a) (𝓝[t] a)] (ha : tendsto f (𝓝[t] a ⊓ volume.ae) (𝓝 c))
   (hs : unique_diff_within_at ℝ s a . unique_diff_within_at_Ici_Iic_univ) :
   deriv_within (λ u, ∫ x in u..b, f x) s a = -c :=
-(integral_has_deriv_within_at_of_tendsto_ae_left hfm hfi ha).deriv_within hs
+(integral_has_deriv_within_at_of_tendsto_ae_left hf ha).deriv_within hs
 
 /-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous
 on the right or on the left at `a`, then the right (resp., left) derivative of
 `u ↦ ∫ x in u..b, f x` at `a` equals `-f a`. -/
-lemma deriv_within_integral_left (hfm : measurable f) (hfi : interval_integrable f volume a b)
+lemma deriv_within_integral_left (hf : interval_integrable f volume a b)
   {s t : set ℝ} [FTC_filter a (𝓝[s] a) (𝓝[t] a)] (ha : continuous_within_at f t a)
   (hs : unique_diff_within_at ℝ s a . unique_diff_within_at_Ici_Iic_univ) :
   deriv_within (λ u, ∫ x in u..b, f x) s a = -f a :=
-(integral_has_deriv_within_at_left hfm hfi ha).deriv_within hs
+(integral_has_deriv_within_at_left hf ha).deriv_within hs
 
 end interval_integral
diff --git a/src/measure_theory/l1_space.lean b/src/measure_theory/l1_space.lean
index f3ed92d6f942f..42294ebe32b9a 100644
--- a/src/measure_theory/l1_space.lean
+++ b/src/measure_theory/l1_space.lean
@@ -26,7 +26,10 @@ of being almost everywhere equal is defined as a subspace of the space `L⁰`. S
 ## Main definitions
 
 * Let `f : α → β` be a function, where `α` is a `measure_space` and `β` a `normed_group`.
-  Then `f` is called `integrable` if `(∫⁻ a, nnnorm (f a)) < ⊤` holds.
+  Then `has_finite_integral f` means `(∫⁻ a, nnnorm (f a)) < ⊤`.
+
+* If `β` is moreover a `measurable_space` then `f` is called `integrable` if
+  `f` is `measurable` and `has_finite_integral f` holds.
 
 * The space `L¹` is defined as a subspace of `L⁰` :
   An `ae_eq_fun` `[f] : α →ₘ β` is in the space `L¹` if `edist [f] 0 < ⊤`, which means
@@ -53,67 +56,106 @@ integrable, function space, l1
 -/
 
 noncomputable theory
-open_locale classical topological_space
+open_locale classical topological_space big_operators
+
+open set filter topological_space ennreal emetric measure_theory
 
+variables {α β γ δ : Type*} [measurable_space α] {μ ν : measure α}
+variables [normed_group β]
+variables [normed_group γ]
 
 namespace measure_theory
-open set filter topological_space ennreal emetric
-open_locale big_operators
 
-universes u v w
-variables {α : Type u} [measurable_space α] {μ ν : measure α}
-variables {β : Type v} [normed_group β] {γ : Type w} [normed_group γ]
+/-! ### Some results about the Lebesgue integral involving a normed group -/
+
+lemma lintegral_nnnorm_eq_lintegral_edist (f : α → β) :
+  ∫⁻ a, nnnorm (f a) ∂μ = ∫⁻ a, edist (f a) 0 ∂μ :=
+by simp only [edist_eq_coe_nnnorm]
 
-/-- `integrable f μ` means that the integral `∫⁻ a, ∥f a∥ ∂μ` is finite; `integrable f` means
-`integrable f volume`. -/
-def integrable (f : α → β) (μ : measure α . volume_tac) : Prop := ∫⁻ a, nnnorm (f a) ∂μ < ⊤
+lemma lintegral_norm_eq_lintegral_edist (f : α → β) :
+  ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ = ∫⁻ a, edist (f a) 0 ∂μ :=
+by simp only [of_real_norm_eq_coe_nnnorm, edist_eq_coe_nnnorm]
 
-lemma integrable_iff_norm (f : α → β) : integrable f μ ↔ ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ < ⊤ :=
-by simp only [integrable, of_real_norm_eq_coe_nnnorm]
+lemma lintegral_edist_triangle [second_countable_topology β] [measurable_space β]
+  [opens_measurable_space β] {f g h : α → β}
+  (hf : measurable f) (hg : measurable g) (hh : measurable h) :
+  ∫⁻ a, edist (f a) (g a) ∂μ ≤ ∫⁻ a, edist (f a) (h a) ∂μ + ∫⁻ a, edist (g a) (h a) ∂μ :=
+begin
+  rw ← lintegral_add (hf.edist hh) (hg.edist hh),
+  refine lintegral_mono (λ a, _),
+  apply edist_triangle_right
+end
 
-lemma integrable_iff_edist (f : α → β) : integrable f μ ↔ ∫⁻ a, edist (f a) 0 ∂μ < ⊤ :=
-by simp only [integrable_iff_norm, edist_dist, dist_zero_right]
+lemma lintegral_nnnorm_zero : ∫⁻ a : α, nnnorm (0 : β) ∂μ = 0 := by simp
 
-lemma integrable_iff_of_real {f : α → ℝ} (h : 0 ≤ᵐ[μ] f) :
-  integrable f μ ↔ ∫⁻ a, ennreal.of_real (f a) ∂μ < ⊤ :=
+lemma lintegral_nnnorm_add [measurable_space β] [opens_measurable_space β]
+  [measurable_space γ] [opens_measurable_space γ]
+  {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) :
+  ∫⁻ a, nnnorm (f a) + nnnorm (g a) ∂μ = ∫⁻ a, nnnorm (f a) ∂μ + ∫⁻ a, nnnorm (g a) ∂μ :=
+lintegral_add hf.ennnorm hg.ennnorm
+
+lemma lintegral_nnnorm_neg {f : α → β} :
+  ∫⁻ a, nnnorm ((-f) a) ∂μ = ∫⁻ a, nnnorm (f a) ∂μ :=
+by simp only [pi.neg_apply, nnnorm_neg]
+
+/-! ### The predicate `has_finite_integral` -/
+
+/-- `has_finite_integral f μ` means that the integral `∫⁻ a, ∥f a∥ ∂μ` is finite.
+  `has_finite_integral f` means `has_finite_integral f volume`. -/
+def has_finite_integral (f : α → β) (μ : measure α . volume_tac) : Prop :=
+∫⁻ a, nnnorm (f a) ∂μ < ⊤
+
+lemma has_finite_integral_iff_norm (f : α → β) :
+  has_finite_integral f μ ↔ ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ < ⊤ :=
+by simp only [has_finite_integral, of_real_norm_eq_coe_nnnorm]
+
+lemma has_finite_integral_iff_edist (f : α → β) :
+  has_finite_integral f μ ↔ ∫⁻ a, edist (f a) 0 ∂μ < ⊤ :=
+by simp only [has_finite_integral_iff_norm, edist_dist, dist_zero_right]
+
+lemma has_finite_integral_iff_of_real {f : α → ℝ} (h : 0 ≤ᵐ[μ] f) :
+  has_finite_integral f μ ↔ ∫⁻ a, ennreal.of_real (f a) ∂μ < ⊤ :=
 have lintegral_eq : ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ = ∫⁻ a, ennreal.of_real (f a) ∂μ :=
 begin
   refine lintegral_congr_ae (h.mono $ λ a h, _),
   rwa [real.norm_eq_abs, abs_of_nonneg]
 end,
-by rw [integrable_iff_norm, lintegral_eq]
+by rw [has_finite_integral_iff_norm, lintegral_eq]
 
-lemma integrable.mono {f : α → β} {g : α → γ} (hg : integrable g μ) (h : ∀ᵐ a ∂μ, ∥f a∥ ≤ ∥g a∥) :
-  integrable f μ :=
+lemma has_finite_integral.mono {f : α → β} {g : α → γ} (hg : has_finite_integral g μ)
+  (h : ∀ᵐ a ∂μ, ∥f a∥ ≤ ∥g a∥) : has_finite_integral f μ :=
 begin
-  simp only [integrable_iff_norm] at *,
+  simp only [has_finite_integral_iff_norm] at *,
   calc ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ ≤ ∫⁻ (a : α), (ennreal.of_real ∥g a∥) ∂μ :
     lintegral_mono_ae (h.mono $ assume a h, of_real_le_of_real h)
     ... < ⊤ : hg
 end
 
-lemma integrable.mono' {f : α → β} {g : α → ℝ} (hg : integrable g μ) (h : ∀ᵐ a ∂μ, ∥f a∥ ≤ g a) :
-  integrable f μ :=
+lemma has_finite_integral.mono' {f : α → β} {g : α → ℝ} (hg : has_finite_integral g μ)
+  (h : ∀ᵐ a ∂μ, ∥f a∥ ≤ g a) : has_finite_integral f μ :=
 hg.mono $ h.mono $ λ x hx, le_trans hx (le_abs_self _)
 
-lemma integrable.congr' {f : α → β} {g : α → γ} (hf : integrable f μ)
+lemma has_finite_integral.congr' {f : α → β} {g : α → γ} (hf : has_finite_integral f μ)
   (h : ∀ᵐ a ∂μ, ∥f a∥ = ∥g a∥) :
-  integrable g μ :=
+  has_finite_integral g μ :=
 hf.mono $ eventually_eq.le $ eventually_eq.symm h
 
-lemma integrable_congr' {f : α → β} {g : α → γ} (h : ∀ᵐ a ∂μ, ∥f a∥ = ∥g a∥) :
-  integrable f μ ↔ integrable g μ :=
+lemma has_finite_integral_congr' {f : α → β} {g : α → γ} (h : ∀ᵐ a ∂μ, ∥f a∥ = ∥g a∥) :
+  has_finite_integral f μ ↔ has_finite_integral g μ :=
 ⟨λ hf, hf.congr' h, λ hg, hg.congr' $ eventually_eq.symm h⟩
 
-lemma integrable.congr {f g : α → β} (hf : integrable f μ) (h : f =ᵐ[μ] g) : integrable g μ :=
+lemma has_finite_integral.congr {f g : α → β} (hf : has_finite_integral f μ) (h : f =ᵐ[μ] g) :
+  has_finite_integral g μ :=
 hf.congr' $ h.fun_comp norm
 
-lemma integrable_congr {f g : α → β} (h : f =ᵐ[μ] g) : integrable f μ ↔ integrable g μ :=
-integrable_congr' $ h.fun_comp norm
+lemma has_finite_integral_congr {f g : α → β} (h : f =ᵐ[μ] g) :
+  has_finite_integral f μ ↔ has_finite_integral g μ :=
+has_finite_integral_congr' $ h.fun_comp norm
 
-lemma integrable_const_iff {c : β} : integrable (λ x : α, c) μ ↔ c = 0 ∨ μ univ < ⊤ :=
+lemma has_finite_integral_const_iff {c : β} :
+  has_finite_integral (λ x : α, c) μ ↔ c = 0 ∨ μ univ < ⊤ :=
 begin
-  simp only [integrable, lintegral_const],
+  simp only [has_finite_integral, lintegral_const],
   by_cases hc : c = 0,
   { simp [hc] },
   { simp only [hc, false_or],
@@ -123,143 +165,68 @@ begin
     rwa [ne.def, nnnorm_eq_zero] }
 end
 
-lemma integrable_const [finite_measure μ] (c : β) : integrable (λ x : α, c) μ :=
-integrable_const_iff.2 (or.inr $ measure_lt_top _ _)
+lemma has_finite_integral_const [finite_measure μ] (c : β) : has_finite_integral (λ x : α, c) μ :=
+has_finite_integral_const_iff.2 (or.inr $ measure_lt_top _ _)
 
-lemma integrable_of_bounded [finite_measure μ] {f : α → β} {C : ℝ} (hC : ∀ᵐ a ∂μ, ∥f a∥ ≤ C) :
-  integrable f μ :=
-(integrable_const C).mono' hC
+lemma has_finite_integral_of_bounded [finite_measure μ] {f : α → β} {C : ℝ}
+  (hC : ∀ᵐ a ∂μ, ∥f a∥ ≤ C) : has_finite_integral f μ :=
+(has_finite_integral_const C).mono' hC
 
-lemma integrable.mono_measure {f : α → β} (h : integrable f ν) (hμ : μ ≤ ν) :
-  integrable f μ :=
+lemma has_finite_integral.mono_measure {f : α → β} (h : has_finite_integral f ν) (hμ : μ ≤ ν) :
+  has_finite_integral f μ :=
 lt_of_le_of_lt (lintegral_mono' hμ (le_refl _)) h
 
-lemma integrable.add_measure {f : α → β} (hμ : integrable f μ) (hν : integrable f ν) :
-  integrable f (μ + ν) :=
+lemma has_finite_integral.add_measure {f : α → β} (hμ : has_finite_integral f μ)
+  (hν : has_finite_integral f ν) : has_finite_integral f (μ + ν) :=
 begin
-  simp only [integrable, lintegral_add_measure] at *,
+  simp only [has_finite_integral, lintegral_add_measure] at *,
   exact add_lt_top.2 ⟨hμ, hν⟩
 end
 
-lemma integrable.left_of_add_measure {f : α → β} (h : integrable f (μ + ν)) :
-  integrable f μ :=
+lemma has_finite_integral.left_of_add_measure {f : α → β} (h : has_finite_integral f (μ + ν)) :
+  has_finite_integral f μ :=
 h.mono_measure $ measure.le_add_right $ le_refl _
 
-lemma integrable.right_of_add_measure {f : α → β} (h : integrable f (μ + ν)) :
-  integrable f ν :=
+lemma has_finite_integral.right_of_add_measure {f : α → β} (h : has_finite_integral f (μ + ν)) :
+  has_finite_integral f ν :=
 h.mono_measure $ measure.le_add_left $ le_refl _
 
-@[simp] lemma integrable_add_measure {f : α → β} :
-  integrable f (μ + ν) ↔ integrable f μ ∧ integrable f ν :=
+@[simp] lemma has_finite_integral_add_measure {f : α → β} :
+  has_finite_integral f (μ + ν) ↔ has_finite_integral f μ ∧ has_finite_integral f ν :=
 ⟨λ h, ⟨h.left_of_add_measure, h.right_of_add_measure⟩, λ h, h.1.add_measure h.2⟩
 
-lemma integrable.smul_measure {f : α → β} (h : integrable f μ) {c : ennreal} (hc : c < ⊤) :
-  integrable f (c • μ) :=
+lemma has_finite_integral.smul_measure {f : α → β} (h : has_finite_integral f μ) {c : ennreal}
+  (hc : c < ⊤) : has_finite_integral f (c • μ) :=
 begin
-  simp only [integrable, lintegral_smul_measure] at *,
+  simp only [has_finite_integral, lintegral_smul_measure] at *,
   exact mul_lt_top hc h
 end
 
-@[simp] lemma integrable_zero_measure (f : α → β) : integrable f 0 :=
-by simp only [integrable, lintegral_zero_measure, with_top.zero_lt_top]
-
-lemma integrable_map_measure {δ} [measurable_space δ] [measurable_space β]
-  [opens_measurable_space β] {f : α → δ} {g : δ → β}
-  (hf : measurable f) (hg : measurable g) :
-  integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ :=
-by simp only [integrable, lintegral_map hg.ennnorm hf]
-
-lemma lintegral_nnnorm_eq_lintegral_edist (f : α → β) :
-  ∫⁻ a, nnnorm (f a) ∂μ = ∫⁻ a, edist (f a) 0 ∂μ :=
-by simp only [edist_eq_coe_nnnorm]
-
-lemma lintegral_norm_eq_lintegral_edist (f : α → β) :
-  ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ = ∫⁻ a, edist (f a) 0 ∂μ :=
-by simp only [of_real_norm_eq_coe_nnnorm, edist_eq_coe_nnnorm]
-
-lemma lintegral_edist_triangle [second_countable_topology β] [measurable_space β]
-  [opens_measurable_space β] {f g h : α → β}
-  (hf : measurable f) (hg : measurable g) (hh : measurable h) :
-  ∫⁻ a, edist (f a) (g a) ∂μ ≤ ∫⁻ a, edist (f a) (h a) ∂μ + ∫⁻ a, edist (g a) (h a) ∂μ :=
-begin
-  rw ← lintegral_add (hf.edist hh) (hg.edist hh),
-  refine lintegral_mono (λ a, _),
-  apply edist_triangle_right
-end
-
-lemma lintegral_edist_lt_top [second_countable_topology β] [measurable_space β]
-  [opens_measurable_space β] {f g : α → β}
-  (hfm : measurable f) (hfi : integrable f μ) (hgm : measurable g) (hgi : integrable g μ) :
-  ∫⁻ a, edist (f a) (g a) ∂μ < ⊤ :=
-lt_of_le_of_lt
-  (lintegral_edist_triangle hfm hgm (measurable_const : measurable (λa, (0 : β))))
-  (ennreal.add_lt_top.2 $ by { split; rw ← integrable_iff_edist; assumption })
-
-lemma lintegral_nnnorm_zero : ∫⁻ a : α, nnnorm (0 : β) ∂μ = 0 := by simp
+@[simp] lemma has_finite_integral_zero_measure (f : α → β) : has_finite_integral f 0 :=
+by simp only [has_finite_integral, lintegral_zero_measure, with_top.zero_lt_top]
 
 variables (α β μ)
-@[simp] lemma integrable_zero : integrable (λa:α, (0:β)) μ :=
-by simp [integrable]
+@[simp] lemma has_finite_integral_zero : has_finite_integral (λa:α, (0:β)) μ :=
+by simp [has_finite_integral]
 variables {α β μ}
 
-lemma lintegral_nnnorm_add [measurable_space β] [opens_measurable_space β]
-  [measurable_space γ] [opens_measurable_space γ]
-  {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) :
-  ∫⁻ a, nnnorm (f a) + nnnorm (g a) ∂μ = ∫⁻ a, nnnorm (f a) ∂μ + ∫⁻ a, nnnorm (g a) ∂μ :=
-lintegral_add hf.ennnorm hg.ennnorm
-
-lemma integrable.add [measurable_space β] [opens_measurable_space β]
-  {f g : α → β} (hfm : measurable f) (hfi : integrable f μ)
-  (hgm : measurable g) (hgi : integrable g μ) :
-  integrable (f + g) μ :=
-calc
-  ∫⁻ a, nnnorm (f a + g a) ∂μ ≤ ∫⁻ a, nnnorm (f a) + nnnorm (g a) ∂μ :
-    lintegral_mono
-      (assume a, by { simp only [← coe_add, coe_le_coe], exact nnnorm_add_le _ _ })
-  ... = _ :
-    lintegral_nnnorm_add hfm hgm
-  ... < ⊤ : add_lt_top.2 ⟨hfi, hgi⟩
+lemma has_finite_integral.neg {f : α → β} (hfi : has_finite_integral f μ) :
+  has_finite_integral (-f) μ :=
+by simpa [has_finite_integral] using hfi
 
-lemma integrable_finset_sum {ι} [measurable_space β] [borel_space β]
-  [second_countable_topology β] (s : finset ι) {f : ι → α → β}
-  (hfm : ∀ i, measurable (f i)) (hfi : ∀ i, integrable (f i) μ) :
-  integrable (λ a, ∑ i in s, f i a) μ :=
-begin
-  refine finset.induction_on s _ _,
-  { simp only [finset.sum_empty, integrable_zero] },
-  { assume i s his ih,
-    simp only [his, finset.sum_insert, not_false_iff],
-    refine (hfi _).add (hfm _) (s.measurable_sum hfm) ih }
-end
-
-lemma lintegral_nnnorm_neg {f : α → β} :
-  ∫⁻ a, nnnorm ((-f) a) ∂μ = ∫⁻ a, nnnorm (f a) ∂μ :=
-by simp only [pi.neg_apply, nnnorm_neg]
-
-lemma integrable.neg {f : α → β} (hfi : integrable f μ) : integrable (-f) μ :=
-calc _ = _ : lintegral_nnnorm_neg
-   ... < ⊤ : hfi
-
-@[simp] lemma integrable_neg_iff {f : α → β} : integrable (-f) μ ↔ integrable f μ :=
-⟨λ h, neg_neg f ▸ h.neg, integrable.neg⟩
-
-lemma integrable.sub [measurable_space β] [opens_measurable_space β]
-  {f g : α → β} (hfm : measurable f) (hfi : integrable f μ) (hgm : measurable g)
-  (hgi : integrable g μ) : integrable (f - g) μ :=
-calc
-  ∫⁻ a, nnnorm (f a - g a) ∂μ ≤ ∫⁻ a, nnnorm (f a) + nnnorm (-g a) ∂μ :
-    lintegral_mono (assume a, by exact_mod_cast nnnorm_add_le _ _ )
-  ... = _ :
-    by { simp only [nnnorm_neg], exact lintegral_nnnorm_add hfm hgm }
-  ... < ⊤ : add_lt_top.2 ⟨hfi, hgi⟩
+@[simp] lemma has_finite_integral_neg_iff {f : α → β} :
+  has_finite_integral (-f) μ ↔ has_finite_integral f μ :=
+⟨λ h, neg_neg f ▸ h.neg, has_finite_integral.neg⟩
 
-lemma integrable.norm {f : α → β} (hfi : integrable f μ) : integrable (λa, ∥f a∥) μ :=
+lemma has_finite_integral.norm {f : α → β} (hfi : has_finite_integral f μ) :
+  has_finite_integral (λa, ∥f a∥) μ :=
 have eq : (λa, (nnnorm ∥f a∥ : ennreal)) = λa, (nnnorm (f a) : ennreal),
   by { funext, rw nnnorm_norm },
-by { rwa [integrable, eq] }
+by { rwa [has_finite_integral, eq] }
 
-lemma integrable_norm_iff (f : α → β) : integrable (λa, ∥f a∥) μ ↔ integrable f μ :=
-integrable_congr' $ eventually_of_forall $ λ x, norm_norm (f x)
+lemma has_finite_integral_norm_iff (f : α → β) :
+  has_finite_integral (λa, ∥f a∥) μ ↔ has_finite_integral f μ :=
+has_finite_integral_congr' $ eventually_of_forall $ λ x, norm_norm (f x)
 
 section dominated_convergence
 
@@ -285,21 +252,21 @@ begin
   exact le_of_tendsto' tendsto_norm (F_le_bound)
 end
 
-lemma integrable_of_dominated_convergence {F : ℕ → α → β} {f : α → β} {bound : α → ℝ}
-  (bound_integrable : integrable bound μ)
+lemma has_finite_integral_of_dominated_convergence {F : ℕ → α → β} {f : α → β} {bound : α → ℝ}
+  (bound_has_finite_integral : has_finite_integral bound μ)
   (h_bound : ∀ n, ∀ᵐ a ∂μ, ∥F n a∥ ≤ bound a)
   (h_lim : ∀ᵐ a ∂μ, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
-  integrable f μ :=
+  has_finite_integral f μ :=
 /- `∥F n a∥ ≤ bound a` and `∥F n a∥ --> ∥f a∥` implies `∥f a∥ ≤ bound a`,
-  and so `∫ ∥f∥ ≤ ∫ bound < ⊤` since `bound` is integrable -/
+  and so `∫ ∥f∥ ≤ ∫ bound < ⊤` since `bound` is has_finite_integral -/
 begin
-  rw integrable_iff_norm,
+  rw has_finite_integral_iff_norm,
   calc ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ ≤ ∫⁻ a, ennreal.of_real (bound a) ∂μ :
     lintegral_mono_ae $ all_ae_of_real_f_le_bound h_bound h_lim
     ... < ⊤ :
     begin
-      rw ← integrable_iff_of_real,
-      { exact bound_integrable },
+      rw ← has_finite_integral_iff_of_real,
+      { exact bound_has_finite_integral },
       exact (h_bound 0).mono (λ a h, le_trans (norm_nonneg _) h)
     end
 end
@@ -309,7 +276,7 @@ lemma tendsto_lintegral_norm_of_dominated_convergence [measurable_space β]
   {F : ℕ → α → β} {f : α → β} {bound : α → ℝ}
   (F_measurable : ∀ n, measurable (F n))
   (f_measurable : measurable f)
-  (bound_integrable : integrable bound μ)
+  (bound_has_finite_integral : has_finite_integral 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, (ennreal.of_real ∥F n a - f a∥) ∂μ) at_top (𝓝 0) :=
@@ -346,11 +313,11 @@ begin
   refine tendsto_lintegral_of_dominated_convergence _ _ hb _ _,
   -- Show `λa, ∥f a - F n a∥` is measurable for all `n`
   { exact λn, measurable_of_real.comp ((F_measurable n).sub f_measurable).norm },
-  -- Show `2 * bound` is integrable
-  { rw integrable_iff_of_real at bound_integrable,
+  -- Show `2 * bound` is has_finite_integral
+  { rw has_finite_integral_iff_of_real at bound_has_finite_integral,
     { calc ∫⁻ a, b a ∂μ = 2 * ∫⁻ a, ennreal.of_real (bound a) ∂μ :
         by { rw lintegral_const_mul', exact coe_ne_top }
-        ... < ⊤ : mul_lt_top (coe_lt_top) bound_integrable },
+        ... < ⊤ : mul_lt_top (coe_lt_top) bound_has_finite_integral },
     filter_upwards [h_bound 0] λ a h, le_trans (norm_nonneg _) h },
   -- Show `∥f a - F n a∥ --> 0`
   { exact h }
@@ -361,10 +328,12 @@ end dominated_convergence
 section pos_part
 /-! Lemmas used for defining the positive part of a `L¹` function -/
 
-lemma integrable.max_zero {f : α → ℝ} (hf : integrable f μ) : integrable (λa, max (f a) 0) μ :=
+lemma has_finite_integral.max_zero {f : α → ℝ} (hf : has_finite_integral f μ) :
+  has_finite_integral (λa, max (f a) 0) μ :=
 hf.mono $ eventually_of_forall $ λ x, by simp [real.norm_eq_abs, abs_le, abs_nonneg, le_abs_self]
 
-lemma integrable.min_zero {f : α → ℝ} (hf : integrable f μ) : integrable (λa, min (f a) 0) μ :=
+lemma has_finite_integral.min_zero {f : α → ℝ} (hf : has_finite_integral f μ) :
+  has_finite_integral (λa, min (f a) 0) μ :=
 hf.mono $ eventually_of_forall $ λ x,
   by simp [real.norm_eq_abs, abs_le, abs_nonneg, neg_le, neg_le_abs_self]
 
@@ -373,9 +342,10 @@ end pos_part
 section normed_space
 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
 
-lemma integrable.smul (c : 𝕜) {f : α → β} : integrable f μ → integrable (c • f) μ :=
+lemma has_finite_integral.smul (c : 𝕜) {f : α → β} : has_finite_integral f μ →
+  has_finite_integral (c • f) μ :=
 begin
-  simp only [integrable], assume hfi,
+  simp only [has_finite_integral], assume hfi,
   calc
     ∫⁻ (a : α), nnnorm (c • f a) ∂μ = ∫⁻ (a : α), (nnnorm c) * nnnorm (f a) ∂μ :
       by simp only [nnnorm_smul, ennreal.coe_mul]
@@ -386,17 +356,175 @@ begin
     end
 end
 
-lemma integrable_smul_iff {c : 𝕜} (hc : c ≠ 0) (f : α → β) :
-  integrable (c • f) μ ↔ integrable f μ :=
+lemma has_finite_integral_smul_iff {c : 𝕜} (hc : c ≠ 0) (f : α → β) :
+  has_finite_integral (c • f) μ ↔ has_finite_integral f μ :=
 begin
   split,
   { assume h,
     simpa only [smul_smul, inv_mul_cancel hc, one_smul] using h.smul c⁻¹ },
-  exact integrable.smul _
+  exact has_finite_integral.smul _
+end
+
+lemma has_finite_integral.const_mul {f : α → ℝ} (h : has_finite_integral f μ) (c : ℝ) :
+  has_finite_integral (λ x, c * f x) μ :=
+(has_finite_integral.smul c h : _)
+
+lemma has_finite_integral.mul_const {f : α → ℝ} (h : has_finite_integral f μ) (c : ℝ) :
+  has_finite_integral (λ x, f x * c) μ :=
+by simp_rw [mul_comm, h.const_mul _]
+end normed_space
+
+/-! ### The predicate `integrable` -/
+
+variables [measurable_space β] [measurable_space γ] [measurable_space δ]
+
+/-- `integrable f μ` means that `f` is measurable and that the integral `∫⁻ a, ∥f a∥ ∂μ` is finite.
+  `integrable f` means `integrable f volume`. -/
+def integrable (f : α → β) (μ : measure α . volume_tac) : Prop :=
+measurable f ∧ has_finite_integral f μ
+
+lemma integrable.measurable {f : α → β} (hf : integrable f μ) : measurable f := hf.1
+lemma integrable.has_finite_integral {f : α → β} (hf : integrable f μ) : has_finite_integral f μ :=
+hf.2
+
+lemma integrable.mono {f : α → β} {g : α → γ} (hg : integrable g μ) (hf : measurable f)
+  (h : ∀ᵐ a ∂μ, ∥f a∥ ≤ ∥g a∥) : integrable f μ :=
+⟨hf, hg.has_finite_integral.mono h⟩
+
+lemma integrable.mono' {f : α → β} {g : α → ℝ} (hg : integrable g μ) (hf : measurable f)
+  (h : ∀ᵐ a ∂μ, ∥f a∥ ≤ g a) : integrable f μ :=
+⟨hf, hg.has_finite_integral.mono' h⟩
+
+lemma integrable.congr' {f : α → β} {g : α → γ} (hf : integrable f μ) (hg : measurable g)
+  (h : ∀ᵐ a ∂μ, ∥f a∥ = ∥g a∥) : integrable g μ :=
+⟨hg, hf.has_finite_integral.congr' h⟩
+
+lemma integrable_congr' {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g)
+  (h : ∀ᵐ a ∂μ, ∥f a∥ = ∥g a∥) : integrable f μ ↔ integrable g μ :=
+⟨λ h2f, h2f.congr' hg h, λ h2g, h2g.congr' hf $ eventually_eq.symm h⟩
+
+lemma integrable.congr {f g : α → β} (hf : integrable f μ) (hg : measurable g) (h : f =ᵐ[μ] g) :
+  integrable g μ :=
+hf.congr' hg $ h.fun_comp norm
+
+lemma integrable_congr {f g : α → β} (hf : measurable f) (hg : measurable g) (h : f =ᵐ[μ] g) :
+  integrable f μ ↔ integrable g μ :=
+integrable_congr' hf hg $ h.fun_comp norm
+
+lemma integrable_const_iff {c : β} : integrable (λ x : α, c) μ ↔ c = 0 ∨ μ univ < ⊤ :=
+by rw [integrable, and_iff_right measurable_const, has_finite_integral_const_iff]
+
+lemma integrable_const [finite_measure μ] (c : β) : integrable (λ x : α, c) μ :=
+integrable_const_iff.2 $ or.inr $ measure_lt_top _ _
+
+lemma integrable.mono_measure {f : α → β} (h : integrable f ν) (hμ : μ ≤ ν) : integrable f μ :=
+⟨h.measurable, h.has_finite_integral.mono_measure hμ⟩
+
+lemma integrable.add_measure {f : α → β} (hμ : integrable f μ) (hν : integrable f ν) :
+  integrable f (μ + ν) :=
+⟨hμ.measurable, hμ.has_finite_integral.add_measure hν.has_finite_integral⟩
+
+lemma integrable.left_of_add_measure {f : α → β} (h : integrable f (μ + ν)) : integrable f μ :=
+h.mono_measure $ measure.le_add_right $ le_refl _
+
+lemma integrable.right_of_add_measure {f : α → β} (h : integrable f (μ + ν)) : integrable f ν :=
+h.mono_measure $ measure.le_add_left $ le_refl _
+
+@[simp] lemma integrable_add_measure {f : α → β} :
+  integrable f (μ + ν) ↔ integrable f μ ∧ integrable f ν :=
+⟨λ h, ⟨h.left_of_add_measure, h.right_of_add_measure⟩, λ h, h.1.add_measure h.2⟩
+
+lemma integrable.smul_measure {f : α → β} (h : integrable f μ) {c : ennreal} (hc : c < ⊤) :
+  integrable f (c • μ) :=
+⟨h.measurable, h.has_finite_integral.smul_measure hc⟩
+
+lemma integrable_map_measure [opens_measurable_space β] {f : α → δ} {g : δ → β}
+  (hf : measurable f) (hg : measurable g) :
+  integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ :=
+by { simp only [integrable, has_finite_integral, lintegral_map hg.ennnorm hf, hf, hg, hg.comp hf] }
+
+lemma lintegral_edist_lt_top [second_countable_topology β] [opens_measurable_space β] {f g : α → β}
+  (hf : integrable f μ) (hg : integrable g μ) :
+  ∫⁻ a, edist (f a) (g a) ∂μ < ⊤ :=
+lt_of_le_of_lt
+  (lintegral_edist_triangle hf.measurable hg.measurable
+    (measurable_const : measurable (λa, (0 : β))))
+  (ennreal.add_lt_top.2 $ by { simp_rw ← has_finite_integral_iff_edist,
+                               exact ⟨hf.has_finite_integral, hg.has_finite_integral⟩ })
+
+
+variables (α β μ)
+@[simp] lemma integrable_zero : integrable (λ _, (0 : β)) μ :=
+by simp [integrable, measurable_const]
+variables {α β μ}
+
+lemma integrable.add [borel_space β] [second_countable_topology β]
+  {f g : α → β} (hf : integrable f μ) (hg : integrable g μ) : integrable (f + g) μ :=
+⟨hf.measurable.add hg.measurable, calc
+  ∫⁻ a, nnnorm (f a + g a) ∂μ ≤ ∫⁻ a, nnnorm (f a) + nnnorm (g a) ∂μ :
+    lintegral_mono
+      (assume a, by { simp only [← coe_add, coe_le_coe], exact nnnorm_add_le _ _ })
+  ... = _ :
+    lintegral_nnnorm_add hf.measurable hg.measurable
+  ... < ⊤ : add_lt_top.2 ⟨hf.has_finite_integral, hg.has_finite_integral⟩⟩
+
+lemma integrable_finset_sum {ι} [borel_space β] [second_countable_topology β] (s : finset ι)
+  {f : ι → α → β} (hf : ∀ i, integrable (f i) μ) : integrable (λ a, ∑ i in s, f i a) μ :=
+begin
+  refine finset.induction_on s _ _,
+  { simp only [finset.sum_empty, integrable_zero] },
+  { assume i s his ih, simp only [his, finset.sum_insert, not_false_iff],
+    exact (hf _).add ih }
 end
 
+lemma integrable.neg [borel_space β] {f : α → β} (hf : integrable f μ) : integrable (-f) μ :=
+⟨hf.measurable.neg, hf.has_finite_integral.neg⟩
+
+@[simp] lemma integrable_neg_iff [borel_space β] {f : α → β} : integrable (-f) μ ↔ integrable f μ :=
+⟨λ h, neg_neg f ▸ h.neg, integrable.neg⟩
+
+lemma integrable.sub [borel_space β] [second_countable_topology β] {f g : α → β}
+  (hf : integrable f μ) (hg : integrable g μ) : integrable (f - g) μ :=
+⟨hf.measurable.sub hg.measurable,
+calc
+  ∫⁻ a, nnnorm (f a - g a) ∂μ ≤ ∫⁻ a, nnnorm (f a) + nnnorm (-g a) ∂μ :
+    lintegral_mono (assume a, by exact_mod_cast nnnorm_add_le _ _ )
+  ... = _ :
+    by { simp only [nnnorm_neg], exact lintegral_nnnorm_add hf.measurable hg.measurable }
+  ... < ⊤ : add_lt_top.2 ⟨hf.has_finite_integral, hg.has_finite_integral⟩⟩
+
+lemma integrable.norm [opens_measurable_space β] {f : α → β} (hf : integrable f μ) :
+  integrable (λa, ∥f a∥) μ :=
+⟨hf.measurable.norm, hf.has_finite_integral.norm⟩
+
+lemma integrable_norm_iff [opens_measurable_space β] {f : α → β} (hf : measurable f) :
+  integrable (λa, ∥f a∥) μ ↔ integrable f μ :=
+by simp_rw [integrable, and_iff_right hf, and_iff_right hf.norm, has_finite_integral_norm_iff]
+
+section pos_part
+/-! Lemmas used for defining the positive part of a `L¹` function -/
+
+lemma integrable.max_zero {f : α → ℝ} (hf : integrable f μ) : integrable (λa, max (f a) 0) μ :=
+⟨hf.measurable.max measurable_const, hf.has_finite_integral.max_zero⟩
+
+lemma integrable.min_zero {f : α → ℝ} (hf : integrable f μ) : integrable (λa, min (f a) 0) μ :=
+⟨hf.measurable.min measurable_const, hf.has_finite_integral.min_zero⟩
+
+end pos_part
+
+section normed_space
+variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
+
+lemma integrable.smul [borel_space β] (c : 𝕜) {f : α → β}
+  (hf : integrable f μ) : integrable (c • f) μ :=
+⟨hf.measurable.const_smul c, hf.has_finite_integral.smul c⟩
+
+lemma integrable_smul_iff [borel_space β] {c : 𝕜} (hc : c ≠ 0) (f : α → β) :
+  integrable (c • f) μ ↔ integrable f μ :=
+and_congr (measurable_const_smul_iff hc) (has_finite_integral_smul_iff hc f)
+
 lemma integrable.const_mul {f : α → ℝ} (h : integrable f μ) (c : ℝ) : integrable (λ x, c * f x) μ :=
-(integrable.smul c h : _)
+integrable.smul c h
 
 lemma integrable.mul_const {f : α → ℝ} (h : integrable f μ) (c : ℝ) : integrable (λ x, f x * c) μ :=
 by simp_rw [mul_comm, h.const_mul _]
@@ -405,27 +533,26 @@ end normed_space
 
 variables [second_countable_topology β]
 
-namespace ae_eq_fun
+/-! ### The predicate `integrable` on measurable functions modulo a.e.-equality -/
 
-variable [measurable_space β]
+namespace ae_eq_fun
 
 section
 
 variable [opens_measurable_space β]
 
-/-- An almost everywhere equal function is `integrable` if it has a finite distance to the origin.
-  Should mean the same thing as the predicate `integrable` over functions. -/
+/-- A class of almost everywhere equal functions is `integrable` if it has a finite distance to
+  the origin. It means the same thing as the predicate `integrable` over functions. -/
 def integrable (f : α →ₘ[μ] β) : Prop := f ∈ ball (0 : α →ₘ[μ] β) ⊤
 
 lemma integrable_mk {f : α → β} (hf : measurable f) :
   (integrable (mk f hf : α →ₘ[μ] β)) ↔ measure_theory.integrable f μ :=
-by simp [integrable, zero_def, edist_mk_mk', measure_theory.integrable, nndist_eq_nnnorm]
+by simp [integrable, zero_def, edist_mk_mk', measure_theory.integrable, nndist_eq_nnnorm,
+         has_finite_integral, hf]
 
 lemma integrable_coe_fn {f : α →ₘ[μ] β} : (measure_theory.integrable f μ) ↔ integrable f :=
 by rw [← integrable_mk, mk_coe_fn]
 
-local attribute [simp] integrable_mk
-
 lemma integrable_zero : integrable (0 : α →ₘ[μ] β) := mem_ball_self coe_lt_top
 
 end
@@ -436,9 +563,9 @@ variable [borel_space β]
 
 lemma integrable.add {f g : α →ₘ[μ] β} : integrable f → integrable g → integrable (f + g) :=
 begin
-  refine induction_on₂ f g (λ f hf g hg, _),
-  simp only [integrable_mk, mk_add_mk],
-  exact λ hfi hgi, hfi.add hf hg hgi
+  refine induction_on₂ f g (λ f hf g hg hfi hgi, _),
+  simp only [integrable_mk, mk_add_mk] at hfi hgi ⊢,
+  exact hfi.add hgi
 end
 
 lemma integrable.neg {f : α →ₘ[μ] β} : integrable f → integrable (-f) :=
@@ -465,11 +592,13 @@ end
 
 end ae_eq_fun
 
+/-! ### The `L¹` space of functions -/
+
 variables (α β)
 /-- The space of equivalence classes of integrable (and measurable) functions, where two integrable
     functions are equivalent if they agree almost everywhere, i.e., they differ on a set of measure
     `0`. -/
-def l1 [measurable_space β] [opens_measurable_space β] (μ : measure α) : Type (max u v) :=
+def l1 [opens_measurable_space β] (μ : measure α) : Type* :=
 {f : α →ₘ[μ] β // f.integrable}
 
 notation α ` →₁[`:25 μ `] ` β := l1 α β μ
@@ -480,8 +609,6 @@ namespace l1
 open ae_eq_fun
 local attribute [instance] ae_eq_fun.is_add_subgroup
 
-variables [measurable_space β]
-
 section
 
 variable [opens_measurable_space β]
@@ -564,45 +691,42 @@ end normed_space
 section of_fun
 
 /-- Construct the equivalence class `[f]` of a measurable and integrable function `f`. -/
-def of_fun (f : α → β) (hfm : measurable f) (hfi : integrable f μ) : (α →₁[μ] β) :=
-⟨mk f hfm, by { rw integrable_mk, exact hfi }⟩
+def of_fun (f : α → β) (hf : integrable f μ) : (α →₁[μ] β) :=
+⟨mk f hf.measurable, by { rw integrable_mk, exact hf }⟩
 
-@[simp] lemma of_fun_eq_mk (f : α → β) (hfm hfi) :
-  ((of_fun f hfm hfi : α →₁[μ] β) : α →ₘ[μ] β) = mk f hfm :=
+@[simp] lemma of_fun_eq_mk (f : α → β) (hf : integrable f μ) :
+  (of_fun f hf : α →ₘ[μ] β) = mk f hf.measurable :=
 rfl
 
-lemma of_fun_eq_of_fun (f g : α → β) (hfm hfi hgm hgi) :
-  (of_fun f hfm hfi : α →₁[μ] β) = of_fun g hgm hgi ↔ f =ᵐ[μ] g :=
+lemma of_fun_eq_of_fun (f g : α → β) (hf : integrable f μ) (hg : integrable g μ) :
+  of_fun f hf = of_fun g hg ↔ f =ᵐ[μ] g :=
 by { rw ← l1.eq_iff, simp only [of_fun_eq_mk, mk_eq_mk] }
 
-lemma of_fun_zero :
-  (of_fun (λ _, 0) measurable_zero (integrable_zero α μ β) : α →₁[μ] β) = 0 := rfl
+lemma of_fun_zero : of_fun (λ _, (0 : β)) (integrable_zero α β μ) = 0 := rfl
 
-lemma of_fun_add (f g : α → β) (hfm hfi hgm hgi) :
-  (of_fun (f + g) (measurable.add hfm hgm) (integrable.add hfm hfi hgm hgi) : α →₁[μ] β)
-    = of_fun f hfm hfi + of_fun g hgm hgi :=
+lemma of_fun_add (f g : α → β) (hf : integrable f μ) (hg : integrable g μ) :
+  of_fun (f + g) (hf.add hg) = of_fun f hf + of_fun g hg :=
 rfl
 
-lemma of_fun_neg (f : α → β) (hfm hfi) :
-  (of_fun (- f) (measurable.neg hfm) (integrable.neg hfi) : α →₁[μ] β) = - of_fun f hfm hfi := rfl
+lemma of_fun_neg (f : α → β) (hf : integrable f μ) :
+  of_fun (- f) (integrable.neg hf) = - of_fun f hf := rfl
 
-lemma of_fun_sub (f g : α → β) (hfm hfi hgm hgi) :
-  (of_fun (f - g) (measurable.sub hfm hgm) (integrable.sub hfm hfi hgm hgi) : α →₁[μ] β)
-    = of_fun f hfm hfi - of_fun g hgm hgi :=
+lemma of_fun_sub (f g : α → β) (hf : integrable f μ) (hg : integrable g μ) :
+  of_fun (f - g) (hf.sub hg) = of_fun f hf - of_fun g hg :=
 rfl
 
-lemma norm_of_fun (f : α → β) (hfm hfi) :
-  ∥(of_fun f hfm hfi : α →₁[μ] β)∥ = ennreal.to_real (∫⁻ a, edist (f a) 0 ∂μ) :=
+lemma norm_of_fun (f : α → β) (hf : integrable f μ) :
+  ∥ of_fun f hf ∥ = ennreal.to_real (∫⁻ a, edist (f a) 0 ∂μ) :=
 rfl
 
-lemma norm_of_fun_eq_lintegral_norm (f : α → β) (hfm hfi) :
-  ∥(of_fun f hfm hfi : α →₁[μ] β)∥ = ennreal.to_real (∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ) :=
+lemma norm_of_fun_eq_lintegral_norm (f : α → β) (hf : integrable f μ) :
+  ∥ of_fun f hf ∥ = ennreal.to_real (∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ) :=
 by { rw [norm_of_fun, lintegral_norm_eq_lintegral_edist] }
 
 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
 
-lemma of_fun_smul (f : α → β) (hfm : measurable f) (hfi : integrable f μ) (k : 𝕜) :
-  of_fun (λa, k • f a) (hfm.const_smul _) (hfi.smul _) = k • of_fun f hfm hfi := rfl
+lemma of_fun_smul (f : α → β) (hf : integrable f μ) (k : 𝕜) :
+  of_fun (λa, k • f a) (hf.smul k) = k • of_fun f hf := rfl
 
 end of_fun
 
@@ -616,18 +740,20 @@ f.measurable.norm
 protected lemma integrable (f : α →₁[μ] β) : integrable ⇑f μ :=
 integrable_coe_fn.2 f.2
 
+protected lemma has_finite_integral (f : α →₁[μ] β) : has_finite_integral ⇑f μ :=
+f.integrable.has_finite_integral
+
 lemma integrable_norm (f : α →₁[μ] β) : integrable (λ a, ∥f a∥) μ :=
-(integrable_norm_iff _).mpr f.integrable
+(integrable_norm_iff f.measurable).mpr f.integrable
 
-lemma of_fun_to_fun (f : α →₁[μ] β) : of_fun f f.measurable f.integrable = f :=
+lemma of_fun_to_fun (f : α →₁[μ] β) : of_fun f f.integrable = f :=
 subtype.ext (f : α →ₘ[μ] β).mk_coe_fn
 
 lemma mk_to_fun (f : α →₁[μ] β) : (mk f f.measurable : α →ₘ[μ] β) = f :=
 by { rw ← of_fun_eq_mk, rw l1.eq_iff, exact of_fun_to_fun f }
 
-lemma to_fun_of_fun (f : α → β) (hfm hfi) :
-  ⇑(of_fun f hfm hfi : α →₁[μ] β) =ᵐ[μ] f :=
-coe_fn_mk f hfm
+lemma to_fun_of_fun (f : α → β) (hf : integrable f μ) : ⇑(of_fun f hf : α →₁[μ] β) =ᵐ[μ] f :=
+coe_fn_mk f hf.measurable
 
 variables (α β)
 lemma zero_to_fun : ⇑(0 : α →₁[μ] β) =ᵐ[μ] 0 := ae_eq_fun.coe_fn_zero
@@ -641,8 +767,7 @@ lemma neg_to_fun (f : α →₁[μ] β) : ⇑(-f) =ᵐ[μ] -⇑f := ae_eq_fun.co
 lemma sub_to_fun (f g : α →₁[μ] β) : ⇑(f - g) =ᵐ[μ] ⇑f - ⇑g :=
 ae_eq_fun.coe_fn_sub _ _
 
-lemma dist_to_fun (f g : α →₁[μ] β) :
-  dist f g = ennreal.to_real (∫⁻ x, edist (f x) (g x) ∂μ) :=
+lemma dist_to_fun (f g : α →₁[μ] β) : dist f g = ennreal.to_real (∫⁻ x, edist (f x) (g x) ∂μ) :=
 by { simp only [← coe_coe, dist_eq, edist_eq_coe] }
 
 lemma norm_eq_nnnorm_to_fun (f : α →₁[μ] β) : ∥f∥ = ennreal.to_real (∫⁻ a, nnnorm (f a) ∂μ) :=
@@ -653,10 +778,7 @@ lemma norm_eq_norm_to_fun (f : α →₁[μ] β) :
 by { rw norm_eq_nnnorm_to_fun, congr, funext, rw of_real_norm_eq_coe_nnnorm }
 
 lemma lintegral_edist_to_fun_lt_top (f g : α →₁[μ] β) : (∫⁻ a, edist (f a) (g a) ∂μ) < ⊤ :=
-begin
-  apply lintegral_edist_lt_top,
-  exact f.measurable, exact f.integrable, exact g.measurable, exact g.integrable
-end
+lintegral_edist_lt_top f.integrable g.integrable
 
 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
 
@@ -671,8 +793,9 @@ section pos_part
 def pos_part (f : α →₁[μ] ℝ) : α →₁[μ] ℝ :=
 ⟨ae_eq_fun.pos_part f,
   begin
-    rw [← ae_eq_fun.integrable_coe_fn, integrable_congr (coe_fn_pos_part _)],
-    exact integrable.max_zero f.integrable
+    rw [← ae_eq_fun.integrable_coe_fn,
+      integrable_congr (ae_eq_fun.measurable _) (f.measurable.max measurable_const) (coe_fn_pos_part _)],
+    exact f.integrable.max_zero
   end ⟩
 
 /-- Negative part of a function in `L¹` space. -/
@@ -703,8 +826,8 @@ begin
   rw to_real_le_to_real,
   { apply lintegral_mono_ae,
     exact h.mono (λ a h, of_real_le_of_real h) },
-  { rw [← lt_top_iff_ne_top, ← integrable_iff_norm], exact f.integrable },
-  { rw [← lt_top_iff_ne_top, ← integrable_iff_norm], exact g.integrable }
+  { rw [← lt_top_iff_ne_top, ← has_finite_integral_iff_norm], exact f.has_finite_integral },
+  { rw [← lt_top_iff_ne_top, ← has_finite_integral_iff_norm], exact g.has_finite_integral }
 end
 
 lemma continuous_pos_part : continuous $ λf : α →₁[μ] ℝ, pos_part f :=
@@ -734,3 +857,8 @@ end pos_part
 end l1
 
 end measure_theory
+open measure_theory
+
+lemma measurable.integrable_zero [measurable_space β] {f : α → β} (hf : measurable f) :
+  integrable f 0 :=
+⟨hf, has_finite_integral_zero_measure f⟩
diff --git a/src/measure_theory/set_integral.lean b/src/measure_theory/set_integral.lean
index 31caea2aa7f33..e74b3f2839250 100644
--- a/src/measure_theory/set_integral.lean
+++ b/src/measure_theory/set_integral.lean
@@ -23,7 +23,7 @@ We also define `integrable_on f s μ := integrable f (μ.restrict s)` and prove
 `integrable_on_union : integrable_on f (s ∪ t) μ ↔ integrable_on f s μ ∧ integrable_on f t μ`.
 
 Next we define a predicate `integrable_at_filter (f : α → E) (l : filter α) (μ : measure α)`
-saying that `f` is integrable at some set `s ∈ l` and prove that a function is integrable
+saying that `f` is integrable at some set `s ∈ l` and prove that a measurable function is integrable
 at `l` with respect to `μ` provided that `f` is bounded above at `l ⊓ μ.ae` and `μ` is finite
 at `l`.
 
@@ -89,10 +89,16 @@ namespace measure_theory
 
 section normed_group
 
-variables [normed_group E] {f : α → E} {s t : set α} {μ ν : measure α}
+lemma has_finite_integral_restrict_of_bounded [normed_group E] {f : α → E} {s : set α}
+  {μ : measure α} {C}  (hs : μ s < ⊤) (hf : ∀ᵐ x ∂(μ.restrict s), ∥f x∥ ≤ C) :
+  has_finite_integral f (μ.restrict s) :=
+by haveI : finite_measure (μ.restrict s) := ⟨by rwa [measure.restrict_apply_univ]⟩;
+  exact has_finite_integral_of_bounded hf
+
+variables [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ ν : measure α}
 
-/-- A function is `integrable_on` a set `s` if the integral of its pointwise norm over `s` is less
-than infinity. -/
+/-- A function is `integrable_on` a set `s` if it is a measurable function and if the integral of
+  its pointwise norm over `s` is less than infinity. -/
 def integrable_on (f : α → E) (s : set α) (μ : measure α . volume_tac) : Prop :=
 integrable f (μ.restrict s)
 
@@ -100,8 +106,8 @@ lemma integrable_on.integrable (h : integrable_on f s μ) :
   integrable f (μ.restrict s) :=
 h
 
-@[simp] lemma integrable_on_empty : integrable_on f ∅ μ :=
-by simp [integrable_on]
+@[simp] lemma integrable_on_empty (hf : measurable f) : integrable_on f ∅ μ :=
+by simp [integrable_on, measurable.integrable_zero hf]
 
 @[simp] lemma integrable_on_univ : integrable_on f univ μ ↔ integrable f μ :=
 by rw [integrable_on, measure.restrict_univ]
@@ -147,18 +153,17 @@ lemma integrable_on.union (hs : integrable_on f s μ) (ht : integrable_on f t μ
   integrable_on f (s ∪ t) μ ↔ integrable_on f s μ ∧ integrable_on f t μ :=
 ⟨λ h, ⟨h.left_of_union, h.right_of_union⟩, λ h, h.1.union h.2⟩
 
-@[simp] lemma integrable_on_finite_union {s : set β} (hs : finite s) {t : β → set α} :
-  integrable_on f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, integrable_on f (t i) μ :=
+@[simp] lemma integrable_on_finite_union (hf : measurable f) {s : set β} (hs : finite s)
+  {t : β → set α} : integrable_on f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, integrable_on f (t i) μ :=
 begin
   apply hs.induction_on,
-  { simp },
-  { intros a s ha hs hf,
-    simp [hf, or_imp_distrib, forall_and_distrib] }
+  { simp [hf] },
+  { intros a s ha hs hf, simp [hf, or_imp_distrib, forall_and_distrib] }
 end
 
-@[simp] lemma integrable_on_finset_union {s : finset β} {t : β → set α} :
+@[simp] lemma integrable_on_finset_union (hf : measurable f) {s : finset β} {t : β → set α} :
   integrable_on f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, integrable_on f (t i) μ :=
-integrable_on_finite_union s.finite_to_set
+integrable_on_finite_union hf s.finite_to_set
 
 lemma integrable_on.add_measure (hμ : integrable_on f s μ) (hν : integrable_on f s ν) :
   integrable_on f s (μ + ν) :=
@@ -170,19 +175,14 @@ by { delta integrable_on, rw measure.restrict_add, exact hμ.integrable.add_meas
   h.mono_measure (measure.le_add_left (le_refl _))⟩,
   λ h, h.1.add_measure h.2⟩
 
-lemma integrable_indicator_iff (hs : is_measurable s) :
+lemma integrable_indicator_iff (hf : measurable f) (hs : is_measurable s) :
   integrable (indicator s f) μ ↔ integrable_on f s μ :=
-by simp only [integrable_on, integrable, nnnorm_indicator_eq_indicator_nnnorm,
-  ennreal.coe_indicator, lintegral_indicator _ hs]
+by simp only [integrable_on, integrable, has_finite_integral, nnnorm_indicator_eq_indicator_nnnorm,
+  ennreal.coe_indicator, lintegral_indicator _ hs, hf, hf.indicator hs]
 
 lemma integrable_on.indicator (h : integrable_on f s μ) (hs : is_measurable s) :
   integrable (indicator s f) μ :=
-(integrable_indicator_iff hs).2 h
-
-lemma integrable_on_of_bounded {C} (hs : μ s < ⊤) (hf : ∀ᵐ x ∂(μ.restrict s), ∥f x∥ ≤ C) :
-  integrable_on f s μ :=
-by haveI : finite_measure (μ.restrict s) := ⟨by rwa [measure.restrict_apply_univ]⟩;
-  exact integrable_of_bounded hf
+(integrable_indicator_iff h.measurable hs).2 h
 
 /-- We say that a function `f` is *integrable at filter* `l` if it is integrable on some
 set `s ∈ l`. Equivalently, it is eventually integrable on `s` in `l.lift' powerset`. -/
@@ -223,7 +223,8 @@ alias integrable_at_filter.inf_ae_iff ↔ measure_theory.integrable_at_filter.of
 
 /-- If `μ` is a measure finite at filter `l` and `f` is a function such that its norm is bounded
 above at `l`, then `f` is integrable at `l`. -/
-lemma measure.finite_at_filter.integrable_at_filter {l : filter α} [is_measurably_generated l]
+lemma measure.finite_at_filter.integrable_at_filter (hfm : measurable f)
+  {l : filter α} [is_measurably_generated l]
   (hμ : μ.finite_at_filter l) (hf : l.is_bounded_under (≤) (norm ∘ f)) :
   integrable_at_filter f l μ :=
 begin
@@ -232,7 +233,8 @@ begin
   simp only [eventually_map] at hC,
   rcases hC.exists_measurable_mem with ⟨t, htl, htm, hC⟩,
   refine ⟨t ∩ s, inter_mem_sets htl hsl, _⟩,
-  refine integrable_on_of_bounded (lt_of_le_of_lt (measure_mono $ inter_subset_right _ _) hsμ) _,
+  refine ⟨hfm, has_finite_integral_restrict_of_bounded
+    (lt_of_le_of_lt (measure_mono $ inter_subset_right _ _) hsμ) _⟩,
   exact C,
   suffices : ∀ᵐ x ∂μ.restrict t, ∥f x∥ ≤ C,
     from ae_mono (measure.restrict_mono (inter_subset_left _ _) (le_refl _)) this,
@@ -240,40 +242,37 @@ begin
   exact eventually_of_forall hC
 end
 
-lemma measure.finite_at_filter.integrable_at_filter_of_tendsto_ae
+lemma measure.finite_at_filter.integrable_at_filter_of_tendsto_ae (hfm : measurable f)
   {l : filter α} [is_measurably_generated l] (hμ : μ.finite_at_filter l) {b}
   (hf : tendsto f (l ⊓ μ.ae) (𝓝 b)) :
   integrable_at_filter f l μ :=
-(hμ.inf_of_left.integrable_at_filter hf.norm.is_bounded_under_le).of_inf_ae
+(hμ.inf_of_left.integrable_at_filter hfm hf.norm.is_bounded_under_le).of_inf_ae
 
 alias measure.finite_at_filter.integrable_at_filter_of_tendsto_ae ←
   filter.tendsto.integrable_at_filter_ae
 
-lemma measure.finite_at_filter.integrable_at_filter_of_tendsto
+lemma measure.finite_at_filter.integrable_at_filter_of_tendsto (hfm : measurable f)
   {l : filter α} [is_measurably_generated l] (hμ : μ.finite_at_filter l) {b}
   (hf : tendsto f l (𝓝 b)) :
   integrable_at_filter f l μ :=
-hμ.integrable_at_filter hf.norm.is_bounded_under_le
+hμ.integrable_at_filter hfm hf.norm.is_bounded_under_le
 
 alias measure.finite_at_filter.integrable_at_filter_of_tendsto ← filter.tendsto.integrable_at_filter
 
-variables [measurable_space E]
+variables [borel_space E] [second_countable_topology E]
 
 lemma integrable_add [opens_measurable_space E] {f g : α → E}
-  (h : univ ⊆ f ⁻¹' {0} ∪ g ⁻¹' {0})
-  (hf : measurable f) (hg : measurable g) :
+  (h : univ ⊆ f ⁻¹' {0} ∪ g ⁻¹' {0}) (hf : measurable f) (hg : measurable g) :
   integrable (f + g) μ ↔ integrable f μ ∧ integrable g μ :=
 begin
-  refine ⟨λ hfg, _, λ h, h.1.add hf hg h.2⟩,
+  refine ⟨λ hfg, _, λ h, h.1.add h.2⟩,
   rw [← indicator_add_eq_left h],
   conv { congr, skip, rw [← indicator_add_eq_right h] },
-  rw [integrable_indicator_iff (hf (is_measurable_singleton 0)).compl],
-  rw [integrable_indicator_iff (hg (is_measurable_singleton 0)).compl],
-  exact ⟨hfg.integrable_on, hfg.integrable_on⟩
+  rw [integrable_indicator_iff _ (hf (is_measurable_singleton 0)).compl],
+  rw [integrable_indicator_iff _ (hg (is_measurable_singleton 0)).compl],
+  exact ⟨hfg.integrable_on, hfg.integrable_on⟩, exact hf.add hg, exact hf.add hg
 end
 
-variables [borel_space E] [second_countable_topology E]
-
 /-- To prove something for an arbitrary measurable + integrable function in a second countable
 Borel normed group, it suffices to show that
 * the property holds for (multiples of) characteristic functions;
@@ -289,11 +288,11 @@ of their images is a subset of `{0}`).
 @[elab_as_eliminator]
 lemma integrable.induction (P : (α → E) → Prop)
   (h_ind : ∀ (c : E) ⦃s⦄, is_measurable s → μ s < ⊤ → P (s.indicator (λ _, c)))
-  (h_sum : ∀ ⦃f g : α → E⦄, set.univ ⊆ f ⁻¹' {0} ∪ g ⁻¹' {0} → measurable f → measurable g →
-    integrable f μ → integrable g μ → P f → P g → P (f + g))
+  (h_sum : ∀ ⦃f g : α → E⦄, set.univ ⊆ f ⁻¹' {0} ∪ g ⁻¹' {0} → integrable f μ → integrable g μ →
+    P f → P g → P (f + g))
   (h_closed : is_closed {f : α →₁[μ] E | P f} )
-  (h_ae : ∀ ⦃f g⦄, f =ᵐ[μ] g → measurable f → measurable g → integrable f μ → P f → P g) :
-  ∀ ⦃f : α → E⦄ (hf : measurable f) (h2f : integrable f μ), P f :=
+  (h_ae : ∀ ⦃f g⦄, f =ᵐ[μ] g → integrable f μ → measurable g → P f → P g) :
+  ∀ ⦃f : α → E⦄ (hf : integrable f μ), P f :=
 begin
   have : ∀ (f : simple_func α E), integrable f μ → P f,
   { refine simple_func.induction _ _,
@@ -304,18 +303,19 @@ begin
       apply h_ind c hs,
       have : (nnnorm c : ennreal) * μ s < ⊤,
       { have := @comp_indicator _ _ _ _ (λ x : E, (nnnorm x : ennreal)) (const α c) s,
-        dsimp only at this, simpa [integrable, this, lintegral_indicator, hs] using h },
+        dsimp only at this,
+        have h' := h.has_finite_integral,
+        simpa [has_finite_integral, this, lintegral_indicator, hs] using h' },
       exact ennreal.lt_top_of_mul_lt_top_right this (by simp [hc]) },
     { intros f g hfg hf hg int_fg,
       rw [simple_func.coe_add, integrable_add hfg f.measurable g.measurable] at int_fg,
-      refine h_sum hfg f.measurable g.measurable int_fg.1 int_fg.2 (hf int_fg.1) (hg int_fg.2) } },
+      refine h_sum hfg int_fg.1 int_fg.2 (hf int_fg.1) (hg int_fg.2) } },
   have : ∀ (f : α →₁ₛ[μ] E), P f,
-  { intro f, exact h_ae f.to_simple_func_eq_to_fun f.measurable (l1.measurable _) f.integrable
+  { intro f, exact h_ae f.to_simple_func_eq_to_fun f.integrable (l1.measurable _)
       (this f.to_simple_func f.integrable) },
   have : ∀ (f : α →₁[μ] E), P f :=
     λ f, l1.simple_func.dense_range.induction_on f h_closed this,
-  exact λ f hf h2f, h_ae (l1.to_fun_of_fun f hf h2f) (l1.measurable _) hf (l1.integrable _)
-    (this (l1.of_fun f hf h2f))
+  exact λ f hf, h_ae (l1.to_fun_of_fun f hf) (l1.integrable _) hf.measurable (this (l1.of_fun f hf))
 end
 
 variables [complete_space E] [normed_space ℝ E]
@@ -347,7 +347,7 @@ calc ∫ x, indicator s f x ∂μ = ∫ x in s, indicator s f x ∂μ + ∫ x in
     (integral_congr_ae hfms measurable_const (indicator_ae_eq_restrict_compl hs))
 ... = ∫ x in s, f x ∂μ : by simp
 else
-by { rwa [integral_non_integrable, integral_non_integrable], rwa integrable_indicator_iff hs }
+by { rwa [integral_undef, integral_undef], rwa integrable_indicator_iff hfm hs }
 
 lemma set_integral_const (c : E) : ∫ x in s, c ∂μ = (μ s).to_real • c :=
 by rw [integral_const, measure.restrict_apply_univ]
@@ -397,13 +397,14 @@ end measure_theory
 
 open measure_theory asymptotics metric
 
+variables [measurable_space E] [normed_group E]
+
 /-- Fundamental theorem of calculus for set integrals: if `μ` is a measure that is finite
 at a filter `l` and `f` is a measurable function that has a finite limit `b` at `l ⊓ μ.ae`,
 then `∫ x in s, f x ∂μ = μ s • b + o(μ s)` as `s` tends to `l.lift' powerset`. Since `μ s` is
 an `ennreal` number, we use `(μ s).to_real` in the actual statement. -/
 lemma filter.tendsto.integral_sub_linear_is_o_ae
-  [normed_group E] [normed_space ℝ E] [second_countable_topology E] [complete_space E]
-  [measurable_space E] [borel_space E]
+  [normed_space ℝ E] [second_countable_topology E] [complete_space E] [borel_space E]
   {μ : measure α} {l : filter α} [l.is_measurably_generated]
   {f : α → E} {b : E} (h : tendsto f (l ⊓ μ.ae) (𝓝 b)) (hfm : measurable f)
   (hμ : μ.finite_at_filter l) :
@@ -414,42 +415,42 @@ begin
   intros ε ε₀,
   have : ∀ᶠ s in l.lift' powerset, ∀ᶠ x in μ.ae, x ∈ s → f x ∈ closed_ball b ε :=
     eventually_lift'_powerset_eventually.2 (h.eventually $ closed_ball_mem_nhds _ ε₀),
-  refine hμ.eventually.mp ((h.integrable_at_filter_ae hμ).eventually.mp (this.mono _)),
+  refine hμ.eventually.mp ((h.integrable_at_filter_ae hfm hμ).eventually.mp (this.mono _)),
   simp only [mem_closed_ball, dist_eq_norm],
   intros s h_norm h_integrable hμs,
-  rw [← set_integral_const, ← integral_sub hfm h_integrable measurable_const
-    (integrable_on_const.2 $ or.inr hμs), real.norm_eq_abs, abs_of_nonneg ennreal.to_real_nonneg],
+  rw [← set_integral_const, ← integral_sub h_integrable (integrable_on_const.2 $ or.inr hμs),
+    real.norm_eq_abs, abs_of_nonneg ennreal.to_real_nonneg],
   exact norm_set_integral_le_of_norm_le_const_ae' hμs h_norm (hfm.sub measurable_const)
 end
 
 /-- If a function is integrable at `𝓝[s] x` for each point `x` of a compact set `s`, then it is
 integrable on `s`. -/
-lemma is_compact.integrable_on_of_nhds_within
-  [topological_space α] [normed_group E] {μ : measure α} {s : set α} (hs : is_compact s)
-  {f : α → E} (hf : ∀ x ∈ s, integrable_at_filter f (𝓝[s] x) μ) :
+lemma is_compact.integrable_on_of_nhds_within [topological_space α] {μ : measure α} {s : set α}
+  (hs : is_compact s) {f : α → E} (hfm : measurable f)
+  (hf : ∀ x ∈ s, integrable_at_filter f (𝓝[s] x) μ) :
   integrable_on f s μ :=
-is_compact.induction_on hs integrable_on_empty (λ s t hst ht, ht.mono_set hst)
+is_compact.induction_on hs (integrable_on_empty hfm) (λ s t hst ht, ht.mono_set hst)
   (λ s t hs ht, hs.union ht) hf
 
 /-- A function `f` continuous on a compact set `s` is integrable on this set with respect to any
 locally finite measure. -/
-lemma continuous_on.integrable_on_compact
-  [topological_space α] [opens_measurable_space α] [t2_space α]
-  [normed_group E] {μ : measure α} [locally_finite_measure μ] {s : set α} (hs : is_compact s)
-  {f : α → E} (hf : continuous_on f s) :
+lemma continuous_on.integrable_on_compact [topological_space α] [opens_measurable_space α]
+  [t2_space α] {μ : measure α} [locally_finite_measure μ]
+  {s : set α} (hs : is_compact s)
+  {f : α → E} (hfm : measurable f) (hf : continuous_on f s) :
   integrable_on f s μ :=
-hs.integrable_on_of_nhds_within $ λ x hx,
+hs.integrable_on_of_nhds_within hfm $ λ x hx,
   by haveI := hs.is_measurable.nhds_within_is_measurably_generated;
-    exact (hf x hx).integrable_at_filter (μ.finite_at_nhds_within _ _)
+    exact (hf x hx).integrable_at_filter hfm (μ.finite_at_nhds_within _ _)
 
 /-- A continuous function `f` is integrable on any compact set with respect to any locally finite
 measure. -/
 lemma continuous.integrable_on_compact
   [topological_space α] [opens_measurable_space α] [t2_space α]
-  [normed_group E] {μ : measure α} [locally_finite_measure μ] {s : set α} (hs : is_compact s)
-  {f : α → E} (hf : continuous f) :
+  [borel_space E] {μ : measure α} [locally_finite_measure μ] {s : set α}
+  (hs : is_compact s) {f : α → E} (hf : continuous f) :
   integrable_on f s μ :=
-hf.continuous_on.integrable_on_compact hs
+hf.continuous_on.integrable_on_compact hs hf.measurable
 
 /-- Fundamental theorem of calculus for set integrals, `nhds` version: if `μ` is a locally finite
 measure that and `f` is a measurable function that is continuous at a point `a`,
@@ -457,8 +458,8 @@ then `∫ x in s, f x ∂μ = μ s • f a + o(μ s)` as `s` tends to `(𝓝 a).
 Since `μ s` is an `ennreal` number, we use `(μ s).to_real` in the actual statement. -/
 lemma continuous_at.integral_sub_linear_is_o_ae
   [topological_space α] [opens_measurable_space α]
-  [normed_group E] [normed_space ℝ E] [second_countable_topology E] [complete_space E]
-  [measurable_space E] [borel_space E]
+  [normed_space ℝ E] [second_countable_topology E] [complete_space E]
+  [borel_space E]
   {μ : measure α} [locally_finite_measure μ] {a : α}
   {f : α → E} (ha : continuous_at f a) (hfm : measurable f) :
   is_o (λ s, ∫ x in s, f x ∂μ - (μ s).to_real • f a) (λ s, (μ s).to_real) ((𝓝 a).lift' powerset) :=
@@ -483,40 +484,39 @@ Then we can prove the commutation result using continuity of all relevant operat
 and the result on simple functions.
 -/
 
-variables {μ : measure α} [normed_group E] [normed_space ℝ E] [normed_group F]  [normed_space ℝ F]
+variables {μ : measure α} [normed_space ℝ E]
+variables [normed_group F] [normed_space ℝ F]
 
 namespace continuous_linear_map
 
-lemma integrable_comp {φ : α → E} (L : E →L[ℝ] F) (φ_int : integrable φ μ) :
-  integrable (λ (a : α), L (φ a)) μ :=
-((integrable.norm φ_int).const_mul ∥L∥).mono' (eventually_of_forall $ λ a, L.le_op_norm (φ a))
+lemma norm_comp_l1_apply_le [opens_measurable_space E] [second_countable_topology E] (φ : α →₁[μ] E)
+  (L : E →L[ℝ] F) : ∀ᵐ a ∂μ, ∥L (φ a)∥ ≤ ∥L∥ * ∥φ a∥ :=
+eventually_of_forall (λ a, L.le_op_norm (φ a))
 
-variables [second_countable_topology E] [measurable_space E] [borel_space E]
+variables [measurable_space F] [borel_space F]
 
-lemma norm_comp_l1_apply_le (φ : α →₁[μ] E) (L : E →L[ℝ] F) : ∀ᵐ a ∂μ, ∥L (φ a)∥ ≤ ∥L∥*∥φ a∥ :=
-eventually_of_forall (λ a, L.le_op_norm (φ a))
+lemma integrable_comp [opens_measurable_space E] {φ : α → E} (L : E →L[ℝ] F)
+  (φ_int : integrable φ μ) : integrable (λ (a : α), L (φ a)) μ :=
+((integrable.norm φ_int).const_mul ∥L∥).mono' (L.measurable.comp φ_int.measurable)
+  (eventually_of_forall $ λ a, L.le_op_norm (φ a))
 
-section
-variables [measurable_space F] [borel_space F] [second_countable_topology F]
+variables [borel_space E] [second_countable_topology E]
 
 /-- Composing `φ : α →₁[μ] E` with `L : E →L[ℝ] F`. -/
-def comp_l1 (L : E →L[ℝ] F) (φ : α →₁[μ] E) : α →₁[μ] F :=
-l1.of_fun (λ a, L (φ a)) (L.measurable_comp φ.measurable) (L.integrable_comp φ.integrable)
+def comp_l1 [second_countable_topology F] (L : E →L[ℝ] F) (φ : α →₁[μ] E) : α →₁[μ] F :=
+l1.of_fun (λ a, L (φ a)) (L.integrable_comp φ.integrable)
 
-lemma comp_l1_apply (L : E →L[ℝ] F) (φ : α →₁[μ] E) : ∀ᵐ a ∂μ, (L.comp_l1 φ) a = L (φ a) :=
-l1.to_fun_of_fun _ _ _
-
-end
+lemma comp_l1_apply [second_countable_topology F] (L : E →L[ℝ] F) (φ : α →₁[μ] E) :
+  ∀ᵐ a ∂μ, (L.comp_l1 φ) a = L (φ a) :=
+l1.to_fun_of_fun _ _
 
 lemma integrable_comp_l1 (L : E →L[ℝ] F) (φ : α →₁[μ] E) : integrable (λ a, L (φ a)) μ :=
 L.integrable_comp φ.integrable
 
-variables [measurable_space F]
-
-lemma measurable_comp_l1 [borel_space F] (L : E →L[ℝ] F) (φ : α →₁[μ] E) :
+lemma measurable_comp_l1 (L : E →L[ℝ] F) (φ : α →₁[μ] E) :
   measurable (λ a, L (φ a)) := L.measurable.comp φ.measurable
 
-variables [borel_space F] [second_countable_topology F]
+variables [second_countable_topology F]
 
 lemma integral_comp_l1 [complete_space F] (L : E →L[ℝ] F) (φ : α →₁[μ] E) :
   ∫ a, (L.comp_l1 φ) a ∂μ = ∫ a, L (φ a) ∂μ :=
@@ -546,8 +546,7 @@ lemma norm_comp_l1_le (φ : α →₁[μ] E) (L : E →L[ℝ] F) : ∥L.comp_l1
 begin
   erw l1.norm_of_fun_eq_integral_norm,
   calc
-  ∫ a, ∥L (φ a)∥ ∂μ ≤ ∫ a, ∥L∥ *∥φ a∥ ∂μ : integral_mono (L.measurable.comp φ.measurable).norm
-                                (L.integrable_comp_l1 φ).norm (φ.measurable_norm.const_mul $ ∥L∥)
+  ∫ a, ∥L (φ a)∥ ∂μ ≤ ∫ a, ∥L∥ *∥φ a∥ ∂μ : integral_mono (L.integrable_comp_l1 φ).norm
                                 (φ.integrable_norm.const_mul $ ∥L∥) (L.norm_comp_l1_apply_le φ)
   ... = ∥L∥ * ∥φ∥ : by rw [integral_mul_left, φ.norm_eq_integral_norm]
 end
@@ -571,8 +570,8 @@ end
 
 variables [complete_space E]
 
-lemma integral_comp_comm (L : E →L[ℝ] F) {φ : α → E} (φ_meas : measurable φ)
-  (φ_int : integrable φ μ) : ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) :=
+lemma integral_comp_comm (L : E →L[ℝ] F) {φ : α → E} (φ_int : integrable φ μ) :
+  ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) :=
 begin
   apply integrable.induction (λ φ, ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ)),
   { intros e s s_meas s_finite,
@@ -580,21 +579,20 @@ begin
         ← integral_indicator_const (L e) s_meas],
     congr' 1 with a,
     rw set.indicator_comp_of_zero L.map_zero },
-  { intros f g H f_meas g_meas f_int g_int hf hg,
-    simp [L.map_add, integral_add f_meas f_int g_meas g_int,
-      integral_add (L.measurable_comp f_meas) (L.integrable_comp f_int)
-      (L.measurable_comp g_meas) (L.integrable_comp g_int), hf, hg] },
+  { intros f g H f_int g_int hf hg,
+    simp [L.map_add, integral_add f_int g_int,
+      integral_add (L.integrable_comp f_int) (L.integrable_comp g_int), hf, hg] },
   { exact is_closed_eq L.continuous_integral_comp_l1 (L.continuous.comp continuous_integral) },
-  { intros f g hfg f_meas g_meas f_int hf,
+  { intros f g hfg f_int g_meas hf,
     convert hf using 1 ; clear hf,
-    { exact integral_congr_ae (L.measurable.comp g_meas) (L.measurable.comp f_meas) (hfg.fun_comp L).symm },
-    { rw integral_congr_ae g_meas f_meas hfg.symm } },
+    { exact integral_congr_ae (L.measurable.comp g_meas) (L.measurable.comp f_int.measurable)
+        (hfg.fun_comp L).symm },
+    { rw integral_congr_ae g_meas f_int.measurable hfg.symm } },
   all_goals { assumption }
 end
 
-lemma integral_comp_l1_comm (L : E →L[ℝ] F) (φ : α →₁[μ] E) :
-  ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) :=
-L.integral_comp_comm φ.measurable φ.integrable
+lemma integral_comp_l1_comm (L : E →L[ℝ] F) (φ : α →₁[μ] E) : ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) :=
+L.integral_comp_comm φ.integrable
 
 end continuous_linear_map
 
diff --git a/src/measure_theory/simple_func_dense.lean b/src/measure_theory/simple_func_dense.lean
index 65b0c890b5a91..967c310e58e17 100644
--- a/src/measure_theory/simple_func_dense.lean
+++ b/src/measure_theory/simple_func_dense.lean
@@ -42,7 +42,7 @@ let A' (N k : ℕ) : set α :=
   f ⁻¹' (metric.ball (e k) (1 / (N+1 : ℝ)) \ metric.ball 0 (1 / (N+1 : ℝ))) in
 let A N := disjointed (A' N) in
 have is_measurable_A' : ∀ {N k}, is_measurable (A' N k) :=
-  λ N k, hf $ is_measurable.inter is_measurable_ball $ is_measurable.compl is_measurable_ball,
+  λ N k, hf $ is_measurable_ball.inter is_measurable_ball.compl,
 have is_measurable_A : ∀ {N k}, is_measurable (A N k) :=
   λ N, is_measurable.disjointed $ λ k, is_measurable_A',
 have A_subset_A' : ∀ {N k x}, x ∈ A N k → x ∈ A' N k := λ N k, inter_subset_left _ _,
@@ -236,17 +236,16 @@ classical.by_cases
   have F_eq_0 : F N x = 0 := if_neg h,
   by { simp only [F_eq_0, norm_zero], exact add_nonneg (norm_nonneg _) (norm_nonneg _) } )⟩⟩
 
-lemma simple_func_sequence_tendsto' {μ : measure α} {f : α → β} (hfm : measurable f)
-  (hfi : integrable f μ) :
+lemma simple_func_sequence_tendsto' {μ : measure α} {f : α → β} (hf : integrable f μ) :
     ∃ (F : ℕ → (α →ₛ β)), (∀n, integrable (F n) μ) ∧
    tendsto (λ n, ∫⁻ x,  nndist (F n x) (f x) ∂μ) at_top (𝓝 0) :=
-let ⟨F, hF⟩ := simple_func_sequence_tendsto hfm in
+let ⟨F, hF⟩ := simple_func_sequence_tendsto hf.measurable in
 let G : ℕ → α → ennreal := λn x, nndist (F n x) (f x) in
 let g : α → ennreal := λx, nnnorm (f x) + nnnorm (f x) + nnnorm (f x) in
-have hF_meas : ∀ n, measurable (G n) := λ n, measurable.comp measurable_coe $
-  (F n).measurable.nndist hfm,
-have hg_meas : measurable g := measurable.comp measurable_coe $ measurable.add
-  (measurable.add hfm.nnnorm hfm.nnnorm) hfm.nnnorm,
+have hF_meas : ∀ n, measurable (G n) := λ n, measurable_coe.comp $
+  (F n).measurable.nndist hf.measurable,
+have hg_meas : measurable g := measurable_coe.comp $
+  (hf.measurable.nnnorm.add hf.measurable.nnnorm).add hf.measurable.nnnorm,
 have h_bound : ∀ n, G n ≤ᵐ[μ] g := λ n, ae_of_all _ $ λ x, coe_le_coe.2 $
   calc
     nndist (F n x) (f x) ≤ nndist (F n x) 0 + nndist 0 (f x) : nndist_triangle _ _ _
@@ -257,9 +256,9 @@ have h_finite : ∫⁻ x, g x ∂μ < ⊤ :=
   calc
     ∫⁻ x, nnnorm (f x) + nnnorm (f x) + nnnorm (f x) ∂μ =
       ∫⁻ x, nnnorm (f x) ∂μ + ∫⁻ x, nnnorm (f x) ∂μ + ∫⁻ x, nnnorm (f x) ∂μ :
-    by { rw [lintegral_add, lintegral_nnnorm_add],
-      exacts [hfm, hfm, hfm.ennnorm.add hfm.ennnorm, hfm.ennnorm] }
-    ... < ⊤ : by { simp only [and_self, add_lt_top], exact hfi},
+    by { rw [lintegral_add, lintegral_nnnorm_add hf.measurable hf.measurable],
+      exacts [hf.measurable.ennnorm.add hf.measurable.ennnorm, hf.measurable.ennnorm] }
+    ... < ⊤ : by { simp only [and_self, add_lt_top], exact hf.has_finite_integral },
 have h_lim : ∀ᵐ x ∂μ, tendsto (λ n, G n x) at_top (𝓝 0) := ae_of_all _ $ λ x,
   begin
     apply (@tendsto_coe ℕ at_top (λ n, nndist (F n x) (f x)) 0).2,
@@ -268,14 +267,14 @@ have h_lim : ∀ᵐ x ∂μ, tendsto (λ n, G n x) at_top (𝓝 0) := ae_of_all
   end,
 begin
   use F, split,
-  { assume n,
+  { assume n, use (F n).measurable,
     calc
       ∫⁻ a, nnnorm (F n a) ∂μ ≤ ∫⁻ a, nnnorm (f a) + nnnorm (f a) ∂μ :
         lintegral_mono
           (by { assume a, simp only [coe_add.symm, coe_le_coe], exact (hF a).2 n })
        ... = ∫⁻ a, nnnorm (f a) ∂μ + ∫⁻ a, nnnorm (f a) ∂μ :
-         lintegral_nnnorm_add hfm hfm
-       ... < ⊤ : by simp only [add_lt_top, and_self]; exact hfi },
+         lintegral_nnnorm_add hf.measurable hf.measurable
+       ... < ⊤ : by simp only [add_lt_top, and_self]; exact hf.has_finite_integral },
   convert tendsto_lintegral_of_dominated_convergence g hF_meas h_bound h_finite h_lim,
   simp only [lintegral_zero]
 end