Revert "More consistent use of the dot notation"

This reverts commit 854a499.

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 :=
@@ -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 (max u v) :=
+def simple_func : Type* :=
 { f : α →₁ β // ∃ (s : α →ₛ β),  integrable s ∧ ae_eq_fun.mk s s.measurable = f}
 
 variables {α β}
@@ -1033,82 +1033,117 @@ if hf : measurable f ∧ integrable f
 then (l1.of_fun f hf.1 hf.2).integral
 else 0
 
-local notation `∫` binders `, ` r:(scoped f, integral f) := r
+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 : α → β) (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 (f : α → β) : integral f =
+  if hf : measurable f ∧ integrable f then (l1.of_fun f hf.1 hf.2).integral else 0 := rfl
 
-lemma integral_non_integrable (h : ¬ integrable f) : integral f = 0 :=
-integral_undef $ not_and_of_not_right _ 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_measurable (h : ¬ measurable f) : integral f = 0 :=
-integral_undef $ not_and_of_not_left _ 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 }
 
 variables (α β)
 @[simp] lemma integral_zero : integral (0 : α → β) = 0 :=
-by rw [integral_eq, l1.of_fun_zero, l1.integral_zero]
-
+begin
+  simp only [integral], rw dif_pos,
+  { apply l1.integral_zero },
+  { exact ⟨(measurable_const : measurable (λb:α, (0:β))), integrable_zero⟩ }
+end
 variables {α β}
 
-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_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_neg (f : α → β) : integral (-f) = - integral f :=
 begin
-  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] }
+  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 } }
 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_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_smul (r : ℝ) (f : α → β) : integral (r • f) = r • integral f :=
+lemma integral_smul (r : ℝ) (f : α → β) : (∫ x, r • (f x)) = r • integral f :=
 begin
-  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] }
+  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 } },
 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,
-    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]
-},
+    simp only [integral],
+    repeat { rw dif_pos },
+    rotate, { exact ⟨hgm, hgi⟩ }, { exact ⟨hfm, hfi⟩ },
+    rw ← l1.of_fun_eq_of_fun f g hfm hfi hgm hgi at h,
+    rw h },
   { have hgi : ¬ integrable g, { rw integrable_iff_of_ae_eq h at hfi, exact hfi },
-    rw [integral_non_integrable hfi, integral_non_integrable hgi] },
+    rw [integral_eq_zero_of_non_integrable hfi, integral_eq_zero_of_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 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],
+  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],
     exact to_real_nonneg }
 end
 
@@ -1205,7 +1240,7 @@ begin
       assume a h,
       rw max_eq_left h },
     rw [h_min, h_max, zero_to_real, _root_.sub_zero] },
-  { rw integral_non_integrable hfi,
+  { rw integral_eq_zero_of_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,
@@ -1220,7 +1255,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_non_measurable hfm }
+  { rw integral_eq_zero_of_non_measurable hfm }
 end
 
 lemma integral_nonpos_of_nonpos_ae {f : α → ℝ} (hf : ∀ₘ a, f a ≤ 0) : integral f ≤ 0 :=
@@ -1248,10 +1283,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_non_measurable h, _root_.norm_zero],
+    rw [integral_eq_zero_of_non_measurable h, _root_.norm_zero],
     exact integral_nonneg_of_nonneg_ae le_ae
   end )
 

src/measure_theory/borel_space.lean

@@ -512,17 +512,19 @@ 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 γ]
@@ -539,10 +541,10 @@ begin
   assume h,
   have eq : (λ (x : γ), c⁻¹ • (λ (x : γ), c • f x) x) = f,
   { funext, rw [smul_smul, inv_mul_cancel hc, one_smul] },
-  have := h.smul c⁻¹,
+  have := measurable_smul c⁻¹ h,
   rwa eq at this
 end
-$ measurable.smul c
+$ measurable_smul c
 
 lemma measurable_dist' {α : Type*} [metric_space α] [second_countable_topology α] :
   measurable (λp:α×α, dist p.1 p.2) :=
@@ -552,10 +554,10 @@ begin
   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_dist'.comp (measurable.prod_mk hf hg)
+measurable.comp measurable_dist' (measurable.prod_mk hf hg)
 
 lemma measurable_nndist' {α : Type*} [metric_space α] [second_countable_topology α] :
   measurable (λp:α×α, nndist p.1 p.2) :=
