mathlib3 documentation

analysis.special_functions.trigonometric.inverse

Inverse trigonometric functions. #

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

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 on trigonometric functions.

source
noncomputable 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
source
theorem real.arcsin_mem_Icc (x : ℝ) :
real.arcsin x ∈ set.Icc (-(real.pi / 2)) (real.pi / 2)
source
@[simp]
theorem real.range_arcsin  :
set.range real.arcsin = set.Icc (-(real.pi / 2)) (real.pi / 2)
source
theorem real.arcsin_le_pi_div_two (x : ℝ) :
real.arcsin x ≤ real.pi / 2
source
theorem real.neg_pi_div_two_le_arcsin (x : ℝ) :
-(real.pi / 2) ≤ real.arcsin x
source
theorem real.arcsin_proj_Icc (x : ℝ) :
real.arcsin ↑(set.proj_Icc (-1) 1 _ x) = real.arcsin x
source
theorem real.sin_arcsin' {x : ℝ} (hx : x ∈ set.Icc (-1) 1) :
real.sin (real.arcsin x) = x
source
theorem real.sin_arcsin {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) :
real.sin (real.arcsin x) = x
source
theorem real.arcsin_sin' {x : ℝ} (hx : x ∈ set.Icc (-(real.pi / 2)) (real.pi / 2)) :
real.arcsin (real.sin x) = x
source
theorem real.arcsin_sin {x : ℝ} (hx₁ : -(real.pi / 2) ≤ x) (hx₂ : x ≤ real.pi / 2) :
real.arcsin (real.sin x) = x
source
theorem real.strict_mono_on_arcsin  :
strict_mono_on real.arcsin (set.Icc (-1) 1)
source
theorem real.monotone_arcsin  :
monotone real.arcsin
source
theorem real.inj_on_arcsin  :
set.inj_on real.arcsin (set.Icc (-1) 1)
source
theorem real.arcsin_inj {x y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) :
real.arcsin x = real.arcsin y ↔ x = y
source
@[continuity]
theorem real.continuous_arcsin  :
continuous real.arcsin
source
theorem real.continuous_at_arcsin {x : ℝ} :
continuous_at real.arcsin x
source
theorem real.arcsin_eq_of_sin_eq {x y : ℝ} (h₁ : real.sin x = y) (h₂ : x ∈ set.Icc (-(real.pi / 2)) (real.pi / 2)) :
real.arcsin y = x
source
@[simp]
theorem real.arcsin_zero  :
real.arcsin 0 = 0
source
@[simp]
theorem real.arcsin_one  :
real.arcsin 1 = real.pi / 2
source
theorem real.arcsin_of_one_le {x : ℝ} (hx : 1 ≤ x) :
real.arcsin x = real.pi / 2
source
theorem real.arcsin_neg_one  :
real.arcsin (-1) = -(real.pi / 2)
source
theorem real.arcsin_of_le_neg_one {x : ℝ} (hx : x ≤ -1) :
real.arcsin x = -(real.pi / 2)
source
@[simp]
theorem real.arcsin_neg (x : ℝ) :
real.arcsin (-x) = -real.arcsin x
source
theorem real.arcsin_le_iff_le_sin {x y : ℝ} (hx : x ∈ set.Icc (-1) 1) (hy : y ∈ set.Icc (-(real.pi / 2)) (real.pi / 2)) :
real.arcsin x ≤ y ↔ x ≤ real.sin y
source
theorem real.arcsin_le_iff_le_sin' {x y : ℝ} (hy : y ∈ set.Ico (-(real.pi / 2)) (real.pi / 2)) :
real.arcsin x ≤ y ↔ x ≤ real.sin y
source
theorem real.le_arcsin_iff_sin_le {x y : ℝ} (hx : x ∈ set.Icc (-(real.pi / 2)) (real.pi / 2)) (hy : y ∈ set.Icc (-1) 1) :
x ≤ real.arcsin y ↔ real.sin x ≤ y
source
theorem real.le_arcsin_iff_sin_le' {x y : ℝ} (hx : x ∈ set.Ioc (-(real.pi / 2)) (real.pi / 2)) :
x ≤ real.arcsin y ↔ real.sin x ≤ y
source
theorem real.arcsin_lt_iff_lt_sin {x y : ℝ} (hx : x ∈ set.Icc (-1) 1) (hy : y ∈ set.Icc (-(real.pi / 2)) (real.pi / 2)) :
real.arcsin x < y ↔ x < real.sin y
source
theorem real.arcsin_lt_iff_lt_sin' {x y : ℝ} (hy : y ∈ set.Ioc (-(real.pi / 2)) (real.pi / 2)) :
real.arcsin x < y ↔ x < real.sin y
source
theorem real.lt_arcsin_iff_sin_lt {x y : ℝ} (hx : x ∈ set.Icc (-(real.pi / 2)) (real.pi / 2)) (hy : y ∈ set.Icc (-1) 1) :
x < real.arcsin y ↔ real.sin x < y
source
theorem real.lt_arcsin_iff_sin_lt' {x y : ℝ} (hx : x ∈ set.Ico (-(real.pi / 2)) (real.pi / 2)) :
x < real.arcsin y ↔ real.sin x < y
source
theorem real.arcsin_eq_iff_eq_sin {x y : ℝ} (hy : y ∈ set.Ioo (-(real.pi / 2)) (real.pi / 2)) :
real.arcsin x = y ↔ x = real.sin y
source
@[simp]
theorem real.arcsin_nonneg {x : ℝ} :
0 ≤ real.arcsin x ↔ 0 ≤ x
source
@[simp]
theorem real.arcsin_nonpos {x : ℝ} :
real.arcsin x ≤ 0 ↔ x ≤ 0
source
@[simp]
theorem real.arcsin_eq_zero_iff {x : ℝ} :
real.arcsin x = 0 ↔ x = 0
source
@[simp]
theorem real.zero_eq_arcsin_iff {x : ℝ} :
0 = real.arcsin x ↔ x = 0
source
@[simp]
theorem real.arcsin_pos {x : ℝ} :
0 < real.arcsin x ↔ 0 < x
source
@[simp]
theorem real.arcsin_lt_zero {x : ℝ} :
real.arcsin x < 0 ↔ x < 0
source
@[simp]
theorem real.arcsin_lt_pi_div_two {x : ℝ} :
real.arcsin x < real.pi / 2 ↔ x < 1
source
@[simp]
theorem real.neg_pi_div_two_lt_arcsin {x : ℝ} :
-(real.pi / 2) < real.arcsin x ↔ -1 < x
source
@[simp]
theorem real.arcsin_eq_pi_div_two {x : ℝ} :
real.arcsin x = real.pi / 2 ↔ 1 ≤ x
source
@[simp]
theorem real.pi_div_two_eq_arcsin {x : ℝ} :
real.pi / 2 = real.arcsin x ↔ 1 ≤ x
source
@[simp]
theorem real.pi_div_two_le_arcsin {x : ℝ} :
real.pi / 2 ≤ real.arcsin x ↔ 1 ≤ x
source
@[simp]
theorem real.arcsin_eq_neg_pi_div_two {x : ℝ} :
real.arcsin x = -(real.pi / 2) ↔ x ≤ -1
source
@[simp]
theorem real.neg_pi_div_two_eq_arcsin {x : ℝ} :
-(real.pi / 2) = real.arcsin x ↔ x ≤ -1
source
@[simp]
theorem real.arcsin_le_neg_pi_div_two {x : ℝ} :
real.arcsin x ≤ -(real.pi / 2) ↔ x ≤ -1
source
@[simp]
theorem real.pi_div_four_le_arcsin {x : ℝ} :
real.pi / 4 ≤ real.arcsin x ↔ real.sqrt 2 / 2 ≤ x
source
theorem real.maps_to_sin_Ioo  :
set.maps_to real.sin (set.Ioo (-(real.pi / 2)) (real.pi / 2)) (set.Ioo (-1) 1)
source
@[simp]
noncomputable def real.sin_local_homeomorph  :
local_homeomorph ℝ ℝ

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

