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 differentiable, with the derivative cos x.

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

@[simp]

The complex hyperbolic sine function is everywhere differentiable, with the derivative cosh 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 measurable.ccos {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.cos (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 measurable.csin {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.sin (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 measurable.ccosh {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.cosh (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 measurable.csinh {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.sinh (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_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_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_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_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 measurable.cos {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.cos (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 measurable.sin {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.sin (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 measurable.cosh {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.cosh (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 measurable.sinh {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.sinh (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_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_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_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_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 * π

@[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.cos_add_two_pi (x : ) :

theorem real.sin_pi_sub (x : ) :

theorem real.cos_add_pi (x : ) :

theorem real.cos_pi_sub (x : ) :

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_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_nat_mul_pi (n : ) :
real.sin ((n) * π) = 0

theorem real.sin_int_mul_pi (n : ) :
real.sin ((n) * π) = 0

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_int_mul_two_pi_add_pi (n : ) :
real.cos ((n) * 2 * π + π) = -1

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_square_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.square_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.square_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.deriv_arcsin_aux {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) :

theorem real.arccos_cos {x : } (hx₁ : 0 x) (hx₂ : x π) :

theorem real.arccos_inj {x y : } (hx₁ : -1 x) (hx₂ : x 1) (hy₁ : -1 y) (hy₂ : y 1) :

@[simp]
theorem real.arccos_zero  :

@[simp]
theorem real.arccos_one  :

@[simp]
theorem real.arccos_neg_one  :

@[simp]
theorem real.arccos_eq_zero {x : } :

@[simp]
theorem real.arccos_eq_pi_div_two {x : } :
real.arccos x = π / 2 x = 0

@[simp]
theorem real.arccos_eq_pi {x : } :

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

theorem real.has_deriv_at_arccos {x : } (h₁ : x -1) (h₂ : x 1) :

theorem real.times_cont_diff_at_arccos {x : } (h₁ : x -1) (h₂ : x 1) {n : with_top } :

@[simp]
theorem real.deriv_arccos  :
deriv real.arccos = λ (x : ), -(1 / real.sqrt (1 - x ^ 2))

@[simp]
theorem real.tan_pi_div_four  :
real.tan (π / 4) = 1

@[simp]
theorem real.tan_pi_div_two  :
real.tan (π / 2) = 0

theorem real.tan_pos_of_pos_of_lt_pi_div_two {x : } (h0x : 0 < x) (hxp : x < π / 2) :

theorem real.tan_nonneg_of_nonneg_of_le_pi_div_two {x : } (h0x : 0 x) (hxp : x π / 2) :

theorem real.tan_neg_of_neg_of_pi_div_two_lt {x : } (hx0 : x < 0) (hpx : -(π / 2) < x) :

theorem real.tan_nonpos_of_nonpos_of_neg_pi_div_two_le {x : } (hx0 : x 0) (hpx : -(π / 2) x) :

theorem real.tan_lt_tan_of_nonneg_of_lt_pi_div_two {x y : } (hx₁ : 0 x) (hy₂ : y < π / 2) (hxy : x < y) :

theorem real.tan_lt_tan_of_lt_of_lt_pi_div_two {x y : } (hx₁ : -(π / 2) < x) (hy₂ : y < π / 2) (hxy : x < y) :

theorem real.tan_inj_of_lt_of_lt_pi_div_two {x y : } (hx₁ : -(π / 2) < x) (hx₂ : x < π / 2) (hy₁ : -(π / 2) < y) (hy₂ : y < π / 2) (hxy : real.tan x = real.tan y) :
x = y

def complex.arg (x : ) :

arg returns values in the range (-π, π], such that for x ≠ 0, sin (arg x) = x.im / x.abs and cos (arg x) = x.re / x.abs, arg 0 defaults to 0

Equations
theorem complex.arg_le_pi (x : ) :

theorem complex.neg_pi_lt_arg (x : ) :

theorem complex.arg_eq_arg_neg_add_pi_of_im_nonneg_of_re_neg {x : } (hxr : x.re < 0) (hxi : 0 x.im) :
x.arg = (-x).arg + π

theorem complex.arg_eq_arg_neg_sub_pi_of_im_neg_of_re_neg {x : } (hxr : x.re < 0) (hxi : x.im < 0) :
x.arg = (-x).arg - π

@[simp]
theorem complex.arg_zero  :
0.arg = 0

@[simp]
theorem complex.arg_one  :
1.arg = 0

@[simp]
theorem complex.arg_neg_one  :
(-1).arg = π

@[simp]
theorem complex.arg_I  :

@[simp]
theorem complex.arg_neg_I  :

theorem complex.cos_arg {x : } (hx : x 0) :

theorem complex.tan_arg {x : } :

theorem complex.arg_cos_add_sin_mul_I {x : } (hx₁ : -π < x) (hx₂ : x π) :

theorem complex.arg_eq_arg_iff {x y : } (hx : x 0) (hy : y 0) :

theorem complex.arg_real_mul (x : ) {r : } (hr : 0 < r) :
((r) * x).arg = x.arg

theorem complex.ext_abs_arg {x y : } (h₁ : complex.abs x = complex.abs y) (h₂ : x.arg = y.arg) :
x = y

theorem complex.arg_of_real_of_nonneg {x : } (hx : 0 x) :
x.arg = 0

theorem complex.arg_of_real_of_neg {x : } (hx : x < 0) :

def complex.log (x : ) :

Inverse of the exp function. Returns values such that (log x).im > - π and (log x).im ≤ π. log 0 = 0

Equations