chore(measure_theory/special_functions): add measurability attributes (…

…#8570)

That attribute makes the `measurability` tactic aware of those lemmas.

src/measure_theory/special_functions.lean

@@ -20,47 +20,48 @@ open_locale nnreal ennreal
 
 namespace real
 
-lemma measurable_exp : measurable exp := continuous_exp.measurable
+@[measurability] lemma measurable_exp : measurable exp := continuous_exp.measurable
 
-lemma measurable_log : measurable log :=
+@[measurability] lemma measurable_log : measurable log :=
 measurable_of_measurable_on_compl_singleton 0 $ continuous.measurable $
   continuous_on_iff_continuous_restrict.1 continuous_on_log
 
-lemma measurable_sin : measurable sin := continuous_sin.measurable
+@[measurability] lemma measurable_sin : measurable sin := continuous_sin.measurable
 
-lemma measurable_cos : measurable cos := continuous_cos.measurable
+@[measurability] lemma measurable_cos : measurable cos := continuous_cos.measurable
 
-lemma measurable_sinh : measurable sinh := continuous_sinh.measurable
+@[measurability] lemma measurable_sinh : measurable sinh := continuous_sinh.measurable
 
-lemma measurable_cosh : measurable cosh := continuous_cosh.measurable
+@[measurability] lemma measurable_cosh : measurable cosh := continuous_cosh.measurable
 
-lemma measurable_arcsin : measurable arcsin := continuous_arcsin.measurable
+@[measurability] lemma measurable_arcsin : measurable arcsin := continuous_arcsin.measurable
 
-lemma measurable_arccos : measurable arccos := continuous_arccos.measurable
+@[measurability] lemma measurable_arccos : measurable arccos := continuous_arccos.measurable
 
-lemma measurable_arctan : measurable arctan := continuous_arctan.measurable
+@[measurability] lemma measurable_arctan : measurable arctan := continuous_arctan.measurable
 
 end real
 
 namespace complex
 
-lemma measurable_re : measurable re := continuous_re.measurable
+@[measurability] lemma measurable_re : measurable re := continuous_re.measurable
 
-lemma measurable_im : measurable im := continuous_im.measurable
+@[measurability] lemma measurable_im : measurable im := continuous_im.measurable
 
-lemma measurable_of_real : measurable (coe : ℝ → ℂ) := continuous_of_real.measurable
+@[measurability] lemma measurable_of_real : measurable (coe : ℝ → ℂ) :=
+continuous_of_real.measurable
 
-lemma measurable_exp : measurable exp := continuous_exp.measurable
+@[measurability] lemma measurable_exp : measurable exp := continuous_exp.measurable
 
-lemma measurable_sin : measurable sin := continuous_sin.measurable
+@[measurability] lemma measurable_sin : measurable sin := continuous_sin.measurable
 
-lemma measurable_cos : measurable cos := continuous_cos.measurable
+@[measurability] lemma measurable_cos : measurable cos := continuous_cos.measurable
 
-lemma measurable_sinh : measurable sinh := continuous_sinh.measurable
+@[measurability] lemma measurable_sinh : measurable sinh := continuous_sinh.measurable
 
-lemma measurable_cosh : measurable cosh := continuous_cosh.measurable
+@[measurability] lemma measurable_cosh : measurable cosh := continuous_cosh.measurable
 
-lemma measurable_arg : measurable arg :=
+@[measurability] lemma measurable_arg : measurable arg :=
 have A : measurable (λ x : ℂ, real.arcsin (x.im / x.abs)),
   from real.measurable_arcsin.comp (measurable_im.div measurable_norm),
 have B : measurable (λ x : ℂ, real.arcsin ((-x).im / x.abs)),
@@ -69,7 +70,7 @@ measurable.ite (is_closed_le continuous_const continuous_re).measurable_set A $
   measurable.ite (is_closed_le continuous_const continuous_im).measurable_set
     (B.add_const _) (B.sub_const _)
 
-lemma measurable_log : measurable log :=
+@[measurability] lemma measurable_log : measurable log :=
 (measurable_of_real.comp $ real.measurable_log.comp measurable_norm).add $
   (measurable_of_real.comp measurable_arg).mul_const I
 
@@ -79,28 +80,28 @@ section real_composition
 open real
 variables {α : Type*} [measurable_space α] {f : α → ℝ} (hf : measurable f)
 
-lemma measurable.exp : measurable (λ x, real.exp (f x)) :=
+@[measurability] lemma measurable.exp : measurable (λ x, real.exp (f x)) :=
 real.measurable_exp.comp hf
 
-lemma measurable.log : measurable (λ x, log (f x)) :=
+@[measurability] lemma measurable.log : measurable (λ x, log (f x)) :=
 measurable_log.comp hf
 
-lemma measurable.cos : measurable (λ x, real.cos (f x)) :=
+@[measurability] lemma measurable.cos : measurable (λ x, real.cos (f x)) :=
 real.measurable_cos.comp hf
 
-lemma measurable.sin : measurable (λ x, real.sin (f x)) :=
+@[measurability] lemma measurable.sin : measurable (λ x, real.sin (f x)) :=
 real.measurable_sin.comp hf
 
-lemma measurable.cosh : measurable (λ x, real.cosh (f x)) :=
+@[measurability] lemma measurable.cosh : measurable (λ x, real.cosh (f x)) :=
 real.measurable_cosh.comp hf
 
-lemma measurable.sinh : measurable (λ x, real.sinh (f x)) :=
+@[measurability] lemma measurable.sinh : measurable (λ x, real.sinh (f x)) :=
 real.measurable_sinh.comp hf
 
-lemma measurable.arctan : measurable (λ x, arctan (f x)) :=
+@[measurability] lemma measurable.arctan : measurable (λ x, arctan (f x)) :=
 measurable_arctan.comp hf
 
-lemma measurable.sqrt : measurable (λ x, sqrt (f x)) :=
+@[measurability] lemma measurable.sqrt : measurable (λ x, sqrt (f x)) :=
 continuous_sqrt.measurable.comp hf
 
 end real_composition
@@ -109,25 +110,25 @@ section complex_composition
 open complex
 variables {α : Type*} [measurable_space α] {f : α → ℂ} (hf : measurable f)
 
-lemma measurable.cexp : measurable (λ x, complex.exp (f x)) :=
+@[measurability] lemma measurable.cexp : measurable (λ x, complex.exp (f x)) :=
 complex.measurable_exp.comp hf
 
-lemma measurable.ccos : measurable (λ x, complex.cos (f x)) :=
+@[measurability] lemma measurable.ccos : measurable (λ x, complex.cos (f x)) :=
 complex.measurable_cos.comp hf
 
-lemma measurable.csin : measurable (λ x, complex.sin (f x)) :=
+@[measurability] lemma measurable.csin : measurable (λ x, complex.sin (f x)) :=
 complex.measurable_sin.comp hf
 
-lemma measurable.ccosh : measurable (λ x, complex.cosh (f x)) :=
+@[measurability] lemma measurable.ccosh : measurable (λ x, complex.cosh (f x)) :=
 complex.measurable_cosh.comp hf
 
-lemma measurable.csinh : measurable (λ x, complex.sinh (f x)) :=
+@[measurability] lemma measurable.csinh : measurable (λ x, complex.sinh (f x)) :=
 complex.measurable_sinh.comp hf
 
-lemma measurable.carg : measurable (λ x, arg (f x)) :=
+@[measurability] lemma measurable.carg : measurable (λ x, arg (f x)) :=
 measurable_arg.comp hf
 
-lemma measurable.clog : measurable (λ x, log (f x)) :=
+@[measurability] lemma measurable.clog : measurable (λ x, log (f x)) :=
 measurable_log.comp hf
 
 end complex_composition
@@ -165,12 +166,14 @@ section
 variables {α : Type*} {𝕜 : Type*} {E : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E]
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 
+@[measurability]
 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
 
+@[measurability]
 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 μ) :