mathlib3 documentation

analysis.special_functions.trigonometric.arctan

The arctan function. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
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) :
real.tan (x + y) = (real.tan x + real.tan y) / (1 - real.tan x * real.tan y)
source
theorem real.tan_add' {x y : ℝ} (h : (∀ (k : ℤ), x ≠ (2 * ↑k + 1) * real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * real.pi / 2) :
real.tan (x + y) = (real.tan x + real.tan y) / (1 - real.tan x * real.tan y)
source
theorem real.tan_two_mul {x : ℝ} :
real.tan (2 * x) = 2 * real.tan x / (1 - real.tan x ^ 2)
source
theorem real.tan_ne_zero_iff {θ : ℝ} :
real.tan θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * real.pi / 2
source
theorem real.tan_eq_zero_iff {θ : ℝ} :
real.tan θ = 0 ↔ ∃ (k : ℤ), θ = ↑k * real.pi / 2
source
theorem real.tan_int_mul_pi_div_two (n : ℤ) :
real.tan (↑n * real.pi / 2) = 0
source
theorem real.continuous_on_tan  :
continuous_on real.tan {x : ℝ | real.cos x ≠ 0}
source
@[continuity]
theorem real.continuous_tan  :
continuous (λ (x : ↥{x : ℝ | real.cos x ≠ 0}), real.tan ↑x)
source
theorem real.continuous_on_tan_Ioo  :
continuous_on real.tan (set.Ioo (-(real.pi / 2)) (real.pi / 2))
source
theorem real.surj_on_tan  :
set.surj_on real.tan (set.Ioo (-(real.pi / 2)) (real.pi / 2)) set.univ
source
theorem real.tan_surjective  :
function.surjective real.tan
source
theorem real.image_tan_Ioo  :
real.tan '' set.Ioo (-(real.pi / 2)) (real.pi / 2) = set.univ
source
noncomputable def real.tan_order_iso  :
↥(set.Ioo (-(real.pi / 2)) (real.pi / 2)) ≃o ℝ

real.tan as an order_iso between (-(π / 2), π / 2) and ℝ.

Equations
source
noncomputable def real.arctan (x : ℝ) :
ℝ

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

Equations
source
@[simp]
theorem real.tan_arctan (x : ℝ) :
real.tan (real.arctan x) = x
source
theorem real.arctan_mem_Ioo (x : ℝ) :
real.arctan x ∈ set.Ioo (-(real.pi / 2)) (real.pi / 2)
source
@[simp]
theorem real.range_arctan  :
set.range real.arctan = set.Ioo (-(real.pi / 2)) (real.pi / 2)
source
theorem real.arctan_tan {x : ℝ} (hx₁ : -(real.pi / 2) < x) (hx₂ : x < real.pi / 2) :
real.arctan (real.tan x) = x
source
theorem real.cos_arctan_pos (x : ℝ) :
0 < real.cos (real.arctan x)
source
theorem real.cos_sq_arctan (x : ℝ) :
real.cos (real.arctan x) ^ 2 = 1 / (1 + x ^ 2)
source
theorem real.sin_arctan (x : ℝ) :
real.sin (real.arctan x) = x / √ (1 + x ^ 2)
source
theorem real.cos_arctan (x : ℝ) :
real.cos (real.arctan x) = 1 / √ (1 + x ^ 2)
source
theorem real.arctan_lt_pi_div_two (x : ℝ) :
real.arctan x < real.pi / 2
source
theorem real.neg_pi_div_two_lt_arctan (x : ℝ) :
-(real.pi / 2) < real.arctan x
source
theorem real.arctan_eq_arcsin (x : ℝ) :
real.arctan x = real.arcsin (x / √ (1 + x ^ 2))
source
theorem real.arcsin_eq_arctan {x : ℝ} (h : x ∈ set.Ioo (-1) 1) :
real.arcsin x = real.arctan (x / √ (1 - x ^ 2))
source
@[simp]
theorem real.arctan_zero  :
real.arctan 0 = 0
source
theorem real.arctan_eq_of_tan_eq {x y : ℝ} (h : real.tan x = y) (hx : x ∈ set.Ioo (-(real.pi / 2)) (real.pi / 2)) :
real.arctan y = x
source
@[simp]
theorem real.arctan_one  :
real.arctan 1 = real.pi / 4
source
@[simp]
theorem real.arctan_neg (x : ℝ) :
real.arctan (-x) = -real.arctan x
source
theorem real.arctan_eq_arccos {x : ℝ} (h : 0 ≤ x) :
real.arctan x = real.arccos (√ (1 + x ^ 2))⁻¹
source
theorem real.arccos_eq_arctan {x : ℝ} (h : 0 < x) :
real.arccos x = real.arctan (√ (1 - x ^ 2) / x)
source
@[continuity]
theorem real.continuous_arctan  :
continuous real.arctan
source
theorem real.continuous_at_arctan {x : ℝ} :
continuous_at real.arctan x
source
noncomputable def real.tan_local_homeomorph  :
local_homeomorph ℝ ℝ

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

Equations
source
@[simp]
theorem real.coe_tan_local_homeomorph  :
⇑real.tan_local_homeomorph = real.tan
source
@[simp]
theorem real.coe_tan_local_homeomorph_symm  :
⇑(real.tan_local_homeomorph.symm) = real.arctan