mathlib documentation

analysis.special_functions.trigonometric

Trigonometric functions #

Main definitions #

This file contains the following definitions:

Main statements #

Many basic inequalities on trigonometric functions are established.

The continuity and differentiability of the usual trigonometric functions are proved, and their derivatives are computed.

Tags #

log, sin, cos, tan, arcsin, arccos, arctan, angle, argument

The complex sine function is everywhere strictly differentiable, with the derivative cos x.

The complex sine function is everywhere differentiable, with the derivative cos x.

The complex cosine function is everywhere strictly differentiable, with the derivative -sin x.

The complex cosine function is everywhere differentiable, with the derivative -sin x.

@[simp]

The complex hyperbolic sine function is everywhere strictly differentiable, with the derivative cosh x.

The complex hyperbolic sine function is everywhere differentiable, with the derivative cosh x.

The complex hyperbolic cosine function is everywhere strictly differentiable, with the derivative sinh x.

The complex hyperbolic cosine function is everywhere differentiable, with the derivative sinh x.

Simp lemmas for derivatives of λ x, complex.cos (f x) etc., f : ℂ → ℂ #

complex.cos #

theorem has_strict_deriv_at.ccos {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), complex.cos (f x)) ((-complex.sin (f x)) * f') x
theorem has_deriv_at.ccos {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), complex.cos (f x)) ((-complex.sin (f x)) * f') x
theorem has_deriv_within_at.ccos {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), complex.cos (f x)) ((-complex.sin (f x)) * f') s x
theorem deriv_within_ccos {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.cos (f x)) s x = (-complex.sin (f x)) * deriv_within f s x
@[simp]
theorem deriv_ccos {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.cos (f x)) x = (-complex.sin (f x)) * deriv f x

complex.sin #

theorem has_strict_deriv_at.csin {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), complex.sin (f x)) ((complex.cos (f x)) * f') x
theorem has_deriv_at.csin {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), complex.sin (f x)) ((complex.cos (f x)) * f') x
theorem has_deriv_within_at.csin {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), complex.sin (f x)) ((complex.cos (f x)) * f') s x
theorem deriv_within_csin {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.sin (f x)) s x = (complex.cos (f x)) * deriv_within f s x
@[simp]
theorem deriv_csin {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.sin (f x)) x = (complex.cos (f x)) * deriv f x

complex.cosh #

theorem has_strict_deriv_at.ccosh {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), complex.cosh (f x)) ((complex.sinh (f x)) * f') x
theorem has_deriv_at.ccosh {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), complex.cosh (f x)) ((complex.sinh (f x)) * f') x
theorem has_deriv_within_at.ccosh {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), complex.cosh (f x)) ((complex.sinh (f x)) * f') s x
theorem deriv_within_ccosh {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.cosh (f x)) s x = (complex.sinh (f x)) * deriv_within f s x
@[simp]
theorem deriv_ccosh {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.cosh (f x)) x = (complex.sinh (f x)) * deriv f x

complex.sinh #

theorem has_strict_deriv_at.csinh {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), complex.sinh (f x)) ((complex.cosh (f x)) * f') x
theorem has_deriv_at.csinh {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), complex.sinh (f x)) ((complex.cosh (f x)) * f') x
theorem has_deriv_within_at.csinh {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), complex.sinh (f x)) ((complex.cosh (f x)) * f') s x
theorem deriv_within_csinh {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.sinh (f x)) s x = (complex.cosh (f x)) * deriv_within f s x
@[simp]
theorem deriv_csinh {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.sinh (f x)) x = (complex.cosh (f x)) * deriv f x

Simp lemmas for derivatives of λ x, complex.cos (f x) etc., f : E → ℂ #

complex.cos #

theorem has_strict_fderiv_at.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), complex.cos (f x)) (-complex.sin (f x) f') x
theorem has_fderiv_at.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), complex.cos (f x)) (-complex.sin (f x) f') x
theorem has_fderiv_within_at.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), complex.cos (f x)) (-complex.sin (f x) f') s x
theorem differentiable_within_at.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), complex.cos (f x)) s x
@[simp]
theorem differentiable_at.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), complex.cos (f x)) x
theorem differentiable_on.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), complex.cos (f x)) s
@[simp]
theorem differentiable.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), complex.cos (f x))
theorem fderiv_within_ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), complex.cos (f x)) s x = -complex.sin (f x) fderiv_within f s x
@[simp]
theorem fderiv_ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), complex.cos (f x)) x = -complex.sin (f x) fderiv f x
theorem times_cont_diff.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), complex.cos (f x))
theorem times_cont_diff_at.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), complex.cos (f x)) x
theorem times_cont_diff_on.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), complex.cos (f x)) s
theorem times_cont_diff_within_at.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), complex.cos (f x)) s x

