mathlib documentation

analysis.special_functions.trigonometric.inverse

Inverse trigonometric functions. #

See also analysis.special_functions.trigonometric.arctan for the inverse tan function. (This is delayed as it is easier to set up after developing complex trigonometric functions.)

Basic inequalities and derivatives.

def real.arcsin  :

Inverse of the sin function, returns values in the range -π / 2 ≤ arcsin x ≤ π / 2. It defaults to -π / 2 on (-∞, -1) and to π / 2 to (1, ∞).

Equations
theorem real.arcsin_mem_Icc (x : ) :
@[simp]
theorem real.sin_arcsin' {x : } (hx : x set.Icc (-1) 1) :
theorem real.sin_arcsin {x : } (hx₁ : -1 x) (hx₂ : x 1) :
theorem real.arcsin_sin' {x : } (hx : x set.Icc (-(π / 2)) (π / 2)) :
theorem real.arcsin_sin {x : } (hx₁ : -(π / 2) x) (hx₂ : x π / 2) :
theorem real.arcsin_inj {x y : } (hx₁ : -1 x) (hx₂ : x 1) (hy₁ : -1 y) (hy₂ : y 1) :
theorem real.arcsin_eq_of_sin_eq {x y : } (h₁ : real.sin x = y) (h₂ : x set.Icc (-(π / 2)) (π / 2)) :
@[simp]
theorem real.arcsin_zero  :
@[simp]
theorem real.arcsin_one  :
theorem real.arcsin_of_one_le {x : } (hx : 1 x) :
theorem real.arcsin_neg_one  :
real.arcsin (-1) = -(π / 2)
theorem real.arcsin_of_le_neg_one {x : } (hx : x -1) :
@[simp]
theorem real.arcsin_neg (x : ) :
theorem real.arcsin_le_iff_le_sin {x y : } (hx : x set.Icc (-1) 1) (hy : y set.Icc (-(π / 2)) (π / 2)) :
theorem real.arcsin_le_iff_le_sin' {x y : } (hy : y set.Ico (-(π / 2)) (π / 2)) :
theorem real.le_arcsin_iff_sin_le {x y : } (hx : x set.Icc (-(π / 2)) (π / 2)) (hy : y set.Icc (-1) 1) :
theorem real.le_arcsin_iff_sin_le' {x y : } (hx : x set.Ioc (-(π / 2)) (π / 2)) :
theorem real.arcsin_lt_iff_lt_sin {x y : } (hx : x set.Icc (-1) 1) (hy : y set.Icc (-(π / 2)) (π / 2)) :
theorem real.arcsin_lt_iff_lt_sin' {x y : } (hy : y set.Ioc (-(π / 2)) (π / 2)) :
theorem real.lt_arcsin_iff_sin_lt {x y : } (hx : x set.Icc (-(π / 2)) (π / 2)) (hy : y set.Icc (-1) 1) :
theorem real.lt_arcsin_iff_sin_lt' {x y : } (hx : x set.Ico (-(π / 2)) (π / 2)) :
theorem real.arcsin_eq_iff_eq_sin {x y : } (hy : y set.Ioo (-(π / 2)) (π / 2)) :
@[simp]
theorem real.arcsin_nonneg {x : } :
@[simp]
theorem real.arcsin_nonpos {x : } :
@[simp]
theorem real.arcsin_eq_zero_iff {x : } :
real.arcsin x = 0 x = 0
@[simp]
theorem real.zero_eq_arcsin_iff {x : } :
0 = real.arcsin x x = 0
@[simp]
theorem real.arcsin_pos {x : } :
0 < real.arcsin x 0 < x
@[simp]
theorem real.arcsin_lt_zero {x : } :
real.arcsin x < 0 x < 0
@[simp]
theorem real.arcsin_lt_pi_div_two {x : } :
real.arcsin x < π / 2 x < 1
@[simp]
theorem real.neg_pi_div_two_lt_arcsin {x : } :
-(π / 2) < real.arcsin x -1 < x
@[simp]
theorem real.arcsin_eq_pi_div_two {x : } :
@[simp]
theorem real.pi_div_two_eq_arcsin {x : } :
@[simp]
theorem real.pi_div_two_le_arcsin {x : } :
@[simp]
theorem real.arcsin_eq_neg_pi_div_two {x : } :
real.arcsin x = -(π / 2) x -1
@[simp]
theorem real.neg_pi_div_two_eq_arcsin {x : } :
-(π / 2) = real.arcsin x x -1
@[simp]
theorem real.maps_to_sin_Ioo  :
set.maps_to real.sin (set.Ioo (-(π / 2)) (π / 2)) (set.Ioo (-1) 1)
@[simp]

real.sin as a local_homeomorph between (-π / 2, π / 2) and (-1, 1).

Equations
theorem real.cos_arcsin {x : } (hx₁ : -1 x) (hx₂ : x 1) :
theorem real.has_strict_deriv_at_arcsin {x : } (h₁ : x -1) (h₂ : x 1) :
theorem real.has_deriv_at_arcsin {x : } (h₁ : x -1) (h₂ : x 1) :
theorem real.times_cont_diff_at_arcsin {x : } (h₁ : x -1) (h₂ : x 1) {n : with_top } :
@[simp]
theorem real.deriv_arcsin  :
deriv real.arcsin = λ (x : ), 1 / real.sqrt (1 - x ^ 2)
def real.arccos (x : ) :

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.cos_arccos {x : } (hx₁ : -1 x) (hx₂ : x 1) :
theorem real.arccos_cos {x : } (hx₁ : 0 x) (hx₂ : x π) :
theorem real.arccos_inj {x y : } (hx₁ : -1 x) (hx₂ : x 1) (hy₁ : -1 y) (hy₂ : y 1) :
@[simp]
theorem real.arccos_zero  :
@[simp]
theorem real.arccos_one  :
@[simp]
theorem real.arccos_neg_one  :
@[simp]
theorem real.arccos_eq_zero {x : } :
@[simp]
theorem real.arccos_eq_pi_div_two {x : } :
real.arccos x = π / 2 x = 0
@[simp]
theorem real.arccos_eq_pi {x : } :
theorem real.sin_arccos {x : } (hx₁ : -1 x) (hx₂ : x 1) :
theorem real.has_strict_deriv_at_arccos {x : } (h₁ : x -1) (h₂ : x 1) :
theorem real.has_deriv_at_arccos {x : } (h₁ : x -1) (h₂ : x 1) :
theorem real.times_cont_diff_at_arccos {x : } (h₁ : x -1) (h₂ : x 1) {n : with_top } :
@[simp]
theorem real.deriv_arccos  :
deriv real.arccos = λ (x : ), -(1 / real.sqrt (1 - x ^ 2))