# mathlibdocumentation

analysis.special_functions.trigonometric

# Trigonometric functions

## Main definitions

This file contains the following definitions:

• π, arcsin, arccos, arctan
• argument of a complex number
• logarithm on complex numbers

## 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.

• `polynomial.chebyshev₁_complex_cos`: the `n`-th Chebyshev polynomial evaluates on `complex.cos θ` to the value `n * complex.cos θ`.

## Tags

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

theorem complex.has_deriv_at_sin (x : ) :

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

@[simp]

theorem complex.has_deriv_at_cos (x : ) :

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

theorem complex.deriv_cos {x : } :

@[simp]
theorem complex.deriv_cos'  :
= λ (x : ),

theorem complex.has_deriv_at_sinh (x : ) :

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

@[simp]

theorem complex.has_deriv_at_cosh (x : ) :

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

@[simp]

Register lemmas for the derivatives of the composition of `complex.cos`, `complex.sin`, `complex.cosh` and `complex.sinh` with a differentiable function, for standalone use and use with `simp`.

`complex.cos`

theorem measurable.ccos {f : } :
measurable (λ (x : ), complex.cos (f x))

theorem has_deriv_at.ccos {f : } {f' x : } :
f' xhas_deriv_at (λ (x : ), complex.cos (f x)) ((-complex.sin (f x)) * f') x

