chore(analysis/special_functions): move measurability statements to measure_theory folder (#8006)

Make sure that measure theory is not imported in basic files defining trigonometric functions and real powers. The measurability of these functions is postponed to a new file `measure_theory.special_functions`.

Author: sgouezel

src/analysis/normed_space/inner_product.lean

@@ -8,6 +8,7 @@ import linear_algebra.bilinear_form
 import linear_algebra.sesquilinear_form
 import data.complex.is_R_or_C
 import analysis.special_functions.sqrt
+import analysis.complex.basic
 
 /-!
 # Inner Product Space
@@ -1668,7 +1669,7 @@ end deriv
 section continuous
 
 /-!
-### Continuity and measurability of the inner product
+### Continuity of the inner product
 
 Since the inner product is `ℝ`-smooth, it is continuous. We do not need a `[normed_space ℝ E]`
 structure to *state* this fact and its corollaries, so we introduce them in the proof instead.
@@ -1688,25 +1689,6 @@ lemma filter.tendsto.inner {f g : α → E} {l : filter α} {x y : E} (hf : tend
   tendsto (λ t, ⟪f t, g t⟫) l (𝓝 ⟪x, y⟫) :=
 (continuous_inner.tendsto _).comp (hf.prod_mk_nhds hg)
 
-lemma measurable.inner [measurable_space α] [measurable_space E] [opens_measurable_space E]
-  [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜]
-  {f g : α → E} (hf : measurable f) (hg : measurable g) :
-  measurable (λ t, ⟪f t, g t⟫) :=
-continuous.measurable2 continuous_inner hf hg
-
-lemma ae_measurable.inner [measurable_space α] [measurable_space E] [opens_measurable_space E]
-  [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜]
-  {μ : measure_theory.measure α} {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
-  ae_measurable (λ x, ⟪f x, g x⟫) μ :=
-begin
-  refine ⟨λ x, ⟪hf.mk f x, hg.mk g x⟫, hf.measurable_mk.inner hg.measurable_mk, _⟩,
-  refine hf.ae_eq_mk.mp (hg.ae_eq_mk.mono (λ x hxg hxf, _)),
-  dsimp only,
-  congr,
-  { exact hxf, },
-  { exact hxg, },
-end
-
 variables [topological_space α] {f g : α → E} {x : α} {s : set α}
 
 include 𝕜

src/analysis/special_functions/exp_log.lean

@@ -5,7 +5,6 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne
 -/
 import data.complex.exponential
 import analysis.calculus.inverse
-import measure_theory.borel_space
 import analysis.complex.real_deriv
 
 /-!
@@ -35,12 +34,6 @@ open_locale classical topological_space
 
 namespace complex
 
-lemma measurable_re : measurable re := continuous_re.measurable
-
-lemma measurable_im : measurable im := continuous_im.measurable
-
-lemma measurable_of_real : measurable (coe : ℝ → ℂ) := continuous_of_real.measurable
-
 /-- The complex exponential is everywhere differentiable, with the derivative `exp x`. -/
 lemma has_deriv_at_exp (x : ℂ) : has_deriv_at exp (exp x) x :=
 begin
@@ -92,8 +85,6 @@ times_cont_diff_exp.times_cont_diff_at.has_strict_deriv_at' (has_deriv_at_exp x)
 lemma is_open_map_exp : is_open_map exp :=
 open_map_of_strict_deriv has_strict_deriv_at_exp exp_ne_zero
 
-lemma measurable_exp : measurable exp := continuous_exp.measurable
-
 end complex
 
 section
@@ -127,10 +118,6 @@ section
 variables {E : Type*} [normed_group E] [normed_space ℂ E] {f : E → ℂ} {f' : E →L[ℂ] ℂ}
   {x : E} {s : set E}
 
-lemma measurable.cexp {α : Type*} [measurable_space α] {f : α → ℂ} (hf : measurable f) :
-  measurable (λ x, complex.exp (f x)) :=
-complex.measurable_exp.comp hf
-
 lemma has_strict_fderiv_at.cexp (hf : has_strict_fderiv_at f f' x) :
   has_strict_fderiv_at (λ x, complex.exp (f x)) (complex.exp (f x) • f') x :=
 (complex.has_strict_deriv_at_exp (f x)).comp_has_strict_fderiv_at x hf
@@ -209,8 +196,6 @@ differentiable_exp.continuous
 lemma continuous_on_exp {s : set ℝ} : continuous_on exp s :=
 continuous_exp.continuous_on
 
-lemma measurable_exp : measurable exp := continuous_exp.measurable
-
 end real
 
 
@@ -250,10 +235,6 @@ function, for standalone use and use with `simp`. -/
 variables {E : Type*} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ}
   {x : E} {s : set E}
 
-lemma measurable.exp {α : Type*} [measurable_space α] {f : α → ℝ} (hf : measurable f) :
-  measurable (λ x, real.exp (f x)) :=
-real.measurable_exp.comp hf
-
 lemma times_cont_diff.exp {n} (hf : times_cont_diff ℝ n f) :
   times_cont_diff ℝ n (λ x, real.exp (f x)) :=
 real.times_cont_diff_exp.comp hf
@@ -571,10 +552,6 @@ else (has_deriv_at_log hx).deriv
 
 @[simp] lemma deriv_log' : deriv log = has_inv.inv := funext deriv_log
 
-lemma measurable_log : measurable log :=
-measurable_of_measurable_on_compl_singleton 0 $ continuous.measurable $
-  continuous_on_iff_continuous_restrict.1 continuous_on_log
-
 lemma times_cont_diff_on_log {n : with_top ℕ} : times_cont_diff_on ℝ n log {0}ᶜ :=
 begin
   suffices : times_cont_diff_on ℝ ⊤ log {0}ᶜ, from this.of_le le_top,
@@ -623,10 +600,6 @@ section deriv
 
 variables {f : ℝ → ℝ} {x f' : ℝ} {s : set ℝ}
 
-lemma measurable.log {α : Type*} [measurable_space α] {f : α → ℝ} (hf : measurable f) :
-  measurable (λ x, log (f x)) :=
-measurable_log.comp hf
-
 lemma has_deriv_within_at.log (hf : has_deriv_within_at f f' s x) (hx : f x ≠ 0) :
   has_deriv_within_at (λ y, log (f y)) (f' / (f x)) s x :=
 begin

src/analysis/special_functions/pow.lean

@@ -148,11 +148,6 @@ lemma has_fderiv_at_cpow {p : ℂ × ℂ} (hp : 0 < p.1.re ∨ p.1.im ≠ 0) :
       (p.1 ^ p.2 * log p.1) • continuous_linear_map.snd ℂ ℂ ℂ) p :=
 (has_strict_fderiv_at_cpow hp).has_fderiv_at
 
-instance : has_measurable_pow ℂ ℂ :=
-⟨measurable.ite (measurable_fst (measurable_set_singleton 0))
-  (measurable.ite (measurable_snd (measurable_set_singleton 0)) measurable_one measurable_zero)
-  (measurable_fst.clog.mul measurable_snd).cexp⟩
-
 end complex
 
 section lim
@@ -858,10 +853,6 @@ end
 
 end sqrt
 
-instance : has_measurable_pow ℝ ℝ :=
-⟨complex.measurable_re.comp $ ((complex.measurable_of_real.comp measurable_fst).pow
-  (complex.measurable_of_real.comp measurable_snd))⟩
-
 end real
 
 section differentiability
@@ -1151,9 +1142,6 @@ begin
   rw [←nnreal.coe_rpow, real.to_nnreal_coe],
 end
 
-instance : has_measurable_pow ℝ≥0 ℝ :=
-⟨(measurable_fst.coe_nnreal_real.pow measurable_snd).subtype_mk⟩
-
 end nnreal
 
 open filter
@@ -1686,17 +1674,4 @@ lemma rpow_left_monotone_of_nonneg {x : ℝ} (hx : 0 ≤ x) : monotone (λ y : 
 lemma rpow_left_strict_mono_of_pos {x : ℝ} (hx : 0 < x) : strict_mono (λ y : ℝ≥0∞, y^x) :=
 λ y z hyz, rpow_lt_rpow hyz hx
 
-instance : has_measurable_pow ℝ≥0∞ ℝ :=
-begin
-  refine ⟨ennreal.measurable_of_measurable_nnreal_prod _ _⟩,
-  { simp_rw ennreal.coe_rpow_def,
-    refine measurable.ite _ measurable_const
-      (measurable_fst.pow measurable_snd).coe_nnreal_ennreal,
-    exact measurable_set.inter (measurable_fst (measurable_set_singleton 0))
-      (measurable_snd measurable_set_Iio), },
-  { simp_rw ennreal.top_rpow_def,
-    refine measurable.ite measurable_set_Ioi measurable_const _,
-    exact measurable.ite (measurable_set_singleton 0) measurable_const measurable_const, },
-end
-
 end ennreal

src/analysis/special_functions/sqrt.lean

@@ -5,7 +5,6 @@ Authors: Yury G. Kudryashov
 -/
 import data.real.sqrt
 import analysis.calculus.inverse
-import measure_theory.borel_space
 
 /-!
 # Smoothness of `real.sqrt`
@@ -70,10 +69,6 @@ end real
 
 open real
 
-lemma measurable.sqrt {α : Type*} [measurable_space α] {f : α → ℝ} (hf : measurable f) :
-  measurable (λ x, sqrt (f x)) :=
-continuous_sqrt.measurable.comp hf
-
 section deriv
 
 variables {f : ℝ → ℝ} {s : set ℝ} {f' x : ℝ}