Inverse trigonometric functions.

See also Analysis.SpecialFunctions.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.

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

• Real.arcsin = Subtype.val ∘ Set.IccExtend Real.arcsin.proof_2 ⇑Real.sinOrderIso.symm

theorem Real.arcsin_mem_Icc (x : ℝ) : x.arcsin ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)

@[simp]

theorem Real.range_arcsin : Set.range Real.arcsin = Set.Icc (-(Real.pi / 2)) (Real.pi / 2)

theorem Real.arcsin_le_pi_div_two (x : ℝ) : x.arcsin ≤ Real.pi / 2

theorem Real.neg_pi_div_two_le_arcsin (x : ℝ) : -(Real.pi / 2) ≤ x.arcsin

theorem Real.arcsin_projIcc (x : ℝ) : (↑(Set.projIcc (-1) 1 ⋯ x)).arcsin = x.arcsin

theorem Real.sin_arcsin' {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : x.arcsin.sin = x

theorem Real.sin_arcsin {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) : x.arcsin.sin = x

theorem Real.arcsin_sin' {x : ℝ} (hx : x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) : x.sin.arcsin = x

theorem Real.arcsin_sin {x : ℝ} (hx₁ : -(Real.pi / 2) ≤ x) (hx₂ : x ≤ Real.pi / 2) : x.sin.arcsin = x

theorem Real.strictMonoOn_arcsin : StrictMonoOn Real.arcsin (Set.Icc (-1) 1)

theorem Real.monotone_arcsin : Monotone Real.arcsin

theorem Real.injOn_arcsin : Set.InjOn Real.arcsin (Set.Icc (-1) 1)

theorem Real.arcsin_inj {x : ℝ} {y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) : x.arcsin = y.arcsin ↔ x = y

theorem Real.continuous_arcsin : Continuous Real.arcsin

theorem Real.continuousAt_arcsin {x : ℝ} : ContinuousAt Real.arcsin x

theorem Real.arcsin_eq_of_sin_eq {x : ℝ} {y : ℝ} (h₁ : x.sin = y) (h₂ : x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) : y.arcsin = x

@[simp]

theorem Real.arcsin_zero : Real.arcsin 0 = 0

@[simp]

theorem Real.arcsin_one : Real.arcsin 1 = Real.pi / 2

theorem Real.arcsin_of_one_le {x : ℝ} (hx : 1 ≤ x) : x.arcsin = Real.pi / 2

theorem Real.arcsin_neg_one : (-1).arcsin = -(Real.pi / 2)

theorem Real.arcsin_of_le_neg_one {x : ℝ} (hx : x ≤ -1) : x.arcsin = -(Real.pi / 2)

@[simp]

theorem Real.arcsin_neg (x : ℝ) : (-x).arcsin = -x.arcsin

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)) : x.arcsin ≤ y ↔ x ≤ y.sin

theorem Real.arcsin_le_iff_le_sin' {x : ℝ} {y : ℝ} (hy : y ∈ Set.Ico (-(Real.pi / 2)) (Real.pi / 2)) : x.arcsin ≤ y ↔ x ≤ y.sin

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 ≤ y.arcsin ↔ x.sin ≤ y

theorem Real.le_arcsin_iff_sin_le' {x : ℝ} {y : ℝ} (hx : x ∈ Set.Ioc (-(Real.pi / 2)) (Real.pi / 2)) : x ≤ y.arcsin ↔ x.sin ≤ y

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)) : x.arcsin < y ↔ x < y.sin

theorem Real.arcsin_lt_iff_lt_sin' {x : ℝ} {y : ℝ} (hy : y ∈ Set.Ioc (-(Real.pi / 2)) (Real.pi / 2)) : x.arcsin < y ↔ x < y.sin

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 < y.arcsin ↔ x.sin < y

theorem Real.lt_arcsin_iff_sin_lt' {x : ℝ} {y : ℝ} (hx : x ∈ Set.Ico (-(Real.pi / 2)) (Real.pi / 2)) : x < y.arcsin ↔ x.sin < y

theorem Real.arcsin_eq_iff_eq_sin {x : ℝ} {y : ℝ} (hy : y ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) : x.arcsin = y ↔ x = y.sin

@[simp]

theorem Real.arcsin_nonneg {x : ℝ} : 0 ≤ x.arcsin ↔ 0 ≤ x

@[simp]

theorem Real.arcsin_nonpos {x : ℝ} : x.arcsin ≤ 0 ↔ x ≤ 0

@[simp]

theorem Real.arcsin_eq_zero_iff {x : ℝ} : x.arcsin = 0 ↔ x = 0

@[simp]

theorem Real.zero_eq_arcsin_iff {x : ℝ} : 0 = x.arcsin ↔ x = 0

@[simp]

theorem Real.arcsin_pos {x : ℝ} : 0 < x.arcsin ↔ 0 < x

@[simp]

theorem Real.arcsin_lt_zero {x : ℝ} : x.arcsin < 0 ↔ x < 0

@[simp]

theorem Real.arcsin_lt_pi_div_two {x : ℝ} : x.arcsin < Real.pi / 2 ↔ x < 1

@[simp]

theorem Real.neg_pi_div_two_lt_arcsin {x : ℝ} : -(Real.pi / 2) < x.arcsin ↔ -1 < x

@[simp]

