refactor(measure_theory/*): rename is_(null_)?measurable to (null_)?measurable_set (#6001)

Search & replace:
* `is_null_measurable` → `null_measurable`;
* `is_measurable` → `measurable_set'`;
* `measurable_set_set` → `measurable_set`;
* `measurable_set_spanning_sets` → `measurable_spanning_sets`;
* `measurable_set_superset` → `measurable_superset`.

Author: urkud

src/analysis/calculus/fderiv_measurable.lean

@@ -13,7 +13,7 @@ import measure_theory.borel_space
 In this file we prove that the derivative of any function with complete codomain is a measurable
 function. Namely, we prove:
 
-* `is_measurable_set_of_differentiable_at`: the set `{x | differentiable_at 𝕜 f x}` is measurable;
+* `measurable_set_of_differentiable_at`: the set `{x | differentiable_at 𝕜 f x}` is measurable;
 * `measurable_fderiv`: the function `fderiv 𝕜 f` is measurable;
 * `measurable_fderiv_apply_const`: for a fixed vector `y`, the function `λ x, fderiv 𝕜 f x y`
   is measurable;
@@ -392,21 +392,21 @@ variables (𝕜 f)
 
 /-- The set of differentiability points of a function, with derivative in a given complete set,
 is Borel-measurable. -/
-theorem is_measurable_set_of_differentiable_at_of_is_complete
+theorem measurable_set_of_differentiable_at_of_is_complete
   {K : set (E →L[𝕜] F)} (hK : is_complete K) :
-  is_measurable {x | differentiable_at 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} :=
-by simp [differentiable_set_eq_D K hK, D, is_open_B.is_measurable, is_measurable.Inter_Prop,
-         is_measurable.Inter, is_measurable.Union]
+  measurable_set {x | differentiable_at 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} :=
+by simp [differentiable_set_eq_D K hK, D, is_open_B.measurable_set, measurable_set.Inter_Prop,
+         measurable_set.Inter, measurable_set.Union]
 
 variable [complete_space F]
 
 /-- The set of differentiability points of a function taking values in a complete space is
 Borel-measurable. -/
-theorem is_measurable_set_of_differentiable_at :
-  is_measurable {x | differentiable_at 𝕜 f x} :=
+theorem measurable_set_of_differentiable_at :
+  measurable_set {x | differentiable_at 𝕜 f x} :=
 begin
   have : is_complete (univ : set (E →L[𝕜] F)) := complete_univ,
-  convert is_measurable_set_of_differentiable_at_of_is_complete 𝕜 f this,
+  convert measurable_set_of_differentiable_at_of_is_complete 𝕜 f this,
   simp
 end
 
@@ -417,8 +417,8 @@ begin
     {x | (0 : E →L[𝕜] F) ∈ s} ∩ {x | ¬differentiable_at 𝕜 f x} :=
     set.ext (λ x, mem_preimage.trans fderiv_mem_iff),
   rw this,
-  exact (is_measurable_set_of_differentiable_at_of_is_complete _ _ hs.is_complete).union
-    ((is_measurable.const _).inter (is_measurable_set_of_differentiable_at _ _).compl)
+  exact (measurable_set_of_differentiable_at_of_is_complete _ _ hs.is_complete).union
+    ((measurable_set.const _).inter (measurable_set_of_differentiable_at _ _).compl)
 end
 
 lemma measurable_fderiv_apply_const [measurable_space F] [borel_space F] (y : E) :

src/analysis/special_functions/pow.lean

@@ -603,8 +603,8 @@ section measurability_real
 
 lemma real.measurable_rpow : measurable (λ p : ℝ × ℝ, p.1 ^ p.2) :=
 begin
-  have h_meas : is_measurable {p : ℝ × ℝ | p.1 = 0} :=
-    (is_closed_singleton.preimage continuous_fst).is_measurable,
+  have h_meas : measurable_set {p : ℝ × ℝ | p.1 = 0} :=
+    (is_closed_singleton.preimage continuous_fst).measurable_set,
   refine measurable_of_measurable_union_cover {p : ℝ × ℝ | p.1 = 0} {p : ℝ × ℝ | p.1 ≠ 0} h_meas
     h_meas.compl _ _ _,
   { intro x, simp [em (x.fst = 0)], },
@@ -621,7 +621,7 @@ begin
     change measurable ((λ x : ℝ, ite (x = 0) (1:ℝ) (0:ℝ))
       ∘ (λ a : {p : ℝ × ℝ | p.fst = 0}, (a:ℝ×ℝ).snd)),
     refine measurable.comp _ (measurable_snd.comp measurable_subtype_coe),
-    exact measurable.ite (is_measurable_singleton 0) measurable_const measurable_const, },
+    exact measurable.ite (measurable_set_singleton 0) measurable_const measurable_const, },
   { refine continuous.measurable _,
     rw continuous_iff_continuous_at,
     intro x,
@@ -1558,11 +1558,11 @@ begin
   refine ennreal.measurable_of_measurable_nnreal_prod _ _,
   { simp_rw ennreal.coe_rpow_def,
     refine measurable.ite _ measurable_const nnreal.measurable_rpow.ennreal_coe,
-    exact is_measurable.inter (measurable_fst (is_measurable_singleton 0))
-      (measurable_snd is_measurable_Iio), },
+    exact measurable_set.inter (measurable_fst (measurable_set_singleton 0))
+      (measurable_snd measurable_set_Iio), },
   { simp_rw ennreal.top_rpow_def,
-    refine measurable.ite is_measurable_Ioi measurable_const _,
-    exact measurable.ite (is_measurable_singleton 0) measurable_const measurable_const, },
+    refine measurable.ite measurable_set_Ioi measurable_const _,
+    exact measurable.ite (measurable_set_singleton 0) measurable_const measurable_const, },
 end
 
 lemma measurable.ennreal_rpow {α} [measurable_space α] {f : α → ennreal} (hf : measurable f)

src/measure_theory/ae_measurable_sequence.lean

@@ -89,15 +89,15 @@ end
 
 end mem_ae_seq_set
 
-lemma ae_seq_set_is_measurable {hf : ∀ i, ae_measurable (f i) μ} :
-  is_measurable (ae_seq_set hf p) :=
-(is_measurable_to_measurable _ _).compl
+lemma ae_seq_set_measurable_set {hf : ∀ i, ae_measurable (f i) μ} :
+  measurable_set (ae_seq_set hf p) :=
+(measurable_set_to_measurable _ _).compl
 
 lemma measurable (hf : ∀ i, ae_measurable (f i) μ) (p : α → (ι → β) → Prop)
   (i : ι) :
   measurable (ae_seq hf p i) :=
 begin
-  refine measurable.ite ae_seq_set_is_measurable (hf i).measurable_mk _,
+  refine measurable.ite ae_seq_set_measurable_set (hf i).measurable_mk _,
   by_cases hα : nonempty α,
   { exact @measurable_const _ _ _ _ (⟨f i hα.some⟩ : nonempty β).some },
   { exact measurable_of_not_nonempty hα _ }

src/measure_theory/bochner_integration.lean

@@ -235,7 +235,7 @@ begin
   refine finset.sum_image' _ (assume b hb, _),
   rcases mem_range.1 hb with ⟨a, rfl⟩,
   rw [map_preimage_singleton, ← sum_measure_preimage_singleton _
-    (λ _ _, f.is_measurable_preimage _)],
+    (λ _ _, f.measurable_set_preimage _)],
   -- Now we use `hf : integrable f μ` to show that `ennreal.to_real` is additive.
   by_cases ha : g (f a) = 0,
   { simp only [ha, smul_zero],
@@ -1509,7 +1509,7 @@ begin
     ((integrable_map_measure hfm.ae_measurable hφ).1 hfi),
   ext1 i,
   simp only [simple_func.approx_on_comp, simple_func.integral, measure.map_apply, hφ,
-    simple_func.is_measurable_preimage, ← preimage_comp, simple_func.coe_comp],
+    simple_func.measurable_set_preimage, ← preimage_comp, simple_func.coe_comp],
   refine (finset.sum_subset (simple_func.range_comp_subset_range _ hφ) (λ y _ hy, _)).symm,
   rw [simple_func.mem_range, ← set.preimage_singleton_eq_empty, simple_func.coe_comp] at hy,
   simp [hy]