Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore(src/analysis/special_functions/trigonometric/basic) : prove continuity of sin/cos/sinh/cosh without derivatives #9502

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore(src/analysis/special_functions/trigonometric/basic) : prove continuity of sin/cos/sinh/cosh without derivatives #9502

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
40 changes: 16 additions & 24 deletions src/analysis/special_functions/trigonometric/basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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`. -/
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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

Expand All @@ -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
Expand All @@ -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 :=
Expand Down