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.

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 fmeasurable (λ (x : ), complex.cos (f x))

theorem has_deriv_at.ccos {f : } {f' x : } :
has_deriv_at f 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 } :
has_deriv_within_at f f' 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 } :

@[simp]
theorem differentiable_at.ccos {f : } {x : } :

theorem differentiable_on.ccos {f : } {s : set } :

@[simp]
theorem differentiable.ccos {f : } :

theorem deriv_within_ccos {f : } {x : } {s : set } :

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

complex.sin

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

theorem has_deriv_at.csin {f : } {f' x : } :
has_deriv_at f 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 } :
has_deriv_within_at f f' 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 } :

@[simp]
theorem differentiable_at.csin {f : } {x : } :

theorem differentiable_on.csin {f : } {s : set } :

@[simp]
theorem differentiable.csin {f : } :

theorem deriv_within_csin {f : } {x : } {s : set } :

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

complex.cosh

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

theorem has_deriv_at.ccosh {f : } {f' x : } :
has_deriv_at f 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 } :
has_deriv_within_at f f' s xhas_deriv_within_at (λ (x : ), complex.cosh (f x)) ((complex.sinh (f x)) * f') s x

@[simp]
theorem differentiable_at.ccosh {f : } {x : } :

theorem differentiable_on.ccosh {f : } {s : set } :

@[simp]
theorem differentiable.ccosh {f : } :

theorem deriv_within_ccosh {f : } {x : } {s : set } :

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

complex.sinh

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

theorem has_deriv_at.csinh {f : } {f' x : } :
has_deriv_at f 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 } :
has_deriv_within_at f f' s xhas_deriv_within_at (λ (x : ), complex.sinh (f x)) ((complex.cosh (f x)) * f') s x

@[simp]
theorem differentiable_at.csinh {f : } {x : } :

theorem differentiable_on.csinh {f : } {s : set } :

@[simp]
theorem differentiable.csinh {f : } :

theorem deriv_within_csinh {f : } {x : } {s : set } :

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

@[simp]
theorem real.deriv_cos'  :

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 fmeasurable (λ (x : ), real.cos (f x))

theorem has_deriv_at.cos {f : } {f' x : } :
has_deriv_at f 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 } :
has_deriv_within_at f f' 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 } :

@[simp]
theorem differentiable_at.cos {f : } {x : } :

theorem differentiable_on.cos {f : } {s : set } :

@[simp]
theorem differentiable.cos {f : } :

theorem deriv_within_cos {f : } {x : } {s : set } :

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

real.sin

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

theorem has_deriv_at.sin {f : } {f' x : } :
has_deriv_at f 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 } :
has_deriv_within_at f f' 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 } :

@[simp]
theorem differentiable_at.sin {f : } {x : } :

theorem differentiable_on.sin {f : } {s : set } :

@[simp]
theorem differentiable.sin {f : } :

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

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

real.cosh

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

theorem has_deriv_at.cosh {f : } {f' x : } :
has_deriv_at f 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 } :
has_deriv_within_at f f' 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 } :

@[simp]
theorem differentiable_at.cosh {f : } {x : } :

theorem differentiable_on.cosh {f : } {s : set } :

@[simp]
theorem differentiable.cosh {f : } :

theorem deriv_within_cosh {f : } {x : } {s : set } :

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

real.sinh

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

theorem has_deriv_at.sinh {f : } {f' x : } :
has_deriv_at f 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 } :
has_deriv_within_at f f' 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 } :

@[simp]
theorem differentiable_at.sinh {f : } {x : } :

theorem differentiable_on.sinh {f : } {s : set } :

@[simp]
theorem differentiable.sinh {f : } :

theorem deriv_within_sinh {f : } {x : } {s : set } :

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

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

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

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

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

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

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

theorem real.cos_nonpos_of_pi_div_two_le_of_le {x : } :
π / 2 xx π + π / 2real.cos x 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 : } :
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 : } :
-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 < yreal.cos y < real.cos x

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

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

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

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

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

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

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

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

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

@[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 : ) :

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

theorem real.sin_square_pi_over_two_pow (n : ) :
real.sin (π / 2 ^ (n + 1)) ^ 2 = 1 - (0.sqrt_two_add_series 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 {θ ψ : } :
real.cos θ = real.cos ψreal.sin θ = real.sin ψθ = ψ

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 1real.sin x.arcsin = 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 1real.cos x.arccos = 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 {x : } :
-1 xx 1real.cos x.arcsin = real.sqrt (1 - x ^ 2)

theorem real.sin_arccos {x : } :
-1 xx 1real.sin x.arccos = 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 < real.tan x

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

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

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

theorem real.tan_inj_of_lt_of_lt_pi_div_two {x y : } :
-(π / 2) < xx < π / 2-(π / 2) < yy < π / 2real.tan x = real.tan yx = 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 : ) :
real.sin x.arctan = x / real.sqrt (1 + x ^ 2)

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

theorem real.tan_arctan (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.cos_arg {x : } :
x 0real.cos x.arg = x.re / complex.abs x

theorem complex.tan_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 : } :
complex.abs x = complex.abs yx.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 : ) :

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

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

theorem complex.exp_inj_of_neg_pi_lt_of_le_pi {x y : } :
-π < x.imx.im π-π < y.imy.im πcomplex.exp x = complex.exp yx = 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.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 : } :
complex.exp x = 1 ∃ (n : ), x = (n) * (2 * π) * complex.I

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

@[simp]

@[simp]

@[simp]

@[simp]

@[simp]
theorem complex.sin_two_pi  :

@[simp]
theorem complex.cos_two_pi  :

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem real.deriv_tan_of_mem_Ioo {x : } :
x set.Ioo (-(π / 2)) (π / 2)deriv real.tan x = 1 / real.cos x ^ 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 : ) :
has_deriv_at real.arctan (1 / (1 + x ^ 2)) x

@[simp]
theorem real.deriv_arctan  :
deriv real.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 : } :
has_deriv_at f 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 } :
has_deriv_within_at f f' 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 } :

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

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

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

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

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