theorem has_deriv_within_at.ccos {f : } {f' x : } {s : set } :
s xhas_deriv_within_at (λ (x : ), complex.cos (f x)) ((-complex.sin (f x)) * f') s x

theorem differentiable_within_at.ccos {f : } {x : } {s : set } :
(λ (x : ), complex.cos (f x)) s x

@[simp]
theorem differentiable_at.ccos {f : } {x : } :
(λ (x : ), complex.cos (f x)) x

theorem differentiable_on.ccos {f : } {s : set } :
(λ (x : ), complex.cos (f x)) s

@[simp]
theorem differentiable.ccos {f : } :
(λ (x : ), complex.cos (f x))

theorem deriv_within_ccos {f : } {x : } {s : set } :
deriv_within (λ (x : ), complex.cos (f x)) s x = (-complex.sin (f x)) * s x

@[simp]
theorem deriv_ccos {f : } {x : } :
deriv (λ (x : ), complex.cos (f x)) x = (-complex.sin (f x)) * x

`complex.sin`

theorem measurable.csin {f : } :
measurable (λ (x : ), complex.sin (f x))

theorem has_deriv_at.csin {f : } {f' x : } :
f' xhas_deriv_at (λ (x : ), complex.sin (f x)) ((complex.cos (f x)) * f') x

theorem has_deriv_within_at.csin {f : } {f' x : } {s : set } :
s xhas_deriv_within_at (λ (x : ), complex.sin (f x)) ((complex.cos (f x)) * f') s x

theorem differentiable_within_at.csin {f : } {x : } {s : set } :
(λ (x : ), complex.sin (f x)) s x

@[simp]
theorem differentiable_at.csin {f : } {x : } :
(λ (x : ), complex.sin (f x)) x

theorem differentiable_on.csin {f : } {s : set } :
(λ (x : ), complex.sin (f x)) s

@[simp]
theorem differentiable.csin {f : } :
(λ (x : ), complex.sin (f x))

theorem deriv_within_csin {f : } {x : } {s : set } :
deriv_within (λ (x : ), complex.sin (f x)) s x = (complex.cos (f x)) * s x

@[simp]
theorem deriv_csin {f : } {x : } :
deriv (λ (x : ), complex.sin (f x)) x = (complex.cos (f x)) * x

`complex.cosh`

theorem measurable.ccosh {f : } :
measurable (λ (x : ), complex.cosh (f x))

theorem has_deriv_at.ccosh {f : } {f' x : } :
f' xhas_deriv_at (λ (x : ), complex.cosh (f x)) ((complex.sinh (f x)) * f') x

theorem has_deriv_within_at.ccosh {f : } {f' x : } {s : set } :
s xhas_deriv_within_at (λ (x : ), complex.cosh (f x)) ((complex.sinh (f x)) * f') s x

theorem differentiable_within_at.ccosh {f : } {x : } {s : set } :
(λ (x : ), complex.cosh (f x)) s x

@[simp]
theorem differentiable_at.ccosh {f : } {x : } :
(λ (x : ), complex.cosh (f x)) x

theorem differentiable_on.ccosh {f : } {s : set } :
(λ (x : ), complex.cosh (f x)) s

@[simp]
theorem differentiable.ccosh {f : } :
(λ (x : ), complex.cosh (f x))

theorem deriv_within_ccosh {f : } {x : } {s : set } :
deriv_within (λ (x : ), complex.cosh (f x)) s x = (complex.sinh (f x)) * s x

@[simp]
theorem deriv_ccosh {f : } {x : } :
deriv (λ (x : ), complex.cosh (f x)) x = (complex.sinh (f x)) * x

`complex.sinh`

theorem measurable.csinh {f : } :
measurable (λ (x : ), complex.sinh (f x))

theorem has_deriv_at.csinh {f : } {f' x : } :
f' xhas_deriv_at (λ (x : ), complex.sinh (f x)) ((complex.cosh (f x)) * f') x

theorem has_deriv_within_at.csinh {f : } {f' x : } {s : set } :
s xhas_deriv_within_at (λ (x : ), complex.sinh (f x)) ((complex.cosh (f x)) * f') s x

theorem differentiable_within_at.csinh {f : } {x : } {s : set } :
(λ (x : ), complex.sinh (f x)) s x

@[simp]
theorem differentiable_at.csinh {f : } {x : } :
(λ (x : ), complex.sinh (f x)) x

theorem differentiable_on.csinh {f : } {s : set } :
(λ (x : ), complex.sinh (f x)) s

@[simp]
theorem differentiable.csinh {f : } :
(λ (x : ), complex.sinh (f x))

theorem deriv_within_csinh {f : } {x : } {s : set } :
deriv_within (λ (x : ), complex.sinh (f x)) s x = (complex.cosh (f x)) * s x

@[simp]
theorem deriv_csinh {f : } {x : } :
deriv (λ (x : ), complex.sinh (f x)) x = (complex.cosh (f x)) * x

theorem real.has_deriv_at_sin (x : ) :
x

@[simp]
theorem real.deriv_sin  :

theorem real.has_deriv_at_cos (x : ) :

theorem real.deriv_cos {x : } :

@[simp]
theorem real.deriv_cos'  :
= λ (x : ),

theorem real.has_deriv_at_sinh (x : ) :

@[simp]
theorem real.deriv_sinh  :

theorem real.has_deriv_at_cosh (x : ) :

@[simp]
theorem real.deriv_cosh  :

`sinh` is strictly monotone.

Register lemmas for the derivatives of the composition of `real.exp`, `real.cos`, `real.sin`, `real.cosh` and `real.sinh` with a differentiable function, for standalone use and use with `simp`.

`real.cos`

theorem measurable.cos {f : } :
measurable (λ (x : ), real.cos (f x))

theorem has_deriv_at.cos {f : } {f' x : } :
f' xhas_deriv_at (λ (x : ), real.cos (f x)) ((-real.sin (f x)) * f') x

theorem has_deriv_within_at.cos {f : } {f' x : } {s : set } :
s xhas_deriv_within_at (λ (x : ), real.cos (f x)) ((-real.sin (f x)) * f') s x

theorem differentiable_within_at.cos {f : } {x : } {s : set } :
(λ (x : ), real.cos (f x)) s x

@[simp]
theorem differentiable_at.cos {f : } {x : } :
(λ (x : ), real.cos (f x)) x

theorem differentiable_on.cos {f : } {s : set } :
(λ (x : ), real.cos (f x)) s

@[simp]
theorem differentiable.cos {f : } :
(λ (x : ), real.cos (f x))

theorem deriv_within_cos {f : } {x : } {s : set } :
deriv_within (λ (x : ), real.cos (f x)) s x = (-real.sin (f x)) * s x

@[simp]
theorem deriv_cos {f : } {x : } :
deriv (λ (x : ), real.cos (f x)) x = (-real.sin (f x)) * x

`real.sin`

theorem measurable.sin {f : } :
measurable (λ (x : ), real.sin (f x))

theorem has_deriv_at.sin {f : } {f' x : } :
f' xhas_deriv_at (λ (x : ), real.sin (f x)) ((real.cos (f x)) * f') x

theorem has_deriv_within_at.sin {f : } {f' x : } {s : set } :
s xhas_deriv_within_at (λ (x : ), real.sin (f x)) ((real.cos (f x)) * f') s x

theorem differentiable_within_at.sin {f : } {x : } {s : set } :
(λ (x : ), real.sin (f x)) s x

@[simp]
theorem differentiable_at.sin {f : } {x : } :
(λ (x : ), real.sin (f x)) x

theorem differentiable_on.sin {f : } {s : set } :
(λ (x : ), real.sin (f x)) s

@[simp]
theorem differentiable.sin {f : } :
(λ (x : ), real.sin (f x))

theorem deriv_within_sin {f : } {x : } {s : set } :
deriv_within (λ (x : ), real.sin (f x)) s x = (real.cos (f x)) * s x

@[simp]
theorem deriv_sin {f : } {x : } :
deriv (λ (x : ), real.sin (f x)) x = (real.cos (f x)) * x

`real.cosh`

theorem measurable.cosh {f : } :
measurable (λ (x : ), real.cosh (f x))

theorem has_deriv_at.cosh {f : } {f' x : } :
f' xhas_deriv_at (λ (x : ), real.cosh (f x)) ((real.sinh (f x)) * f') x

theorem has_deriv_within_at.cosh {f : } {f' x : } {s : set } :
s xhas_deriv_within_at (λ (x : ), real.cosh (f x)) ((real.sinh (f x)) * f') s x

theorem differentiable_within_at.cosh {f : } {x : } {s : set } :
(λ (x : ), real.cosh (f x)) s x

@[simp]
theorem differentiable_at.cosh {f : } {x : } :
(λ (x : ), real.cosh (f x)) x

theorem differentiable_on.cosh {f : } {s : set } :
(λ (x : ), real.cosh (f x)) s

@[simp]
theorem differentiable.cosh {f : } :
(λ (x : ), real.cosh (f x))

theorem deriv_within_cosh {f : } {x : } {s : set } :
deriv_within (λ (x : ), real.cosh (f x)) s x = (real.sinh (f x)) * s x

@[simp]
theorem deriv_cosh {f : } {x : } :
deriv (λ (x : ), real.cosh (f x)) x = (real.sinh (f x)) * x

`real.sinh`

theorem measurable.sinh {f : } :
measurable (λ (x : ), real.sinh (f x))

theorem has_deriv_at.sinh {f : } {f' x : } :
f' xhas_deriv_at (λ (x : ), real.sinh (f x)) ((real.cosh (f x)) * f') x

theorem has_deriv_within_at.sinh {f : } {f' x : } {s : set } :
s xhas_deriv_within_at (λ (x : ), real.sinh (f x)) ((real.cosh (f x)) * f') s x

theorem differentiable_within_at.sinh {f : } {x : } {s : set } :
(λ (x : ), real.sinh (f x)) s x

@[simp]
theorem differentiable_at.sinh {f : } {x : } :
(λ (x : ), real.sinh (f x)) x

theorem differentiable_on.sinh {f : } {s : set } :
(λ (x : ), real.sinh (f x)) s

@[simp]
theorem differentiable.sinh {f : } :
(λ (x : ), real.sinh (f x))

theorem deriv_within_sinh {f : } {x : } {s : set } :
deriv_within (λ (x : ), real.sinh (f x)) s x = (real.cosh (f x)) * s x

@[simp]
theorem deriv_sinh {f : } {x : } :
deriv (λ (x : ), real.sinh (f x)) x = (real.cosh (f x)) * 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  :
= -1

@[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 : ) :
real.sin (x + π) =

theorem real.sin_add_two_pi (x : ) :
real.sin (x + 2 * π) =

theorem real.cos_add_two_pi (x : ) :
real.cos (x + 2 * π) =

theorem real.sin_pi_sub (x : ) :
real.sin (π - x) =

theorem real.cos_add_pi (x : ) :
real.cos (x + π) =

theorem real.cos_pi_sub (x : ) :
real.cos (π - x) =

theorem real.sin_pos_of_pos_of_lt_pi {x : } :
0 < xx < π0 <

theorem real.sin_nonneg_of_nonneg_of_le_pi {x : } :
0 xx π0

theorem real.sin_neg_of_neg_of_neg_pi_lt {x : } :
x < 0-π < x < 0

theorem real.sin_nonpos_of_nonnpos_of_neg_pi_le {x : } :
x 0-π x 0

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

theorem real.sin_add_pi_div_two (x : ) :
real.sin (x + π / 2) =

theorem real.sin_sub_pi_div_two (x : ) :
real.sin (x - π / 2) =

theorem real.sin_pi_div_two_sub (x : ) :
real.sin (π / 2 - x) =

theorem real.cos_add_pi_div_two (x : ) :
real.cos (x + π / 2) =

theorem real.cos_sub_pi_div_two (x : ) :
real.cos (x - π / 2) =

theorem real.cos_pi_div_two_sub (x : ) :
real.cos (π / 2 - x) =

theorem real.cos_pos_of_mem_Ioo {x : } :
-(π / 2) < xx < π / 20 <

theorem real.cos_nonneg_of_mem_Icc {x : } :
-(π / 2) xx π / 20

theorem real.cos_neg_of_pi_div_two_lt_of_lt {x : } :
π / 2 < xx < π + π / 2 < 0

theorem real.cos_nonpos_of_pi_div_two_le_of_le {x : } :
π / 2 xx π + π / 2 0

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 : } :
-π < xx < π(real.sin x = 0 x = 0)

theorem real.sin_eq_zero_iff {x : } :
= 0 ∃ (n : ), (n) * π = x

theorem real.sin_eq_zero_iff_cos_eq {x : } :
= 0 = 1 = -1

theorem real.cos_eq_one_iff (x : ) :
= 1 ∃ (n : ), (n) * 2 * π = x

theorem real.cos_eq_one_iff_of_lt_of_lt {x : } :
-2 * π < xx < 2 * π(real.cos x = 1 x = 0)

theorem real.cos_lt_cos_of_nonneg_of_le_pi_div_two {x y : } :
0 xy π / 2x < y

theorem real.cos_lt_cos_of_nonneg_of_le_pi {x y : } :
0 xy πx < y

theorem real.cos_le_cos_of_nonneg_of_le_pi {x y : } :
0 xy πx y

theorem real.sin_lt_sin_of_le_of_le_pi_div_two {x y : } :
-(π / 2) xy π / 2x < y

theorem real.sin_le_sin_of_le_of_le_pi_div_two {x y : } :
-(π / 2) xy π / 2x y

theorem real.sin_inj_of_le_of_le_pi_div_two {x y : } :
-(π / 2) xx π / 2-(π / 2) yy π / 2x = y

theorem real.cos_inj_of_nonneg_of_le_pi {x y : } :
0 xx π0 yy πx = y

theorem real.exists_sin_eq  :
set.Icc (-1) 1 real.sin '' set.Icc (-(π / 2)) (π / 2)

theorem real.exists_cos_eq  :
set.Icc (-1) 1

theorem real.range_cos  :
= set.Icc (-1) 1

theorem real.range_sin  :
= set.Icc (-1) 1

theorem real.sin_lt {x : } :
0 < x < x

theorem real.sin_gt_sub_cube {x : } :
0 < xx 1x - x ^ 3 / 4 <

@[simp]

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
theorem real.sqrt_two_add_series_nonneg {x : } (h : 0 x) (n : ) :
0

theorem real.sqrt_two_add_series_monotone_left {x y : } (h : x y) (n : ) :

@[simp]
theorem real.cos_pi_over_two_pow (n : ) :
real.cos (π / 2 ^ (n + 1)) = / 2

theorem real.sin_square_pi_over_two_pow (n : ) :
real.sin (π / 2 ^ (n + 1)) ^ 2 = 1 - / 2) ^ 2

theorem real.sin_square_pi_over_two_pow_succ (n : ) :
real.sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - / 4

@[simp]
theorem real.sin_pi_over_two_pow_succ (n : ) :
real.sin (π / 2 ^ (n + 2)) = real.sqrt (2 - / 2

@[simp]
theorem real.cos_pi_div_four  :
real.cos (π / 4) = / 2

@[simp]
theorem real.sin_pi_div_four  :
real.sin (π / 4) = / 2

@[simp]
theorem real.cos_pi_div_eight  :

@[simp]
theorem real.sin_pi_div_eight  :

@[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  :
real.cos (π / 6) = / 2

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]
theorem real.sin_pi_div_three  :
real.sin (π / 3) = / 2

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

def real.angle  :
Type

The type of angles

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

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 {θ ψ : } :
θ = ψ

def real.arcsin  :

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

Equations
theorem real.sin_arcsin {x : } :
-1 xx 1 = x

theorem real.arcsin_sin {x : } :
-(π / 2) xx π / 2(real.sin x).arcsin = x

theorem real.arcsin_inj {x y : } :
-1 xx 1-1 yy 1x.arcsin = y.arcsinx = y

@[simp]
theorem real.arcsin_zero  :
0.arcsin = 0

@[simp]
theorem real.arcsin_one  :
1.arcsin = π / 2

@[simp]
theorem real.arcsin_neg (x : ) :

@[simp]
theorem real.arcsin_neg_one  :
(-1).arcsin = -(π / 2)

theorem real.arcsin_nonneg {x : } :
0 x0 x.arcsin

theorem real.arcsin_eq_zero_iff {x : } :
-1 xx 1(x.arcsin = 0 x = 0)

theorem real.arcsin_pos {x : } :
0 < xx 10 < x.arcsin

theorem real.arcsin_nonpos {x : } :
x 0x.arcsin 0

def real.arccos  :

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.arccos_le_pi (x : ) :

theorem real.arccos_nonneg (x : ) :

theorem real.cos_arccos {x : } :
-1 xx 1 = x

theorem real.arccos_cos {x : } :
0 xx π(real.cos x).arccos = x

theorem real.arccos_inj {x y : } :
-1 xx 1-1 yy 1x.arccos = y.arccosx = y

@[simp]
theorem real.arccos_zero  :
0.arccos = π / 2

@[simp]
theorem real.arccos_one  :
1.arccos = 0

@[simp]
theorem real.arccos_neg_one  :
(-1).arccos = π

theorem real.arccos_neg (x : ) :

theorem real.cos_arcsin_nonneg (x : ) :
0

theorem real.cos_arcsin {x : } :
-1 xx 1 = real.sqrt (1 - x ^ 2)

theorem real.sin_arccos {x : } :
-1 xx 1 = real.sqrt (1 - x ^ 2)

theorem real.abs_div_sqrt_one_add_lt (x : ) :
abs (x / real.sqrt (1 + x ^ 2)) < 1

theorem real.div_sqrt_one_add_lt_one (x : ) :
x / real.sqrt (1 + x ^ 2) < 1

theorem real.neg_one_lt_div_sqrt_one_add (x : ) :
-1 < x / real.sqrt (1 + x ^ 2)

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

theorem real.tan_pos_of_pos_of_lt_pi_div_two {x : } :
0 < xx < π / 20 <

theorem real.tan_nonneg_of_nonneg_of_le_pi_div_two {x : } :
0 xx π / 20

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

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

theorem real.tan_lt_tan_of_nonneg_of_lt_pi_div_two {x y : } :
0 xy < π / 2x < y

theorem real.tan_lt_tan_of_lt_of_lt_pi_div_two {x y : } :
-(π / 2) < xy < π / 2x < y

theorem real.tan_inj_of_lt_of_lt_pi_div_two {x y : } :
-(π / 2) < xx < π / 2-(π / 2) < yy < π / 2x = y

def real.arctan  :

Inverse of the `tan` function, returns values in the range `-π / 2 < arctan x` and `arctan x < π / 2`

Equations
theorem real.sin_arctan (x : ) :
= x / real.sqrt (1 + x ^ 2)

theorem real.cos_arctan (x : ) :
= 1 / real.sqrt (1 + x ^ 2)

theorem real.tan_arctan (x : ) :
= x

theorem real.arctan_mem_Ioo (x : ) :
x.arctan set.Ioo (-(π / 2)) (π / 2)

theorem real.arctan_tan {x : } :
-(π / 2) < xx < π / 2(real.tan x).arctan = x

@[simp]
theorem real.arctan_zero  :
0.arctan = 0

@[simp]
theorem real.arctan_one  :
1.arctan = π / 4

@[simp]
theorem real.arctan_neg (x : ) :

def complex.arg  :

`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_sub_pi_of_im_neg_of_re_neg {x : } :
x.re < 0x.im < 0x.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.sin_arg (x : ) :
= x.im /

theorem complex.cos_arg {x : } :
x 0 = x.re /

theorem complex.tan_arg {x : } :
= x.im / x.re

theorem complex.arg_cos_add_sin_mul_I {x : } :
-π < xx π + .arg = x

theorem complex.arg_eq_arg_iff {x y : } :
x 0y 0(x.arg = y.arg ((complex.abs y) / (complex.abs x)) * x = y)

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

theorem complex.ext_abs_arg {x y : } :
x.arg = y.argx = y

theorem complex.arg_of_real_of_nonneg {x : } :
0 xx.arg = 0

theorem complex.arg_of_real_of_neg {x : } :
x < 0x.arg = π

def complex.log  :

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

Equations
theorem complex.log_re (x : ) :
x.log.re =

theorem complex.log_im (x : ) :
x.log.im = x.arg

theorem complex.exp_log {x : } :
x 0 = x

theorem complex.range_exp  :
= {x : | x 0}

theorem complex.exp_inj_of_neg_pi_lt_of_le_pi {x y : } :
-π < x.imx.im π-π < y.imy.im πx = y

theorem complex.log_exp {x : } :
-π < x.imx.im π(complex.exp x).log = x

theorem complex.of_real_log {x : } :
0 x(real.log x) = x.log

@[simp]
theorem complex.log_zero  :
0.log = 0

@[simp]
theorem complex.log_one  :
1.log = 0

theorem complex.log_neg_one  :
(-1).log =

theorem complex.exists_pow_nat_eq (x : ) {n : } :
0 < n(∃ (z : ), z ^ n = x)

theorem complex.exists_eq_mul_self (x : ) :
∃ (z : ), x = z * z

theorem complex.exp_eq_one_iff {x : } :
= 1 ∃ (n : ), x = (n) * (2 * π) * complex.I

theorem complex.exp_eq_exp_iff_exists_int {x y : } :
∃ (n : ), x = y + (n) * (2 * π) * complex.I

@[simp]

@[simp]

@[simp]
theorem complex.sin_pi  :

@[simp]
theorem complex.cos_pi  :

@[simp]
theorem complex.sin_two_pi  :

@[simp]
theorem complex.cos_two_pi  :

theorem complex.cos_eq_zero_iff {θ : } :
= 0 ∃ (k : ), θ = (2 * k + 1) * π / 2

theorem complex.cos_ne_zero_iff {θ : } :
0 ∀ (k : ), θ (2 * k + 1) * π / 2

theorem complex.sin_eq_zero_iff {θ : } :
= 0 ∃ (k : ), θ = (k) * π

theorem complex.sin_ne_zero_iff {θ : } :
0 ∀ (k : ), θ (k) * π

theorem complex.cos_eq_cos_iff {x y : } :
∃ (k : ), y = (2 * k) * π + x y = (2 * k) * π - x

theorem complex.sin_eq_sin_iff {x y : } :
∃ (k : ), y = (2 * k) * π + x y = (2 * k + 1) * π - x

theorem complex.has_deriv_at_tan {x : } :
(∀ (k : ), x (2 * k + 1) * π / 2) (1 / ^ 2) x

theorem complex.differentiable_at_tan {x : } :
(∀ (k : ), x (2 * k + 1) * π / 2)

@[simp]
theorem complex.deriv_tan {x : } :
(∀ (k : ), x (2 * k + 1) * π / 2) = 1 / ^ 2

theorem complex.continuous_on_tan  :
{x : | 0}

theorem complex.continuous_tan  :
continuous (λ (x : {x : | 0}),

@[simp]

@[simp]

theorem chebyshev₁_complex_cos (θ : ) (n : ) :
= complex.cos ((n) * θ)

the `n`-th Chebyshev polynomial evaluates on `cos θ` to the value `cos (n * θ)`.

theorem cos_nat_mul (n : ) (θ : ) :
complex.cos ((n) * θ) =

`cos (n * θ)` is equal to the `n`-th Chebyshev polynomial evaluated on `cos θ`.

theorem real.cos_eq_zero_iff {θ : } :
= 0 ∃ (k : ), θ = (2 * k + 1) * π / 2

theorem real.cos_ne_zero_iff {θ : } :
0 ∀ (k : ), θ (2 * k + 1) * π / 2

theorem real.cos_eq_cos_iff {x y : } :
∃ (k : ), y = (2 * k) * π + x y = (2 * k) * π - x

theorem real.sin_eq_sin_iff {x y : } :
∃ (k : ), y = (2 * k) * π + x y = (2 * k + 1) * π - x

theorem real.has_deriv_at_tan {x : } :
(∀ (k : ), x (2 * k + 1) * π / 2) (1 / ^ 2) x

theorem real.differentiable_at_tan {x : } :
(∀ (k : ), x (2 * k + 1) * π / 2)

@[simp]
theorem real.deriv_tan {x : } :
(∀ (k : ), x (2 * k + 1) * π / 2) = 1 / ^ 2

theorem real.continuous_tan  :
continuous (λ (x : {x : | 0}),

theorem real.continuous_on_tan  :
{x : | 0}

theorem real.has_deriv_at_tan_of_mem_Ioo {x : } :
x set.Ioo (-(π / 2)) (π / 2) (1 / ^ 2) x

theorem real.differentiable_at_tan_of_mem_Ioo {x : } :
x set.Ioo (-(π / 2)) (π / 2)

theorem real.deriv_tan_of_mem_Ioo {x : } :
x set.Ioo (-(π / 2)) (π / 2) = 1 / ^ 2

theorem real.continuous_on_tan_Ioo  :
(set.Ioo (-(π / 2)) (π / 2))

### Continuity and differentiability of arctan

The continuity of `arctan` is difficult to prove due to `arctan` being (indirectly) defined naively via `classical.some`. The proof therefore uses the general theorem that monotone functions are homeomorphisms: `homeomorph_of_strict_mono_continuous_Ioo`. We first prove that `tan` (restricted) is a homeomorphism whose inverse is definitionally equal to `arctan`. The fact that `arctan` is continuous is then derived from the fact that it is equal to a homeomorphism, and its differentiability is in turn derived from its continuity using `has_deriv_at.of_local_left_inverse`.

The function `tan`, restricted to the open interval (-π/2, π/2), is a homeomorphism. The inverse function of that homeomorphism is definitionally equal to `arctan` via `homeomorph.change_inv`.

Equations
theorem real.has_deriv_at_arctan (x : ) :
(1 / (1 + x ^ 2)) x

@[simp]
theorem real.deriv_arctan  :
= λ (x : ), 1 / (1 + x ^ 2)

Register lemmas for the derivatives of the composition of `real.arctan` with a differentiable function, for standalone use and use with `simp`.

theorem has_deriv_at.arctan {f : } {f' x : } :
f' xhas_deriv_at (λ (x : ), (f x).arctan) ((1 / (1 + f x ^ 2)) * f') x

theorem has_deriv_within_at.arctan {f : } {f' x : } {s : set } :
s xhas_deriv_within_at (λ (x : ), (f x).arctan) ((1 / (1 + f x ^ 2)) * f') s x

theorem differentiable_within_at.arctan {f : } {x : } {s : set } :
(λ (x : ), (f x).arctan) s x

@[simp]
theorem differentiable_at.arctan {f : } {x : } :
(λ (x : ), (f x).arctan) x

theorem differentiable_on.arctan {f : } {s : set } :
(λ (x : ), (f x).arctan) s

@[simp]
theorem differentiable.arctan {f : } :
(λ (x : ), (f x).arctan)

theorem deriv_within_arctan {f : } {x : } {s : set } :
deriv_within (λ (x : ), (f x).arctan) s x = (1 / (1 + f x ^ 2)) * s x

@[simp]
theorem deriv_arctan {f : } {x : } :
deriv (λ (x : ), (f x).arctan) x = (1 / (1 + f x ^ 2)) * x