@@ -565,10 +567,10 @@ begin
   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_nndist'.comp (measurable.prod_mk hf hg)
+measurable.comp measurable_nndist' (measurable.prod_mk hf hg)
 
 lemma measurable_edist' {α : Type*} [emetric_space α] [second_countable_topology α] :
   measurable (λp:α×α, edist p.1 p.2) :=
@@ -578,25 +580,27 @@ begin
   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_edist'.comp (measurable.prod_mk hf hg)
+measurable.comp measurable_edist' (measurable.prod_mk hf hg)
 
 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_norm'.comp hf
+measurable.comp measurable_norm' hf
 
 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_nnnorm'.comp hf
+measurable.comp measurable_nnnorm' 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)) :=
-ennreal.measurable_coe.comp $ hf.nnnorm
+measurable.comp ennreal.measurable_coe $ measurable_nnnorm hf
+
+end measure_theory

src/measure_theory/l1_space.lean

@@ -125,7 +125,7 @@ lemma lintegral_edist_triangle [second_countable_topology β] {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 (measurable.edist hf hh) (measurable.edist hg hh),
+  rw ← lintegral_add (measurable_edist hf hh) (measurable_edist hg hh),
   apply lintegral_le_lintegral,
   assume a,
   have := edist_triangle (f a) (h a) (g a),
@@ -147,7 +147,7 @@ by { have := coe_lt_top, simpa [integrable] }
 
 lemma lintegral_nnnorm_add {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 (measurable.coe_nnnorm hf) (measurable.coe_nnnorm hg)
+lintegral_add (measurable_coe_nnnorm hf) (measurable_coe_nnnorm hg)
 
 lemma integrable.add {f g : α → β} (hfm : measurable f) (hgm : measurable g) :
   integrable f → integrable g → integrable (f + g) :=
@@ -299,7 +299,7 @@ begin
   -- Using the dominated convergence theorem.
   refine tendsto_lintegral_of_dominated_convergence _ hb _ _,
   -- Show `λa, ∥f a - F n a∥` is measurable for all `n`
-  { exact λn, measurable.comp measurable_of_real (measurable.norm (measurable.sub (F_measurable n)
+  { exact λn, measurable.comp measurable_of_real (measurable_norm (measurable.sub (F_measurable n)
       f_measurable)) },
   -- Show `2 * bound` is integrable
   { rw integrable_iff_of_real at bound_integrable,
@@ -365,7 +365,7 @@ begin
     end
 end
 
-lemma integrable_smul_iff {c : 𝕜} (hc : c ≠ 0) (f : α → β) : integrable (c • f) ↔ integrable f :=
+lemma integrable.smul_iff {c : 𝕜} (hc : c ≠ 0) (f : α → β) : integrable (c • f) ↔ integrable f :=
 begin
   split,
   { assume h,
@@ -429,7 +429,7 @@ 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 : Type (max u v) := subtype (@ae_eq_fun.integrable α _ β _ _)
+def l1 : Type* := subtype (@ae_eq_fun.integrable α _ β _ _)
 
 infixr ` →₁ `:25 := l1
 
@@ -540,7 +540,7 @@ by { rw [norm_of_fun, lintegral_norm_eq_lintegral_edist] }
 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
 
 lemma of_fun_smul (f : α → β) (hfm hfi) (k : 𝕜) :
-  of_fun (k • f) (measurable.smul _ hfm) (integrable.smul _ hfi) = k • of_fun f hfm hfi := rfl
+  of_fun (k • f) (measurable_smul _ hfm) (integrable.smul _ hfi) = k • of_fun f hfm hfi := rfl
 
 end of_fun
 

src/measure_theory/measurable_space.lean

@@ -389,9 +389,6 @@ assume s hs, show is_measurable {b : β | a ∈ s}, from
     (assume h : a ∈ s, by simp [h]; from is_measurable.univ)
     (assume h : a ∉ s, by simp [h]; from is_measurable.empty)
 
-lemma measurable_zero {α β} [measurable_space α] [has_zero α] [measurable_space β] :
-  measurable (λb:β, (0:α)) := measurable_const
-
 end measurable_functions
 
 section constructions