chore(measure_theory/bochner_integration): make proofs shorter (#1871)

* More consistent use of the dot notation

* Revert "More consistent use of the dot notation"

This reverts commit 854a499.

* Revert "Revert "More consistent use of the dot notation""

This reverts commit 57aaf22.

* fix things

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/measure_theory/ae_eq_fun.lean

@@ -347,11 +347,11 @@ variables {γ : Type*} [topological_space γ]
           [add_comm_monoid γ] [semimodule 𝕜 γ] [topological_semimodule 𝕜 γ]
 
 protected def smul : 𝕜 → (α →ₘ γ) → (α →ₘ γ) :=
-λ c f, comp (has_scalar.smul c) (measurable_smul _ measurable_id) f
+λ c f, comp (has_scalar.smul c) (measurable.smul _ measurable_id) f
 
 instance : has_scalar 𝕜 (α →ₘ γ) := ⟨ae_eq_fun.smul⟩
 
-@[simp] lemma smul_mk (c : 𝕜) (f : α → γ) (hf) : c • (mk f hf) = mk (c • f) (measurable_smul _ hf) :=
+@[simp] lemma smul_mk (c : 𝕜) (f : α → γ) (hf) : c • (mk f hf) = mk (c • f) (measurable.smul _ hf) :=
 rfl
 
 lemma smul_to_fun (c : 𝕜) (f : α →ₘ γ) : ∀ₘ a, (c • f).to_fun a = c • f.to_fun a :=
@@ -440,7 +440,7 @@ section
 variables {γ : Type*} [emetric_space γ] [second_countable_topology γ]
 
 /-- `comp_edist [f] [g] a` will return `edist (f a) (g a) -/
-def comp_edist (f g : α →ₘ γ) : α →ₘ ennreal := comp₂ edist measurable_edist' f g
+def comp_edist (f g : α →ₘ γ) : α →ₘ ennreal := comp₂ edist measurable_edist f g
 
 lemma comp_edist_to_fun (f g : α →ₘ γ) :
   ∀ₘ a, (comp_edist f g).to_fun a = edist (f.to_fun a) (g.to_fun a) :=
@@ -528,7 +528,7 @@ begin
   exact calc
     (∫⁻ (a : α), nndist (x • f a) 0) = (∫⁻ (a : α), (nnnorm x) * nnnorm (f a)) :
       lintegral_congr_ae $ by { filter_upwards [], assume a, simp [nndist_eq_nnnorm, nnnorm_smul] }
-    ... = _ : lintegral_const_mul _ (measurable_coe_nnnorm hf)
+    ... = _ : lintegral_const_mul _ (measurable.coe_nnnorm hf)
     ... = _ :
     begin
       convert rfl,

src/measure_theory/bochner_integration.lean

@@ -177,7 +177,7 @@ local infixr ` →ₛ `:25 := simple_func
 namespace simple_func
 
 section bintegral
-/-! 
+/-!
 ### The Bochner integral of simple functions
 
 Define the Bochner integral of simple functions of the type `α →ₛ β` where `β` is a normed group,
@@ -408,7 +408,7 @@ variables [normed_group β] [second_countable_topology β]
 variables (α β)
 /-- `l1.simple_func` is a subspace of L1 consisting of equivalence classes of an integrable simple
     function. -/
-def simple_func : Type* :=
+def simple_func : Type (max u v) :=
 { f : α →₁ β // ∃ (s : α →ₛ β),  integrable s ∧ ae_eq_fun.mk s s.measurable = f}
 
 variables {α β}
@@ -1033,117 +1033,81 @@ if hf : measurable f ∧ integrable f
 then (l1.of_fun f hf.1 hf.2).integral
 else 0
 
-notation `∫` binders `, ` r:(scoped f, integral f) := r
+local notation `∫` binders `, ` r:(scoped f, integral f) := r
 
 section properties
 
 open continuous_linear_map measure_theory.simple_func
 
 variables {f g : α → β}
 
-lemma integral_eq (f : α → β) : integral f =
-  if hf : measurable f ∧ integrable f then (l1.of_fun f hf.1 hf.2).integral else 0 := rfl
+lemma integral_eq (f : α → β) (h₁ : measurable f) (h₂ : integrable f) :
+  integral f = (l1.of_fun f h₁ h₂).integral :=
+dif_pos ⟨h₁, h₂⟩
+
+lemma integral_undef (h : ¬ (measurable f ∧ integrable f)) : integral f = 0 :=
+dif_neg h
 
-lemma integral_eq_zero_of_non_measurable (h : ¬ measurable f) : integral f = 0 :=
-by { rw [integral, dif_neg], rw not_and_distrib, exact or.inl h }
+lemma integral_non_integrable (h : ¬ integrable f) : integral f = 0 :=
+integral_undef $ not_and_of_not_right _ h
 
-lemma integral_eq_zero_of_non_integrable (h : ¬ integrable f) : integral f = 0 :=
-by { rw [integral, dif_neg], rw not_and_distrib, exact or.inr h }
+lemma integral_non_measurable (h : ¬ measurable f) : integral f = 0 :=
+integral_undef $ not_and_of_not_left _ h
 
 variables (α β)
 @[simp] lemma integral_zero : integral (0 : α → β) = 0 :=
-begin
-  simp only [integral], rw dif_pos,
-  { apply l1.integral_zero },
-  { exact ⟨(measurable_const : measurable (λb:α, (0:β))), integrable_zero⟩ }
-end
+by rw [integral_eq, l1.of_fun_zero, l1.integral_zero]
+
 variables {α β}
 
-lemma integral_add (hfm : measurable f) (hfi : integrable f) (hgm : measurable g)
-  (hgi : integrable g) : integral (f + g) = integral f + integral g :=
-begin
-  simp only [integral], repeat { rw dif_pos },
-  { rw ← l1.integral_add, refl },
-  { exact ⟨hgm, hgi⟩ },
-  { exact ⟨hfm, hfi⟩ },
-  { exact ⟨measurable.add hfm hgm, integrable.add hfm hgm hfi hgi⟩ }
-end
+lemma integral_add
+  (hfm : measurable f) (hfi : integrable f) (hgm : measurable g) (hgi : integrable g) :
+  integral (f + g) = integral f + integral g :=
+by rw [integral_eq, integral_eq f hfm hfi, integral_eq g hgm hgi, l1.of_fun_add, l1.integral_add]
 
 lemma integral_neg (f : α → β) : integral (-f) = - integral f :=
 begin
-  simp only [integral],
-  by_cases hfm : measurable f, by_cases hfi : integrable f,
-  { repeat { rw dif_pos },
-    { rw ← l1.integral_neg, refl },
-    { exact ⟨hfm, hfi⟩ },
-    { exact ⟨measurable.neg hfm, integrable.neg hfi⟩ } },
-  { repeat { rw dif_neg },
-    { rw neg_zero },
-    { rw not_and_distrib, exact or.inr hfi },
-    { rw not_and_distrib, rw integrable_neg_iff, exact or.inr hfi } },
-  { repeat { rw dif_neg },
-    { rw neg_zero },
-    { rw not_and_distrib, exact or.inl hfm },
-    { rw not_and_distrib, rw measurable_neg_iff, exact or.inl hfm } }
+  by_cases hf : measurable f ∧ integrable f,
+  { rw [integral_eq f hf.1 hf.2, integral_eq (- f) hf.1.neg hf.2.neg, l1.of_fun_neg,
+    l1.integral_neg] },
+  { have hf' : ¬(measurable (-f) ∧ integrable (-f)),
+    { rwa [measurable_neg_iff, integrable_neg_iff] },
+    rw [integral_undef hf, integral_undef hf', neg_zero] }
 end
 
-lemma integral_sub (hfm : measurable f) (hfi : integrable f) (hgm : measurable g)
-  (hgi : integrable g) : integral (f - g) = integral f - integral g :=
-begin
-  simp only [integral], repeat {rw dif_pos},
-  { rw ← l1.integral_sub, refl },
-  { exact ⟨hgm, hgi⟩ },
-  { exact ⟨hfm, hfi⟩ },
-  { exact ⟨measurable.sub hfm hgm, integrable.sub hfm hgm hfi hgi⟩ }
-end
+lemma integral_sub
+  (hfm : measurable f) (hfi : integrable f) (hgm : measurable g) (hgi : integrable g) :
+  integral (f - g) = integral f - integral g :=
+by simp only [sub_eq_add_neg, integral_neg, integral_add, measurable_neg_iff, integrable_neg_iff, *]
 
-lemma integral_smul (r : ℝ) (f : α → β) : (∫ x, r • (f x)) = r • integral f :=
+lemma integral_smul (r : ℝ) (f : α → β) : integral (r • f) = r • integral f :=
 begin
-  by_cases r0 : r = 0,
-  { have : (λx, r • (f x)) = 0, { funext, rw [r0, zero_smul, pi.zero_apply] },
-    rw [this, r0, zero_smul], apply integral_zero },
-  simp only [integral],
-  by_cases hfm : measurable f, by_cases hfi : integrable f,
-  { rw dif_pos, rw dif_pos,
-    { rw ← l1.integral_smul, refl  },
-    { exact ⟨hfm, hfi⟩ },
-    { exact ⟨measurable_smul _ hfm, integrable.smul _ hfi⟩ } },
-  { repeat { rw dif_neg },
-    { rw smul_zero },
-    { rw not_and_distrib, exact or.inr hfi },
-    { rw not_and_distrib,
-      have : (λx, r • (f x)) = r • f, { funext, simp only [pi.smul_apply] },
-      rw [this, integrable.smul_iff r0], exact or.inr hfi } },
-  { repeat { rw dif_neg },
-    { rw smul_zero },
-    { rw not_and_distrib, exact or.inl hfm },
-    { rw not_and_distrib, rw [measurable_smul_iff r0], exact or.inl hfm, apply_instance } },
+  by_cases hf : measurable f ∧ integrable f,
+  { rw [integral_eq f hf.1 hf.2, integral_eq (r • f), l1.of_fun_smul, l1.integral_smul] },
+  { by_cases hr : r = 0,
+    { simp only [hr, measure_theory.integral_zero, zero_smul] },
+    have hf' : ¬(measurable (r • f) ∧ integrable (r • f)),
+    { rwa [← measurable_smul_iff hr f, ← integrable_smul_iff hr f] at hf },
+    rw [integral_undef hf, integral_undef hf', smul_zero] }
 end
 
 lemma integral_congr_ae (hfm : measurable f) (hgm : measurable g) (h : ∀ₘ a, f a = g a) :
    integral f = integral g :=
 begin
   by_cases hfi : integrable f,
   { have hgi : integrable g := integrable_of_ae_eq hfi h,
-    simp only [integral],
-    repeat { rw dif_pos },
-    rotate, { exact ⟨hgm, hgi⟩ }, { exact ⟨hfm, hfi⟩ },
-    rw ← l1.of_fun_eq_of_fun f g hfm hfi hgm hgi at h,
-    rw h },
+    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_iff_of_ae_eq h at hfi, exact hfi },
-    rw [integral_eq_zero_of_non_integrable hfi, integral_eq_zero_of_non_integrable hgi] },
+    rw [integral_non_integrable hfi, integral_non_integrable hgi] },
 end
 
 lemma norm_integral_le_lintegral_norm (f : α → β) :
   ∥integral f∥ ≤ ennreal.to_real (∫⁻ a, ennreal.of_real ∥f a∥) :=
 begin
-  by_cases hfm : measurable f,
-  by_cases hfi : integrable f,
-  { rw [integral, ← l1.norm_of_fun_eq_lintegral_norm f hfm hfi, dif_pos],
-    exact l1.norm_integral_le _, exact ⟨hfm, hfi⟩ },
-  { rw [integral_eq_zero_of_non_integrable hfi, _root_.norm_zero],
-    exact to_real_nonneg },
-  { rw [integral_eq_zero_of_non_measurable hfm, _root_.norm_zero],
+  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, _root_.norm_zero],
     exact to_real_nonneg }
 end
 
@@ -1240,7 +1204,7 @@ begin
       assume a h,
       rw max_eq_left h },
     rw [h_min, h_max, zero_to_real, _root_.sub_zero] },
-  { rw integral_eq_zero_of_non_integrable hfi,
+  { rw integral_non_integrable hfi,
     rw [integrable_iff_norm, lt_top_iff_ne_top, ne.def, not_not] at hfi,
     have : (∫⁻ (a : α), ennreal.of_real (f a)) = (∫⁻ a, ennreal.of_real ∥f a∥),
     { apply lintegral_congr_ae,
@@ -1255,7 +1219,7 @@ lemma integral_nonneg_of_nonneg_ae {f : α → ℝ} (hf : ∀ₘ a, 0 ≤ f a) :
 begin
   by_cases hfm : measurable f,
   { rw integral_eq_lintegral_of_nonneg_ae hf hfm, exact to_real_nonneg },
-  { rw integral_eq_zero_of_non_measurable hfm }
+  { rw integral_non_measurable hfm }
 end
 
 lemma integral_nonpos_of_nonpos_ae {f : α → ℝ} (hf : ∀ₘ a, f a ≤ 0) : integral f ≤ 0 :=
@@ -1283,10 +1247,10 @@ have le_ae : ∀ₘ (a : α), 0 ≤ ∥f a∥ := by filter_upwards [] λa, norm_
 classical.by_cases
 ( λh : measurable f,
   calc ∥integral f∥ ≤ ennreal.to_real (∫⁻ a, ennreal.of_real ∥f a∥) : norm_integral_le_lintegral_norm _
-    ... = ∫ a, ∥f a∥ : (integral_eq_lintegral_of_nonneg_ae le_ae $ measurable_norm h).symm )
+    ... = ∫ a, ∥f a∥ : (integral_eq_lintegral_of_nonneg_ae le_ae $ measurable.norm h).symm )
 ( λh : ¬measurable f,
   begin
-    rw [integral_eq_zero_of_non_measurable h, _root_.norm_zero],
+    rw [integral_non_measurable h, _root_.norm_zero],
     exact integral_nonneg_of_nonneg_ae le_ae
   end )
 

src/measure_theory/borel_space.lean

@@ -512,19 +512,17 @@ measurable_of_continuous ennreal.continuous_of_real
 
 end ennreal
 
-namespace measure_theory
-
 open topological_space
 
-lemma measurable_smul' {α : Type*} {β : Type*} {γ : Type*}
+lemma measurable.smul' {α : Type*} {β : Type*} {γ : Type*}
   [semiring α] [topological_space α] [second_countable_topology α]
   [topological_space β] [add_comm_monoid β] [second_countable_topology β]
   [semimodule α β] [topological_semimodule α β] [measurable_space γ]
   {f : γ → α} {g : γ → β} (hf : measurable f) (hg : measurable g) :
   measurable (λ c, f c • g c) :=
 measurable_of_continuous2 (continuous_fst.smul continuous_snd) hf hg
 
-lemma measurable_smul {α : Type*} {β : Type*} {γ : Type*}
+lemma measurable.smul {α : Type*} {β : Type*} {γ : Type*}
   [semiring α] [topological_space α]
   [topological_space β] [add_comm_monoid β]
   [semimodule α β] [topological_semimodule α β] [measurable_space γ]
@@ -541,66 +539,64 @@ begin
   assume h,
   have eq : (λ (x : γ), c⁻¹ • (λ (x : γ), c • f x) x) = f,
   { funext, rw [smul_smul, inv_mul_cancel hc, one_smul] },
-  have := measurable_smul c⁻¹ h,
+  have := h.smul c⁻¹,
   rwa eq at this
 end
-$ measurable_smul c
+$ measurable.smul c
 
-lemma measurable_dist' {α : Type*} [metric_space α] [second_countable_topology α] :
+lemma measurable_dist {α : Type*} [metric_space α] [second_countable_topology α] :
   measurable (λp:α×α, dist p.1 p.2) :=
 begin
   rw [borel_prod],
   apply measurable_of_continuous,
   exact continuous_dist continuous_fst continuous_snd
 end
 
-lemma measurable_dist {α : Type*} [metric_space α] [second_countable_topology α]
+lemma measurable.dist {α : Type*} [metric_space α] [second_countable_topology α]
   [measurable_space β] {f g : β → α} (hf : measurable f) (hg : measurable g) :
 	measurable (λ b, dist (f b) (g b)) :=
-measurable.comp measurable_dist' (measurable.prod_mk hf hg)
+measurable_dist.comp (measurable.prod_mk hf hg)
 
-lemma measurable_nndist' {α : Type*} [metric_space α] [second_countable_topology α] :
+lemma measurable_nndist {α : Type*} [metric_space α] [second_countable_topology α] :
   measurable (λp:α×α, nndist p.1 p.2) :=
 begin
   rw [borel_prod],
   apply measurable_of_continuous,
   exact continuous_nndist continuous_fst continuous_snd
 end
 
-lemma measurable_nndist {α : Type*} [metric_space α] [second_countable_topology α]
+lemma measurable.nndist {α : Type*} [metric_space α] [second_countable_topology α]
   [measurable_space β] {f g : β → α} (hf : measurable f) (hg : measurable g) :
 	measurable (λ b, nndist (f b) (g b)) :=
-measurable.comp measurable_nndist' (measurable.prod_mk hf hg)
+measurable_nndist.comp (measurable.prod_mk hf hg)
 
-lemma measurable_edist' {α : Type*} [emetric_space α] [second_countable_topology α] :
+lemma measurable_edist {α : Type*} [emetric_space α] [second_countable_topology α] :
   measurable (λp:α×α, edist p.1 p.2) :=
 begin
   rw [borel_prod],
   apply measurable_of_continuous,
   exact continuous_edist continuous_fst continuous_snd
 end
 
-lemma measurable_edist {α : Type*} [emetric_space α] [second_countable_topology α]
+lemma measurable.edist {α : Type*} [emetric_space α] [second_countable_topology α]
   [measurable_space β] {f g : β → α} (hf : measurable f) (hg : measurable g) :
 	measurable (λ b, edist (f b) (g b)) :=
-measurable.comp measurable_edist' (measurable.prod_mk hf hg)
+measurable_edist.comp (measurable.prod_mk hf hg)
 
-lemma measurable_norm' {α : Type*} [normed_group α] : measurable (norm : α → ℝ) :=
+lemma measurable_norm {α : Type*} [normed_group α] : measurable (norm : α → ℝ) :=
 measurable_of_continuous continuous_norm
 
-lemma measurable_norm {α : Type*} [normed_group α] [measurable_space β]
+lemma measurable.norm {α : Type*} [normed_group α] [measurable_space β]
   {f : β → α} (hf : measurable f) : measurable (λa, norm (f a)) :=
-measurable.comp measurable_norm' hf
+measurable_norm.comp hf
 
-lemma measurable_nnnorm' {α : Type*} [normed_group α] : measurable (nnnorm : α → nnreal) :=
+lemma measurable_nnnorm {α : Type*} [normed_group α] : measurable (nnnorm : α → nnreal) :=
 measurable_of_continuous continuous_nnnorm
 
-lemma measurable_nnnorm {α : Type*} [normed_group α] [measurable_space β]
+lemma measurable.nnnorm {α : Type*} [normed_group α] [measurable_space β]
   {f : β → α} (hf : measurable f) : measurable (λa, nnnorm (f a)) :=
-measurable.comp measurable_nnnorm' hf
+measurable_nnnorm.comp hf
 
-lemma measurable_coe_nnnorm {α : Type*} [normed_group α] [measurable_space β]
+lemma measurable.coe_nnnorm {α : Type*} [normed_group α] [measurable_space β]
   {f : β → α} (hf : measurable f) : measurable (λa, (nnnorm (f a) : ennreal)) :=
-measurable.comp ennreal.measurable_coe $ measurable_nnnorm hf
-
-end measure_theory
+ennreal.measurable_coe.comp $ hf.nnnorm