mathlib documentation

analysis.special_functions.trigonometric.arctan

The arctan function. #

Inequalities, derivatives, and real.tan as a local_homeomorph between (-(π / 2), π / 2) and the whole line.

theorem real.tan_add {x y : } (h : ((∀ (k : ), x (2 * k + 1) * π / 2) ∀ (l : ), y (2 * l + 1) * π / 2) (∃ (k : ), x = (2 * k + 1) * π / 2) ∃ (l : ), y = (2 * l + 1) * π / 2) :
real.tan (x + y) = (real.tan x + real.tan y) / (1 - (real.tan x) * real.tan y)
theorem real.tan_add' {x y : } (h : (∀ (k : ), x (2 * k + 1) * π / 2) ∀ (l : ), y (2 * l + 1) * π / 2) :
real.tan (x + y) = (real.tan x + real.tan y) / (1 - (real.tan x) * real.tan y)
theorem real.tan_two_mul {x : } :
real.tan (2 * x) = 2 * real.tan x / (1 - real.tan x ^ 2)
theorem real.tan_ne_zero_iff {θ : } :
real.tan θ 0 ∀ (k : ), θ (k) * π / 2
theorem real.tan_eq_zero_iff {θ : } :
real.tan θ = 0 ∃ (k : ), θ = (k) * π / 2
theorem real.tan_int_mul_pi_div_two (n : ) :
real.tan ((n) * π / 2) = 0
theorem real.has_deriv_at_tan {x : } (h : real.cos x 0) :
theorem real.tendsto_abs_tan_at_top (k : ) :
filter.tendsto (λ (x : ), |real.tan x|) (𝓝[{(2 * k + 1) * π / 2}] ((2 * k + 1) * π / 2)) filter.at_top
@[simp]
theorem real.deriv_tan (x : ) :
theorem real.continuous_tan  :
continuous (λ (x : {x : | real.cos x 0}), real.tan x)
theorem real.has_deriv_at_tan_of_mem_Ioo {x : } (h : x set.Ioo (-(π / 2)) (π / 2)) :
def real.arctan (x : ) :

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

Equations
@[simp]
theorem real.tan_arctan (x : ) :
theorem real.arctan_mem_Ioo (x : ) :
theorem real.arctan_tan {x : } (hx₁ : -(π / 2) < x) (hx₂ : x < π / 2) :
theorem real.cos_sq_arctan (x : ) :
real.cos (real.arctan x) ^ 2 = 1 / (1 + x ^ 2)
theorem real.sin_arctan (x : ) :
theorem real.cos_arctan (x : ) :
theorem real.arcsin_eq_arctan {x : } (h : x set.Ioo (-1) 1) :
@[simp]
theorem real.arctan_zero  :
theorem real.arctan_eq_of_tan_eq {x y : } (h : real.tan x = y) (hx : x set.Ioo (-(π / 2)) (π / 2)) :
@[simp]
theorem real.arctan_one  :
@[simp]
theorem real.arctan_neg (x : ) :

real.tan as a local_homeomorph between (-(π / 2), π / 2) and the whole line.

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)

Lemmas for derivatives of the composition of real.arctan with a differentiable function #

In this section we register lemmas for the derivatives of the composition of real.arctan with a differentiable function, for standalone use and use with simp.

theorem has_strict_deriv_at.arctan {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), real.arctan (f x)) ((1 / (1 + f x ^ 2)) * f') x
theorem has_deriv_at.arctan {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), real.arctan (f x)) ((1 / (1 + f x ^ 2)) * f') x
theorem has_deriv_within_at.arctan {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), real.arctan (f x)) ((1 / (1 + f x ^ 2)) * f') s x
theorem deriv_within_arctan {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.arctan (f x)) s x = (1 / (1 + f x ^ 2)) * deriv_within f s x
@[simp]
theorem deriv_arctan {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.arctan (f x)) x = (1 / (1 + f x ^ 2)) * deriv f x
theorem has_strict_fderiv_at.arctan {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.arctan (f x)) ((1 / (1 + f x ^ 2)) f') x
theorem has_fderiv_at.arctan {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.arctan (f x)) ((1 / (1 + f x ^ 2)) f') x
theorem has_fderiv_within_at.arctan {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.arctan (f x)) ((1 / (1 + f x ^ 2)) f') s x
theorem fderiv_within_arctan {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.arctan (f x)) s x = (1 / (1 + f x ^ 2)) fderiv_within f s x
@[simp]
theorem fderiv_arctan {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.arctan (f x)) x = (1 / (1 + f x ^ 2)) fderiv f x
theorem differentiable_within_at.arctan {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.arctan (f x)) s x
@[simp]
theorem differentiable_at.arctan {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.arctan (f x)) x
theorem differentiable_on.arctan {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.arctan (f x)) s
@[simp]
theorem differentiable.arctan {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), real.arctan (f x))
theorem times_cont_diff_at.arctan {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (h : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), real.arctan (f x)) x
theorem times_cont_diff.arctan {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.arctan (f x))
theorem times_cont_diff_within_at.arctan {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (h : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), real.arctan (f x)) s x
theorem times_cont_diff_on.arctan {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (h : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), real.arctan (f x)) s