complex.sin #

theorem has_strict_fderiv_at.csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), complex.sin (f x)) (complex.cos (f x) f') x
theorem has_fderiv_at.csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), complex.sin (f x)) (complex.cos (f x) f') x
theorem has_fderiv_within_at.csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), complex.sin (f x)) (complex.cos (f x) f') s x
theorem differentiable_within_at.csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), complex.sin (f x)) s x
@[simp]
theorem differentiable_at.csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), complex.sin (f x)) x
theorem differentiable_on.csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), complex.sin (f x)) s
@[simp]
theorem differentiable.csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), complex.sin (f x))
theorem fderiv_within_csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), complex.sin (f x)) s x = complex.cos (f x) fderiv_within f s x
@[simp]
theorem fderiv_csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), complex.sin (f x)) x = complex.cos (f x) fderiv f x
theorem times_cont_diff.csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), complex.sin (f x))
theorem times_cont_diff_at.csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), complex.sin (f x)) x
theorem times_cont_diff_on.csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), complex.sin (f x)) s
theorem times_cont_diff_within_at.csin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), complex.sin (f x)) s x

complex.cosh #

theorem has_strict_fderiv_at.ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), complex.cosh (f x)) (complex.sinh (f x) f') x
theorem has_fderiv_at.ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), complex.cosh (f x)) (complex.sinh (f x) f') x
theorem has_fderiv_within_at.ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), complex.cosh (f x)) (complex.sinh (f x) f') s x
theorem differentiable_within_at.ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), complex.cosh (f x)) s x
@[simp]
theorem differentiable_at.ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), complex.cosh (f x)) x
theorem differentiable_on.ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), complex.cosh (f x)) s
@[simp]
theorem differentiable.ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), complex.cosh (f x))
theorem fderiv_within_ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), complex.cosh (f x)) s x = complex.sinh (f x) fderiv_within f s x
@[simp]
theorem fderiv_ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), complex.cosh (f x)) x = complex.sinh (f x) fderiv f x
theorem times_cont_diff.ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), complex.cosh (f x))
theorem times_cont_diff_at.ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), complex.cosh (f x)) x
theorem times_cont_diff_on.ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), complex.cosh (f x)) s
theorem times_cont_diff_within_at.ccosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), complex.cosh (f x)) s x

complex.sinh #

theorem has_strict_fderiv_at.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), complex.sinh (f x)) (complex.cosh (f x) f') x
theorem has_fderiv_at.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), complex.sinh (f x)) (complex.cosh (f x) f') x
theorem has_fderiv_within_at.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), complex.sinh (f x)) (complex.cosh (f x) f') s x
theorem differentiable_within_at.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), complex.sinh (f x)) s x
@[simp]
theorem differentiable_at.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), complex.sinh (f x)) x
theorem differentiable_on.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), complex.sinh (f x)) s
@[simp]
theorem differentiable.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), complex.sinh (f x))
theorem fderiv_within_csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), complex.sinh (f x)) s x = complex.cosh (f x) fderiv_within f s x
@[simp]
theorem fderiv_csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), complex.sinh (f x)) x = complex.cosh (f x) fderiv f x
theorem times_cont_diff.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), complex.sinh (f x))
theorem times_cont_diff_at.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), complex.sinh (f x)) x
theorem times_cont_diff_on.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), complex.sinh (f x)) s
theorem times_cont_diff_within_at.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), complex.sinh (f x)) s x
@[simp]
theorem real.deriv_cos'  :