Equations
source
theorem real.cos_arcsin_nonneg (x : ℝ) :
0 ≤ real.cos (real.arcsin x)
source
theorem real.cos_arcsin (x : ℝ) :
real.cos (real.arcsin x) = real.sqrt (1 - x ^ 2)
source
theorem real.tan_arcsin (x : ℝ) :
real.tan (real.arcsin x) = x / real.sqrt (1 - x ^ 2)
source
noncomputable def real.arccos (x : ℝ) :
ℝ

Inverse of the cos function, returns values in the range 0 ≤ arccos x and arccos x ≤ π. It defaults to π on (-∞, -1) and to 0 to (1, ∞).

Equations
source
theorem real.arccos_eq_pi_div_two_sub_arcsin (x : ℝ) :
real.arccos x = real.pi / 2 - real.arcsin x
source
theorem real.arcsin_eq_pi_div_two_sub_arccos (x : ℝ) :
real.arcsin x = real.pi / 2 - real.arccos x
source
theorem real.arccos_le_pi (x : ℝ) :
real.arccos x ≤ real.pi
source
theorem real.arccos_nonneg (x : ℝ) :
0 ≤ real.arccos x
source
@[simp]
theorem real.arccos_pos {x : ℝ} :
0 < real.arccos x ↔ x < 1
source
theorem real.cos_arccos {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) :
real.cos (real.arccos x) = x
source
theorem real.arccos_cos {x : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x ≤ real.pi) :
real.arccos (real.cos x) = x
source
theorem real.strict_anti_on_arccos  :
strict_anti_on real.arccos (set.Icc (-1) 1)
source
theorem real.arccos_inj_on  :
set.inj_on real.arccos (set.Icc (-1) 1)
source
theorem real.arccos_inj {x y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) :
real.arccos x = real.arccos y ↔ x = y
source
@[simp]
theorem real.arccos_zero  :
real.arccos 0 = real.pi / 2
source
@[simp]
theorem real.arccos_one  :
real.arccos 1 = 0
source
@[simp]
theorem real.arccos_neg_one  :
real.arccos (-1) = real.pi
source
@[simp]
theorem real.arccos_eq_zero {x : ℝ} :
real.arccos x = 0 ↔ 1 ≤ x
source
@[simp]
theorem real.arccos_eq_pi_div_two {x : ℝ} :
real.arccos x = real.pi / 2 ↔ x = 0
source
@[simp]
theorem real.arccos_eq_pi {x : ℝ} :
real.arccos x = real.pi ↔ x ≤ -1
source
theorem real.arccos_neg (x : ℝ) :
real.arccos (-x) = real.pi - real.arccos x
source
theorem real.arccos_of_one_le {x : ℝ} (hx : 1 ≤ x) :
real.arccos x = 0
source
theorem real.arccos_of_le_neg_one {x : ℝ} (hx : x ≤ -1) :
real.arccos x = real.pi
source
theorem real.sin_arccos (x : ℝ) :
real.sin (real.arccos x) = real.sqrt (1 - x ^ 2)
source
@[simp]
theorem real.arccos_le_pi_div_two {x : ℝ} :
real.arccos x ≤ real.pi / 2 ↔ 0 ≤ x
source
@[simp]
theorem real.arccos_lt_pi_div_two {x : ℝ} :
real.arccos x < real.pi / 2 ↔ 0 < x
source
@[simp]
theorem real.arccos_le_pi_div_four {x : ℝ} :
real.arccos x ≤ real.pi / 4 ↔ real.sqrt 2 / 2 ≤ x
source
@[continuity]
theorem real.continuous_arccos  :
continuous real.arccos
source
theorem real.tan_arccos (x : ℝ) :
real.tan (real.arccos x) = real.sqrt (1 - x ^ 2) / x
source
theorem real.arccos_eq_arcsin {x : ℝ} (h : 0 ≤ x) :
real.arccos x = real.arcsin (real.sqrt (1 - x ^ 2))
source
theorem real.arcsin_eq_arccos {x : ℝ} (h : 0 ≤ x) :
real.arcsin x = real.arccos (real.sqrt (1 - x ^ 2))