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) * real.pi / 2) ∀ (l : ), y (2 * l + 1) * real.pi / 2) (∃ (k : ), x = (2 * k + 1) * real.pi / 2) ∃ (l : ), y = (2 * l + 1) * real.pi / 2) :
theorem real.tan_add' {x y : } (h : (∀ (k : ), x (2 * k + 1) * real.pi / 2) ∀ (l : ), y (2 * l + 1) * real.pi / 2) :
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 * real.pi / 2
theorem real.tan_eq_zero_iff {θ : } :
real.tan θ = 0 ∃ (k : ), θ = k * real.pi / 2
@[continuity]
theorem real.continuous_tan  :
continuous (λ (x : {x : | real.cos x 0}), real.tan x)
noncomputable 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_tan {x : } (hx₁ : -(real.pi / 2) < x) (hx₂ : x < real.pi / 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 (-(real.pi / 2)) (real.pi / 2)) :
@[simp]
@[simp]
theorem real.arctan_neg (x : ) :

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

Equations