sinh is strictly monotone.

Simp lemmas for derivatives of λ x, real.cos (f x) etc., f : ℝ → ℝ #

real.cos #

theorem has_strict_deriv_at.cos {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), real.cos (f x)) ((-real.sin (f x)) * f') x
theorem has_deriv_at.cos {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), real.cos (f x)) ((-real.sin (f x)) * f') x
theorem has_deriv_within_at.cos {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), real.cos (f x)) ((-real.sin (f x)) * f') s x
theorem deriv_within_cos {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.cos (f x)) s x = (-real.sin (f x)) * deriv_within f s x
@[simp]
theorem deriv_cos {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.cos (f x)) x = (-real.sin (f x)) * deriv f x

real.sin #

theorem has_strict_deriv_at.sin {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), real.sin (f x)) ((real.cos (f x)) * f') x
theorem has_deriv_at.sin {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), real.sin (f x)) ((real.cos (f x)) * f') x
theorem has_deriv_within_at.sin {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), real.sin (f x)) ((real.cos (f x)) * f') s x
theorem deriv_within_sin {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.sin (f x)) s x = (real.cos (f x)) * deriv_within f s x
@[simp]
theorem deriv_sin {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.sin (f x)) x = (real.cos (f x)) * deriv f x

real.cosh #

theorem has_strict_deriv_at.cosh {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), real.cosh (f x)) ((real.sinh (f x)) * f') x
theorem has_deriv_at.cosh {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), real.cosh (f x)) ((real.sinh (f x)) * f') x
theorem has_deriv_within_at.cosh {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), real.cosh (f x)) ((real.sinh (f x)) * f') s x
theorem deriv_within_cosh {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.cosh (f x)) s x = (real.sinh (f x)) * deriv_within f s x
@[simp]
theorem deriv_cosh {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.cosh (f x)) x = (real.sinh (f x)) * deriv f x

real.sinh #

theorem has_strict_deriv_at.sinh {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), real.sinh (f x)) ((real.cosh (f x)) * f') x
theorem has_deriv_at.sinh {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), real.sinh (f x)) ((real.cosh (f x)) * f') x
theorem has_deriv_within_at.sinh {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), real.sinh (f x)) ((real.cosh (f x)) * f') s x
theorem deriv_within_sinh {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.sinh (f x)) s x = (real.cosh (f x)) * deriv_within f s x
@[simp]
theorem deriv_sinh {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.sinh (f x)) x = (real.cosh (f x)) * deriv f x

Simp lemmas for derivatives of λ x, real.cos (f x) etc., f : E → ℝ #

real.cos #

theorem has_strict_fderiv_at.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.cos (f x)) (-real.sin (f x) f') x
theorem has_fderiv_at.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.cos (f x)) (-real.sin (f x) f') x
theorem has_fderiv_within_at.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.cos (f x)) (-real.sin (f x) f') s x
theorem differentiable_within_at.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), real.cos (f x)) s x
@[simp]
theorem differentiable_at.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.cos (f x)) x
theorem differentiable_on.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.cos (f x)) s
@[simp]
theorem differentiable.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), real.cos (f x))
theorem fderiv_within_cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.cos (f x)) s x = -real.sin (f x) fderiv_within f s x
@[simp]
theorem fderiv_cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.cos (f x)) x = -real.sin (f x) fderiv f x
theorem times_cont_diff.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), real.cos (f x))
theorem times_cont_diff_at.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), real.cos (f x)) x
theorem times_cont_diff_on.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), real.cos (f x)) s
theorem times_cont_diff_within_at.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), real.cos (f x)) s x

