chore(src/analysis/special_functions/trigonometric/basic) : prove continuity of sin/cos/sinh/cosh without derivatives (#9502)

In a future PR, I want to split all files in the special_functions folder to avoid importing calculus when not needed (the goal is to avoid importing it in the definition of lp_space in measure_theory). This PR changes the proofs of continuity of trigonometric functions.

Author: RemyDegenne

src/analysis/special_functions/trigonometric/basic.lean

@@ -74,9 +74,8 @@ differentiable_sin x
 @[simp] lemma deriv_sin : deriv sin = cos :=
 funext $ λ x, (has_deriv_at_sin x).deriv
 
-@[continuity]
-lemma continuous_sin : continuous sin :=
-differentiable_sin.continuous
+@[continuity] lemma continuous_sin : continuous sin :=
+by { change continuous (λ z, ((exp (-z * I) - exp (z * I)) * I) / 2), continuity, }
 
 lemma continuous_on_sin {s : set ℂ} : continuous_on sin s := continuous_sin.continuous_on
 
@@ -111,9 +110,8 @@ lemma deriv_cos {x : ℂ} : deriv cos x = -sin x :=
 @[simp] lemma deriv_cos' : deriv cos = (λ x, -sin x) :=
 funext $ λ x, deriv_cos
 
-@[continuity]
-lemma continuous_cos : continuous cos :=
-differentiable_cos.continuous
+@[continuity] lemma continuous_cos : continuous cos :=
+by { change continuous (λ z, (exp (z * I) + exp (-z * I)) / 2), continuity, }
 
 lemma continuous_on_cos {s : set ℂ} : continuous_on cos s := continuous_cos.continuous_on
 
@@ -143,9 +141,8 @@ differentiable_sinh x
 @[simp] lemma deriv_sinh : deriv sinh = cosh :=
 funext $ λ x, (has_deriv_at_sinh x).deriv
 
-@[continuity]
-lemma continuous_sinh : continuous sinh :=
-differentiable_sinh.continuous
+@[continuity] lemma continuous_sinh : continuous sinh :=
+by { change continuous (λ z, (exp z - exp (-z)) / 2), continuity, }
 
 /-- The complex hyperbolic cosine function is everywhere strictly differentiable, with the
 derivative `sinh x`. -/
@@ -173,9 +170,8 @@ differentiable_cosh x
 @[simp] lemma deriv_cosh : deriv cosh = sinh :=
 funext $ λ x, (has_deriv_at_cosh x).deriv
 
-@[continuity]
-lemma continuous_cosh : continuous cosh :=
-differentiable_cosh.continuous
+@[continuity] lemma continuous_cosh : continuous cosh :=
+by { change continuous (λ z, (exp z + exp (-z)) / 2), continuity, }
 
 end complex
 
@@ -528,9 +524,8 @@ differentiable_sin x
 @[simp] lemma deriv_sin : deriv sin = cos :=
 funext $ λ x, (has_deriv_at_sin x).deriv
 
-@[continuity]
-lemma continuous_sin : continuous sin :=
-differentiable_sin.continuous
+@[continuity] lemma continuous_sin : continuous sin :=
+complex.continuous_re.comp (complex.continuous_sin.comp complex.continuous_of_real)
 
 lemma continuous_on_sin {s} : continuous_on sin s :=
 continuous_sin.continuous_on
@@ -556,9 +551,8 @@ lemma deriv_cos : deriv cos x = - sin x :=
 @[simp] lemma deriv_cos' : deriv cos = (λ x, - sin x) :=
 funext $ λ _, deriv_cos
 
-@[continuity]
-lemma continuous_cos : continuous cos :=
-differentiable_cos.continuous
+@[continuity] lemma continuous_cos : continuous cos :=
+complex.continuous_re.comp (complex.continuous_cos.comp complex.continuous_of_real)
 
 lemma continuous_on_cos {s} : continuous_on cos s := continuous_cos.continuous_on
 
@@ -580,9 +574,8 @@ differentiable_sinh x
 @[simp] lemma deriv_sinh : deriv sinh = cosh :=
 funext $ λ x, (has_deriv_at_sinh x).deriv
 
-@[continuity]
-lemma continuous_sinh : continuous sinh :=
-differentiable_sinh.continuous
+@[continuity] lemma continuous_sinh : continuous sinh :=
+complex.continuous_re.comp (complex.continuous_sinh.comp complex.continuous_of_real)
 
 lemma has_strict_deriv_at_cosh (x : ℝ) : has_strict_deriv_at cosh (sinh x) x :=
 (complex.has_strict_deriv_at_cosh x).real_of_complex
@@ -602,9 +595,8 @@ differentiable_cosh x
 @[simp] lemma deriv_cosh : deriv cosh = sinh :=
 funext $ λ x, (has_deriv_at_cosh x).deriv
 
-@[continuity]
-lemma continuous_cosh : continuous cosh :=
-differentiable_cosh.continuous
+@[continuity] lemma continuous_cosh : continuous cosh :=
+complex.continuous_re.comp (complex.continuous_cosh.comp complex.continuous_of_real)
 
 /-- `sinh` is strictly monotone. -/
 lemma sinh_strict_mono : strict_mono sinh :=