theorem Real.arcsin_eq_pi_div_two {x : ℝ} : x.arcsin = Real.pi / 2 ↔ 1 ≤ x

@[simp]

theorem Real.pi_div_two_eq_arcsin {x : ℝ} : Real.pi / 2 = x.arcsin ↔ 1 ≤ x

@[simp]

theorem Real.pi_div_two_le_arcsin {x : ℝ} : Real.pi / 2 ≤ x.arcsin ↔ 1 ≤ x

@[simp]

theorem Real.arcsin_eq_neg_pi_div_two {x : ℝ} : x.arcsin = -(Real.pi / 2) ↔ x ≤ -1

@[simp]

theorem Real.neg_pi_div_two_eq_arcsin {x : ℝ} : -(Real.pi / 2) = x.arcsin ↔ x ≤ -1

@[simp]

theorem Real.arcsin_le_neg_pi_div_two {x : ℝ} : x.arcsin ≤ -(Real.pi / 2) ↔ x ≤ -1

@[simp]

theorem Real.pi_div_four_le_arcsin {x : ℝ} : Real.pi / 4 ≤ x.arcsin ↔ √2 / 2 ≤ x

theorem Real.mapsTo_sin_Ioo : Set.MapsTo Real.sin (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) (Set.Ioo (-1) 1)

def Real.sinPartialHomeomorph : PartialHomeomorph ℝ ℝ

Real.sin as a PartialHomeomorph between (-π / 2, π / 2) and (-1, 1).

Equations

• One or more equations did not get rendered due to their size.

theorem Real.cos_arcsin_nonneg (x : ℝ) : 0 ≤ x.arcsin.cos

theorem Real.cos_arcsin (x : ℝ) : x.arcsin.cos = (1 - x ^ 2).sqrt

theorem Real.tan_arcsin (x : ℝ) : x.arcsin.tan = x / (1 - x ^ 2).sqrt

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

• x.arccos = Real.pi / 2 - x.arcsin

theorem Real.arccos_eq_pi_div_two_sub_arcsin (x : ℝ) : x.arccos = Real.pi / 2 - x.arcsin

theorem Real.arcsin_eq_pi_div_two_sub_arccos (x : ℝ) : x.arcsin = Real.pi / 2 - x.arccos

theorem Real.arccos_le_pi (x : ℝ) : x.arccos ≤ Real.pi

theorem Real.arccos_nonneg (x : ℝ) : 0 ≤ x.arccos

@[simp]

theorem Real.arccos_pos {x : ℝ} : 0 < x.arccos ↔ x < 1

theorem Real.cos_arccos {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) : x.arccos.cos = x

theorem Real.arccos_cos {x : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x ≤ Real.pi) : x.cos.arccos = x

theorem Real.arccos_eq_of_eq_cos {x : ℝ} {y : ℝ} (hy₀ : 0 ≤ y) (hy₁ : y ≤ Real.pi) (hxy : x = y.cos) : x.arccos = y

theorem Real.strictAntiOn_arccos : StrictAntiOn Real.arccos (Set.Icc (-1) 1)

theorem Real.arccos_injOn : Set.InjOn Real.arccos (Set.Icc (-1) 1)

theorem Real.arccos_inj {x : ℝ} {y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) : x.arccos = y.arccos ↔ x = y

@[simp]

theorem Real.arccos_zero : Real.arccos 0 = Real.pi / 2

@[simp]

theorem Real.arccos_one : Real.arccos 1 = 0

@[simp]

theorem Real.arccos_neg_one : (-1).arccos = Real.pi

@[simp]

theorem Real.arccos_eq_zero {x : ℝ} : x.arccos = 0 ↔ 1 ≤ x

@[simp]

theorem Real.arccos_eq_pi_div_two {x : ℝ} : x.arccos = Real.pi / 2 ↔ x = 0

@[simp]

theorem Real.arccos_eq_pi {x : ℝ} : x.arccos = Real.pi ↔ x ≤ -1

theorem Real.arccos_neg (x : ℝ) : (-x).arccos = Real.pi - x.arccos

theorem Real.arccos_of_one_le {x : ℝ} (hx : 1 ≤ x) : x.arccos = 0

theorem Real.arccos_of_le_neg_one {x : ℝ} (hx : x ≤ -1) : x.arccos = Real.pi

theorem Real.sin_arccos (x : ℝ) : x.arccos.sin = (1 - x ^ 2).sqrt

@[simp]

theorem Real.arccos_le_pi_div_two {x : ℝ} : x.arccos ≤ Real.pi / 2 ↔ 0 ≤ x

@[simp]

theorem Real.arccos_lt_pi_div_two {x : ℝ} : x.arccos < Real.pi / 2 ↔ 0 < x

@[simp]

theorem Real.arccos_le_pi_div_four {x : ℝ} : x.arccos ≤ Real.pi / 4 ↔ √2 / 2 ≤ x

theorem Real.continuous_arccos : Continuous Real.arccos

theorem Real.tan_arccos (x : ℝ) : x.arccos.tan = (1 - x ^ 2).sqrt / x

theorem Real.arccos_eq_arcsin {x : ℝ} (h : 0 ≤ x) : x.arccos = (1 - x ^ 2).sqrt.arcsin

theorem Real.arcsin_eq_arccos {x : ℝ} (h : 0 ≤ x) : x.arcsin = (1 - x ^ 2).sqrt.arccos