real.sin #

theorem has_strict_fderiv_at.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.sin (f x)) (real.cos (f x) f') x
theorem has_fderiv_at.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.sin (f x)) (real.cos (f x) f') x
theorem has_fderiv_within_at.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.sin (f x)) (real.cos (f x) f') s x
theorem differentiable_within_at.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), real.sin (f x)) s x
@[simp]
theorem differentiable_at.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.sin (f x)) x
theorem differentiable_on.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.sin (f x)) s
@[simp]
theorem differentiable.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), real.sin (f x))
theorem fderiv_within_sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.sin (f x)) s x = real.cos (f x) fderiv_within f s x
@[simp]
theorem fderiv_sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.sin (f x)) x = real.cos (f x) fderiv f x
theorem times_cont_diff.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), real.sin (f x))
theorem times_cont_diff_at.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), real.sin (f x)) x
theorem times_cont_diff_on.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), real.sin (f x)) s
theorem times_cont_diff_within_at.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), real.sin (f x)) s x

real.cosh #

theorem has_strict_fderiv_at.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.cosh (f x)) (real.sinh (f x) f') x
theorem has_fderiv_at.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.cosh (f x)) (real.sinh (f x) f') x
theorem has_fderiv_within_at.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.cosh (f x)) (real.sinh (f x) f') s x
theorem differentiable_within_at.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), real.cosh (f x)) s x
@[simp]
theorem differentiable_at.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.cosh (f x)) x
theorem differentiable_on.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.cosh (f x)) s
@[simp]
theorem differentiable.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), real.cosh (f x))
theorem fderiv_within_cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.cosh (f x)) s x = real.sinh (f x) fderiv_within f s x
@[simp]
theorem fderiv_cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.cosh (f x)) x = real.sinh (f x) fderiv f x
theorem times_cont_diff.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), real.cosh (f x))
theorem times_cont_diff_at.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), real.cosh (f x)) x
theorem times_cont_diff_on.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), real.cosh (f x)) s
theorem times_cont_diff_within_at.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), real.cosh (f x)) s x

real.sinh #

theorem has_strict_fderiv_at.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.sinh (f x)) (real.cosh (f x) f') x
theorem has_fderiv_at.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.sinh (f x)) (real.cosh (f x) f') x
theorem has_fderiv_within_at.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.sinh (f x)) (real.cosh (f x) f') s x
theorem differentiable_within_at.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), real.sinh (f x)) s x
@[simp]
theorem differentiable_at.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.sinh (f x)) x
theorem differentiable_on.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.sinh (f x)) s
@[simp]
theorem differentiable.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), real.sinh (f x))
theorem fderiv_within_sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.sinh (f x)) s x = real.cosh (f x) fderiv_within f s x
@[simp]
theorem fderiv_sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.sinh (f x)) x = real.cosh (f x) fderiv f x
theorem times_cont_diff.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), real.sinh (f x))
theorem times_cont_diff_at.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), real.sinh (f x)) x
theorem times_cont_diff_on.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), real.sinh (f x)) s
theorem times_cont_diff_within_at.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), real.sinh (f x)) s x
def real.pi  :

The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2], from which one can derive all its properties. For explicit bounds on π, see data.real.pi.

Equations
@[simp]
theorem real.cos_pi_div_two  :
real.cos (π / 2) = 0
theorem real.two_le_pi  :
theorem real.pi_le_four  :
theorem real.pi_pos  :
0 < π
theorem real.pi_ne_zero  :
theorem real.pi_div_two_pos  :
0 < π / 2
theorem real.two_pi_pos  :
0 < 2 * π
def nnreal.pi  :

π considered as a nonnegative real.

