chore(measure_theory/*): use _measure instead of _meas (#3892)

Author: urkud

src/measure_theory/bochner_integration.lean

@@ -347,15 +347,15 @@ begin
     end
 end
 
-lemma integral_add_meas {ν} (f : α →ₛ E) (hf : integrable f (μ + ν)) :
+lemma integral_add_measure {ν} (f : α →ₛ E) (hf : integrable f (μ + ν)) :
   f.integral (μ + ν) = f.integral μ + f.integral ν :=
 begin
   simp only [integral_eq_sum_filter, ← sum_add_distrib, ← add_smul, measure.add_apply],
   refine sum_congr rfl (λ x hx, _),
   rw [to_real_add];
     refine ne_of_lt ((integrable_iff_fin_meas_supp.1 _).meas_preimage_singleton_ne_zero
       (mem_filter.1 hx).2),
-  exacts [hf.left_of_add_meas, hf.right_of_add_meas]
+  exacts [hf.left_of_add_measure, hf.right_of_add_measure]
 end
 
 variables [second_countable_topology E] [measurable_space E] [borel_space E]
@@ -1262,13 +1262,13 @@ calc ∥∫ x, f x ∂μ∥ ≤ ∫ x, C ∂μ : norm_integral_le_of_norm_le mea
 
 variable {ν : measure α}
 
-lemma integral_add_meas {f : α → E} (hfm : measurable f) (hμ : integrable f μ) (hν : integrable f ν) :
+lemma integral_add_measure {f : α → E} (hfm : measurable f) (hμ : integrable f μ) (hν : integrable f ν) :
   ∫ x, f x ∂(μ + ν) = ∫ x, f x ∂μ + ∫ x, f x ∂ν :=
 begin
-  have hfi := hμ.add_meas hν,
+  have hfi := hμ.add_measure hν,
   rcases simple_func_sequence_tendsto' hfm hfi with ⟨F, hFi, hFt⟩,
-  have hFiμ : ∀ i, integrable (F i) μ := λ i, (hFi i).left_of_add_meas,
-  have hFiν : ∀ i, integrable (F i) ν := λ i, (hFi i).right_of_add_meas,
+  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)
@@ -1284,19 +1284,20 @@ begin
     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μν,
-  simpa only [← simple_func.integral_eq_integral, *, simple_func.integral_add_meas] using hμ.add hν
+  simpa only [← simple_func.integral_eq_integral, *, simple_func.integral_add_measure]
+    using hμ.add hν
 end
 
-@[simp] lemma integral_zero_meas (f : α → E) : ∫ x, f x ∂0 = 0 :=
+@[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
 
-lemma integral_map_meas {β} [measurable_space β] {φ : α → β} (hφ : measurable φ)
+lemma integral_map_measure {β} [measurable_space β] {φ : α → β} (hφ : measurable φ)
   {f : β → E} (hfm : measurable f) :
   ∫ 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],
-    rwa [← integrable_map_meas hφ hfm] },
+    rwa [← integrable_map_measure hφ hfm] },
   rcases simple_func_sequence_tendsto' hfm 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 φ μ)) :=
@@ -1305,7 +1306,7 @@ begin
   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_meas, hφ, hfm, (F _).measurable] at 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, _),

src/measure_theory/integration.lean

@@ -977,11 +977,11 @@ calc (∫⁻ a, f a + g a ∂μ) =
 
 lemma lintegral_zero : (∫⁻ a:α, 0 ∂μ) = 0 := by simp
 
-lemma lintegral_smul_meas (c : ennreal) (f : α → ennreal) :
+lemma lintegral_smul_measure (c : ennreal) (f : α → ennreal) :
   ∫⁻ a, f a ∂ (c • μ) = c * ∫⁻ a, f a ∂μ :=
 by simp only [lintegral, supr_subtype', simple_func.lintegral_smul, ennreal.mul_supr, smul_eq_mul]
 
-lemma lintegral_sum_meas {ι} (f : α → ennreal) (μ : ι → measure α) :
+lemma lintegral_sum_measure {ι} (f : α → ennreal) (μ : ι → measure α) :
   ∫⁻ a, f a ∂(measure.sum μ) = ∑' i, ∫⁻ a, f a ∂(μ i) :=
 begin
   simp only [lintegral, supr_subtype', simple_func.lintegral_sum, ennreal.tsum_eq_supr_sum],
@@ -996,11 +996,11 @@ begin
       (finset.sum_le_sum $ λ j hj, simple_func.lintegral_mono le_sup_right (le_refl _))⟩
 end
 
-lemma lintegral_add_meas (f : α → ennreal) (μ ν : measure α) :
+lemma lintegral_add_measure (f : α → ennreal) (μ ν : measure α) :
   ∫⁻ a, f a ∂ (μ + ν) = ∫⁻ a, f a ∂μ + ∫⁻ a, f a ∂ν :=
-by simpa [tsum_fintype] using lintegral_sum_meas f (λ b, cond b μ ν)
+by simpa [tsum_fintype] using lintegral_sum_measure f (λ b, cond b μ ν)
 
-@[simp] lemma lintegral_zero_meas (f : α → ennreal) : ∫⁻ a, f a ∂0 = 0 :=
+@[simp] lemma lintegral_zero_measure (f : α → ennreal) : ∫⁻ a, f a ∂0 = 0 :=
 bot_unique $ by simp [lintegral]
 
 lemma lintegral_finset_sum (s : finset β) {f : β → α → ennreal} (hf : ∀b, measurable (f b)) :
@@ -1352,12 +1352,12 @@ open measure
 lemma lintegral_Union [encodable β] {s : β → set α} (hm : ∀ i, is_measurable (s i))
   (hd : pairwise (disjoint on s)) (f : α → ennreal) :
   ∫⁻ a in ⋃ i, s i, f a ∂μ = ∑' i, ∫⁻ a in s i, f a ∂μ :=
-by simp only [measure.restrict_Union hd hm, lintegral_sum_meas]
+by simp only [measure.restrict_Union hd hm, lintegral_sum_measure]
 
 lemma lintegral_Union_le [encodable β] (s : β → set α) (f : α → ennreal) :
   ∫⁻ a in ⋃ i, s i, f a ∂μ ≤ ∑' i, ∫⁻ a in s i, f a ∂μ :=
 begin
-  rw [← lintegral_sum_meas],
+  rw [← lintegral_sum_measure],
   exact lintegral_mono' restrict_Union_le (le_refl _)
 end
 

src/measure_theory/l1_space.lean

@@ -127,40 +127,40 @@ lemma integrable_of_bounded [finite_measure μ] {f : α → β} {C : ℝ} (hC :
   integrable f μ :=
 (integrable_const C).mono' hC
 
-lemma integrable.mono_meas {f : α → β} (h : integrable f ν) (hμ : μ ≤ ν) :
+lemma integrable.mono_measure {f : α → β} (h : integrable f ν) (hμ : μ ≤ ν) :
   integrable f μ :=
 lt_of_le_of_lt (lintegral_mono' hμ (le_refl _)) h
 
-lemma integrable.add_meas {f : α → β} (hμ : integrable f μ) (hν : integrable f ν) :
+lemma integrable.add_measure {f : α → β} (hμ : integrable f μ) (hν : integrable f ν) :
   integrable f (μ + ν) :=
 begin
-  simp only [integrable, lintegral_add_meas] at *,
+  simp only [integrable, lintegral_add_measure] at *,
   exact add_lt_top.2 ⟨hμ, hν⟩
 end
 
-lemma integrable.left_of_add_meas {f : α → β} (h : integrable f (μ + ν)) :
+lemma integrable.left_of_add_measure {f : α → β} (h : integrable f (μ + ν)) :
   integrable f μ :=
-h.mono_meas $ measure.le_add_right $ le_refl _
+h.mono_measure $ measure.le_add_right $ le_refl _
 
-lemma integrable.right_of_add_meas {f : α → β} (h : integrable f (μ + ν)) :
+lemma integrable.right_of_add_measure {f : α → β} (h : integrable f (μ + ν)) :
   integrable f ν :=
-h.mono_meas $ measure.le_add_left $ le_refl _
+h.mono_measure $ measure.le_add_left $ le_refl _
 
-@[simp] lemma integrable_add_meas {f : α → β} :
+@[simp] lemma integrable_add_measure {f : α → β} :
   integrable f (μ + ν) ↔ integrable f μ ∧ integrable f ν :=
-⟨λ h, ⟨h.left_of_add_meas, h.right_of_add_meas⟩, λ h, h.1.add_meas h.2⟩
+⟨λ h, ⟨h.left_of_add_measure, h.right_of_add_measure⟩, λ h, h.1.add_measure h.2⟩
 
-lemma integrable.smul_meas {f : α → β} (h : integrable f μ) {c : ennreal} (hc : c < ⊤) :
+lemma integrable.smul_measure {f : α → β} (h : integrable f μ) {c : ennreal} (hc : c < ⊤) :
   integrable f (c • μ) :=
 begin
-  simp only [integrable, lintegral_smul_meas] at *,
+  simp only [integrable, lintegral_smul_measure] at *,
   exact mul_lt_top hc h
 end
 
-@[simp] lemma integrable_zero_meas (f : α → β) : integrable f 0 :=
-by simp only [integrable, lintegral_zero_meas, with_top.zero_lt_top]
+@[simp] lemma integrable_zero_measure (f : α → β) : integrable f 0 :=
+by simp only [integrable, lintegral_zero_measure, with_top.zero_lt_top]
 
-lemma integrable_map_meas {δ} [measurable_space δ] [measurable_space β]
+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) μ :=

src/measure_theory/set_integral.lean

@@ -113,22 +113,22 @@ integrable_const_iff.trans $ by rw [measure.restrict_apply_univ]
 
 lemma integrable_on.mono (h : integrable_on f t ν) (hs : s ⊆ t) (hμ : μ ≤ ν) :
   integrable_on f s μ :=
-h.mono_meas $ measure.restrict_mono hs hμ
+h.mono_measure $ measure.restrict_mono hs hμ
 
 lemma integrable_on.mono_set (h : integrable_on f t μ) (hst : s ⊆ t) :
   integrable_on f s μ :=
 h.mono hst (le_refl _)
 
-lemma integrable_on.mono_meas (h : integrable_on f s ν) (hμ : μ ≤ ν) :
+lemma integrable_on.mono_measure (h : integrable_on f s ν) (hμ : μ ≤ ν) :
   integrable_on f s μ :=
 h.mono (subset.refl _) hμ
 
 lemma integrable_on.mono_set_ae (h : integrable_on f t μ) (hst : s ≤ᵐ[μ] t) :
   integrable_on f s μ :=
-h.integrable.mono_meas $ restrict_mono_ae hst
+h.integrable.mono_measure $ restrict_mono_ae hst
 
 lemma integrable.integrable_on (h : integrable f μ) : integrable_on f s μ :=
-h.mono_meas $ measure.restrict_le_self
+h.mono_measure $ measure.restrict_le_self
 
 lemma integrable.integrable_on' (h : integrable f (μ.restrict s)) : integrable_on f s μ :=
 h
@@ -141,7 +141,7 @@ h.mono_set $ subset_union_right _ _
 
 lemma integrable_on.union (hs : integrable_on f s μ) (ht : integrable_on f t μ) :
   integrable_on f (s ∪ t) μ :=
-(hs.add_meas ht).mono_meas $ measure.restrict_union_le _ _
+(hs.add_measure ht).mono_measure $ measure.restrict_union_le _ _
 
 @[simp] lemma integrable_on_union :
   integrable_on f (s ∪ t) μ ↔ integrable_on f s μ ∧ integrable_on f t μ :=
@@ -160,15 +160,15 @@ end
   integrable_on f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, integrable_on f (t i) μ :=
 integrable_on_finite_union s.finite_to_set
 
-lemma integrable_on.add_meas (hμ : integrable_on f s μ) (hν : integrable_on f s ν) :
+lemma integrable_on.add_measure (hμ : integrable_on f s μ) (hν : integrable_on f s ν) :
   integrable_on f s (μ + ν) :=
-by { delta integrable_on, rw measure.restrict_add, exact hμ.integrable.add_meas hν }
+by { delta integrable_on, rw measure.restrict_add, exact hμ.integrable.add_measure hν }
 
-@[simp] lemma integrable_on_add_meas :
+@[simp] lemma integrable_on_add_measure :
   integrable_on f s (μ + ν) ↔ integrable_on f s μ ∧ integrable_on f s ν :=
-⟨λ h, ⟨h.mono_meas (measure.le_add_right (le_refl _)),
-  h.mono_meas (measure.le_add_left (le_refl _))⟩,
-  λ h, h.1.add_meas h.2⟩
+⟨λ h, ⟨h.mono_measure (measure.le_add_right (le_refl _)),
+  h.mono_measure (measure.le_add_left (le_refl _))⟩,
+  λ h, h.1.add_measure h.2⟩
 
 lemma integrable_indicator_iff (hs : is_measurable s) :
   integrable (indicator s f) μ ↔ integrable_on f s μ :=
@@ -213,7 +213,7 @@ begin
   refine ⟨_, λ h, h.filter_mono inf_le_left⟩,
   rintros ⟨s, ⟨t, ht, u, hu, hs⟩, hf⟩,
   refine ⟨t, ht, _⟩,
-  refine hf.integrable.mono_meas (λ v hv, _),
+  refine hf.integrable.mono_measure (λ v hv, _),
   simp only [measure.restrict_apply hv],
   refine measure_mono_ae (mem_sets_of_superset hu $ λ x hx, _),
   exact λ ⟨hv, ht⟩, ⟨hv, hs ⟨ht, hx⟩⟩
@@ -263,9 +263,9 @@ variables [measurable_space E] [borel_space E] [complete_space E] [second_counta
 lemma integral_union (hst : disjoint s t) (hs : is_measurable s) (ht : is_measurable t)
   (hfm : measurable f) (hfs : integrable_on f s μ) (hft : integrable_on f t μ) :
   ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ + ∫ x in t, f x ∂μ :=
-by simp only [integrable_on, measure.restrict_union hst hs ht, integral_add_meas hfm hfs hft]
+by simp only [integrable_on, measure.restrict_union hst hs ht, integral_add_measure hfm hfs hft]
 
-lemma integral_empty : ∫ x in ∅, f x ∂μ = 0 := by rw [measure.restrict_empty, integral_zero_meas]
+lemma integral_empty : ∫ x in ∅, f x ∂μ = 0 := by rw [measure.restrict_empty, integral_zero_measure]
 
 lemma integral_univ : ∫ x in univ, f x ∂μ = ∫ x, f x ∂μ := by rw [measure.restrict_univ]