Equations
@[simp]
@[simp]
theorem real.sin_pi  :
@[simp]
theorem real.cos_pi  :
@[simp]
theorem real.sin_two_pi  :
real.sin (2 * π) = 0
@[simp]
theorem real.cos_two_pi  :
real.cos (2 * π) = 1
theorem real.sin_add_pi (x : ) :
theorem real.sin_add_two_pi (x : ) :
theorem real.sin_sub_pi (x : ) :
theorem real.sin_sub_two_pi (x : ) :
theorem real.sin_pi_sub (x : ) :
theorem real.sin_two_pi_sub (x : ) :
theorem real.sin_nat_mul_pi (n : ) :
real.sin ((n) * π) = 0
theorem real.sin_int_mul_pi (n : ) :
real.sin ((n) * π) = 0
theorem real.sin_add_nat_mul_two_pi (x : ) (n : ) :
real.sin (x + (n) * 2 * π) = real.sin x
theorem real.sin_add_int_mul_two_pi (x : ) (n : ) :
real.sin (x + (n) * 2 * π) = real.sin x
theorem real.sin_sub_nat_mul_two_pi (x : ) (n : ) :
real.sin (x - (n) * 2 * π) = real.sin x
theorem real.sin_sub_int_mul_two_pi (x : ) (n : ) :
real.sin (x - (n) * 2 * π) = real.sin x
theorem real.sin_nat_mul_two_pi_sub (x : ) (n : ) :
real.sin ((n) * 2 * π - x) = -real.sin x
theorem real.sin_int_mul_two_pi_sub (x : ) (n : ) :
real.sin ((n) * 2 * π - x) = -real.sin x
theorem real.cos_add_pi (x : ) :
theorem real.cos_add_two_pi (x : ) :
theorem real.cos_sub_pi (x : ) :
theorem real.cos_sub_two_pi (x : ) :
theorem real.cos_pi_sub (x : ) :
theorem real.cos_two_pi_sub (x : ) :
theorem real.cos_nat_mul_two_pi (n : ) :
real.cos ((n) * 2 * π) = 1
theorem real.cos_int_mul_two_pi (n : ) :
real.cos ((n) * 2 * π) = 1
theorem real.cos_add_nat_mul_two_pi (x : ) (n : ) :
real.cos (x + (n) * 2 * π) = real.cos x
theorem real.cos_add_int_mul_two_pi (x : ) (n : ) :
real.cos (x + (n) * 2 * π) = real.cos x
theorem real.cos_sub_nat_mul_two_pi (x : ) (n : ) :
real.cos (x - (n) * 2 * π) = real.cos x
theorem real.cos_sub_int_mul_two_pi (x : ) (n : ) :
real.cos (x - (n) * 2 * π) = real.cos x
theorem real.cos_nat_mul_two_pi_sub (x : ) (n : ) :
real.cos ((n) * 2 * π - x) = real.cos x
theorem real.cos_int_mul_two_pi_sub (x : ) (n : ) :
real.cos ((n) * 2 * π - x) = real.cos x
theorem real.cos_nat_mul_two_pi_add_pi (n : ) :
real.cos ((n) * 2 * π + π) = -1
theorem real.cos_int_mul_two_pi_add_pi (n : ) :
real.cos ((n) * 2 * π + π) = -1
theorem real.cos_nat_mul_two_pi_sub_pi (n : ) :
real.cos ((n) * 2 * π - π) = -1
theorem real.cos_int_mul_two_pi_sub_pi (n : ) :
real.cos ((n) * 2 * π - π) = -1
theorem real.sin_pos_of_pos_of_lt_pi {x : } (h0x : 0 < x) (hxp : x < π) :
theorem real.sin_pos_of_mem_Ioo {x : } (hx : x set.Ioo 0 π) :
theorem real.sin_nonneg_of_mem_Icc {x : } (hx : x set.Icc 0 π) :
theorem real.sin_nonneg_of_nonneg_of_le_pi {x : } (h0x : 0 x) (hxp : x π) :
theorem real.sin_neg_of_neg_of_neg_pi_lt {x : } (hx0 : x < 0) (hpx : -π < x) :
theorem real.sin_nonpos_of_nonnpos_of_neg_pi_le {x : } (hx0 : x 0) (hpx : -π x) :
@[simp]
theorem real.sin_pi_div_two  :
real.sin (π / 2) = 1
theorem real.cos_pos_of_mem_Ioo {x : } (hx : x set.Ioo (-(π / 2)) (π / 2)) :
theorem real.cos_nonneg_of_mem_Icc {x : } (hx : x set.Icc (-(π / 2)) (π / 2)) :
theorem real.cos_nonneg_of_neg_pi_div_two_le_of_le {x : } (hl : -(π / 2) x) (hu : x π / 2) :
theorem real.cos_neg_of_pi_div_two_lt_of_lt {x : } (hx₁ : π / 2 < x) (hx₂ : x < π + π / 2) :
theorem real.cos_nonpos_of_pi_div_two_le_of_le {x : } (hx₁ : π / 2 x) (hx₂ : x π + π / 2) :
theorem real.sin_eq_sqrt_one_sub_cos_sq {x : } (hl : 0 x) (hu : x π) :
theorem real.cos_eq_sqrt_one_sub_sin_sq {x : } (hl : -(π / 2) x) (hu : x π / 2) :
theorem real.sin_eq_zero_iff_of_lt_of_lt {x : } (hx₁ : -π < x) (hx₂ : x < π) :
real.sin x = 0 x = 0
theorem real.sin_eq_zero_iff {x : } :
real.sin x = 0 ∃ (n : ), (n) * π = x
theorem real.sin_ne_zero_iff {x : } :
real.sin x 0 ∀ (n : ), (n) * π x
theorem real.cos_eq_one_iff (x : ) :
real.cos x = 1 ∃ (n : ), (n) * 2 * π = x
theorem real.cos_eq_one_iff_of_lt_of_lt {x : } (hx₁ : -2 * π < x) (hx₂ : x < 2 * π) :
real.cos x = 1 x = 0
theorem real.cos_lt_cos_of_nonneg_of_le_pi_div_two {x y : } (hx₁ : 0 x) (hy₂ : y π / 2) (hxy : x < y) :
theorem real.cos_lt_cos_of_nonneg_of_le_pi {x y : } (hx₁ : 0 x) (hy₂ : y π) (hxy : x < y) :
theorem real.cos_le_cos_of_nonneg_of_le_pi {x y : } (hx₁ : 0 x) (hy₂ : y π) (hxy : x y) :
theorem real.sin_lt_sin_of_lt_of_le_pi_div_two {x y : } (hx₁ : -(π / 2) x) (hy₂ : y π / 2) (hxy : x < y) :
theorem real.sin_le_sin_of_le_of_le_pi_div_two {x y : } (hx₁ : -(π / 2) x) (hy₂ : y π / 2) (hxy : x y) :
theorem real.surj_on_sin  :
set.surj_on real.sin (set.Icc (-(π / 2)) (π / 2)) (set.Icc (-1) 1)
theorem real.sin_mem_Icc (x : ) :
theorem real.cos_mem_Icc (x : ) :
theorem real.maps_to_sin (s : set ) :
theorem real.maps_to_cos (s : set ) :
theorem real.bij_on_sin  :
set.bij_on real.sin (set.Icc (-(π / 2)) (π / 2)) (set.Icc (-1) 1)
@[simp]
@[simp]
theorem real.sin_lt {x : } (h : 0 < x) :
theorem real.sin_gt_sub_cube {x : } (h : 0 < x) (h' : x 1) :
x - x ^ 3 / 4 < real.sin x
@[simp]
def real.sqrt_two_add_series (x : ) :

the series sqrt_two_add_series x n is sqrt(2 + sqrt(2 + ... )) with n square roots, starting with x. We define it here because cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2

Equations
@[simp]
theorem real.cos_pi_over_two_pow (n : ) :
theorem real.sin_sq_pi_over_two_pow (n : ) :
real.sin (π / 2 ^ (n + 1)) ^ 2 = 1 - (real.sqrt_two_add_series 0 n / 2) ^ 2
@[simp]
@[simp]
theorem real.cos_pi_div_four  :
@[simp]
theorem real.sin_pi_div_four  :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem real.cos_pi_div_three  :
real.cos (π / 3) = 1 / 2

The cosine of π / 3 is 1 / 2.

theorem real.sq_cos_pi_div_six  :
real.cos (π / 6) ^ 2 = 3 / 4

The square of the cosine of π / 6 is 3 / 4 (this is sometimes more convenient than the result for cosine itself).

@[simp]
theorem real.cos_pi_div_six  :

The cosine of π / 6 is √3 / 2.

@[simp]
theorem real.sin_pi_div_six  :
real.sin (π / 6) = 1 / 2

The sine of π / 6 is 1 / 2.

theorem real.sq_sin_pi_div_three  :
real.sin (π / 3) ^ 2 = 3 / 4

The square of the sine of π / 3 is 3 / 4 (this is sometimes more convenient than the result for cosine itself).

@[simp]

The sine of π / 3 is √3 / 2.

def real.angle  :
Type

The type of angles

Equations
@[simp]
theorem real.angle.coe_zero  :
0 = 0
@[simp]
theorem real.angle.coe_add (x y : ) :
(x + y) = x + y
@[simp]
theorem real.angle.coe_neg (x : ) :
@[simp]
theorem real.angle.coe_sub (x y : ) :
(x - y) = x - y
@[simp]
theorem real.angle.coe_nat_mul_eq_nsmul (x : ) (n : ) :
(n) * x = n x
@[simp]
theorem real.angle.coe_int_mul_eq_gsmul (x : ) (n : ) :
(n) * x = n x
@[simp]
theorem real.angle.coe_two_pi  :
2 * π = 0
theorem real.angle.angle_eq_iff_two_pi_dvd_sub {ψ θ : } :
θ = ψ ∃ (k : ), θ - ψ = (2 * π) * k
theorem real.angle.cos_sin_inj {θ ψ : } (Hcos : real.cos θ = real.cos ψ) (Hsin : real.sin θ = real.sin ψ) :
θ = ψ
def real.sin_order_iso  :
(set.Icc (-(π / 2)) (π / 2)) ≃o (set.Icc (-1) 1)

real.sin as an order_iso between [-(π / 2), π / 2] and [-1, 1].

Equations
def real.arcsin  :

Inverse of the sin function, returns values in the range -π / 2 ≤ arcsin x ≤ π / 2. It defaults to -π / 2 on (-∞, -1) and to π / 2 to (1, ∞).

Equations
theorem real.arcsin_mem_Icc (x : ) :
@[simp]
theorem real.sin_arcsin' {x : } (hx : x set.Icc (-1) 1) :
theorem real.sin_arcsin {x : } (hx₁ : -1 x) (hx₂ : x 1) :
theorem real.arcsin_sin' {x : } (hx : x set.Icc (-(π / 2)) (π / 2)) :
theorem real.arcsin_sin {x : } (hx₁ : -(π / 2) x) (hx₂ : x π / 2) :
theorem real.arcsin_inj {x y : } (hx₁ : -1 x) (hx₂ : x 1) (hy₁ : -1 y) (hy₂ : y 1) :
theorem real.arcsin_eq_of_sin_eq {x y : } (h₁ : real.sin x = y) (h₂ : x set.Icc (-(π / 2)) (π / 2)) :
@[simp]
theorem real.arcsin_zero  :
@[simp]
theorem real.arcsin_one  :
theorem real.arcsin_of_one_le {x : } (hx : 1 x) :
theorem real.arcsin_neg_one  :
real.arcsin (-1) = -(π / 2)
theorem real.arcsin_of_le_neg_one {x : } (hx : x -1) :
@[simp]
theorem real.arcsin_neg (x : ) :
theorem real.arcsin_le_iff_le_sin {x y : } (hx : x set.Icc (-1) 1) (hy : y set.Icc (-(π / 2)) (π / 2)) :
theorem real.arcsin_le_iff_le_sin' {x y : } (hy : y set.Ico (-(π / 2)) (π / 2)) :
theorem real.le_arcsin_iff_sin_le {x y : } (hx : x set.Icc (-(π / 2)) (π / 2)) (hy : y set.Icc (-1) 1) :
theorem real.le_arcsin_iff_sin_le' {x y : } (hx : x set.Ioc (-(π / 2)) (π / 2)) :
theorem real.arcsin_lt_iff_lt_sin {x y : } (hx : x set.Icc (-1) 1) (hy : y set.Icc (-(π / 2)) (π / 2)) :
theorem real.arcsin_lt_iff_lt_sin' {x y : } (hy : y set.Ioc (-(π / 2)) (π / 2)) :
theorem real.lt_arcsin_iff_sin_lt {x y : } (hx : x set.Icc (-(π / 2)) (π / 2)) (hy : y set.Icc (-1) 1) :
theorem real.lt_arcsin_iff_sin_lt' {x y : } (hx : x set.Ico (-(π / 2)) (π / 2)) :
theorem real.arcsin_eq_iff_eq_sin {x y : } (hy : y set.Ioo (-(π / 2)) (π / 2)) :
@[simp]
theorem real.arcsin_nonneg {x : } :
@[simp]
theorem real.arcsin_nonpos {x : } :
@[simp]
theorem real.arcsin_eq_zero_iff {x : } :
real.arcsin x = 0 x = 0
@[simp]
theorem real.zero_eq_arcsin_iff {x : } :
0 = real.arcsin x x = 0
@[simp]
theorem real.arcsin_pos {x : } :
0 < real.arcsin x 0 < x
@[simp]
theorem real.arcsin_lt_zero {x : } :
real.arcsin x < 0 x < 0
@[simp]
theorem real.arcsin_lt_pi_div_two {x : } :
real.arcsin x < π / 2 x < 1
@[simp]
theorem real.neg_pi_div_two_lt_arcsin {x : } :
-(π / 2) < real.arcsin x -1 < x
@[simp]
theorem real.arcsin_eq_pi_div_two {x : } :
@[simp]
theorem real.pi_div_two_eq_arcsin {x : } :
@[simp]
theorem real.pi_div_two_le_arcsin {x : } :
@[simp]
theorem real.arcsin_eq_neg_pi_div_two {x : } :
real.arcsin x = -(π / 2) x -1
@[simp]
theorem real.neg_pi_div_two_eq_arcsin {x : } :
-(π / 2) = real.arcsin x x -1
@[simp]
theorem real.maps_to_sin_Ioo  :
set.maps_to real.sin (set.Ioo (-(π / 2)) (π / 2)) (set.Ioo (-1) 1)
@[simp]

real.sin as a local_homeomorph between (-π / 2, π / 2) and (-1, 1).

Equations
theorem real.cos_arcsin {x : } (hx₁ : -1 x) (hx₂ : x 1) :
theorem real.has_strict_deriv_at_arcsin {x : } (h₁ : x -1) (h₂ : x 1) :
theorem real.has_deriv_at_arcsin {x : } (h₁ : x -1) (h₂ : x 1) :
theorem real.times_cont_diff_at_arcsin {x : } (h₁ : x -1) (h₂ : x 1) {n : with_top } :
@[simp]
theorem real.deriv_arcsin  :
deriv real.arcsin = λ (x : ), 1 / real.sqrt (1 - x ^ 2)
def real.arccos (x : ) :

Inverse of the cos function, returns values in the range 0 ≤ arccos x and arccos x ≤ π. If the argument is not between -1 and 1 it defaults to π / 2

Equations
theorem real.cos_arccos {x : } (hx₁ : -1 x) (hx₂ : x 1) :