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, ∞).

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

@[simp]

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

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

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

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

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

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

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

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

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

theorem Real.arcsin_lt_arcsin {x y : ℝ} (hx : -1 ≤ x) (hlt : x < y) (hy : y ≤ 1) : arcsin x < arcsin y

theorem Real.monotone_arcsin : Monotone arcsin

theorem Real.arcsin_le_arcsin {x y : ℝ} (h : x ≤ y) : arcsin x ≤ arcsin y

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

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

theorem Real.continuous_arcsin : Continuous arcsin

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

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

@[simp]

theorem Real.arcsin_zero : arcsin 0 = 0

@[simp]

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

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

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

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

@[simp]

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

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

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

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

theorem Real.le_arcsin_iff_sin_le' {x y : ℝ} (hx : x ∈ Set.Ioc (-(Real.pi / 2)) (Real.pi / 2)) : x ≤ arcsin y ↔ sin x ≤ 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)) : arcsin x < y ↔ x < sin y

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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, ∞).

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

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

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

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

@[simp]

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

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

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

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

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

theorem Real.arccos_lt_arccos {x y : ℝ} (hx : -1 ≤ x) (hlt : x < y) (hy : y ≤ 1) : arccos y < arccos x

theorem Real.arccos_le_arccos {x y : ℝ} (hlt : x ≤ y) : arccos y ≤ arccos x

theorem Real.antitone_arccos : Antitone arccos

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

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

@[simp]

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

@[simp]

theorem Real.arccos_one : arccos 1 = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Real.arccos_lt_pi {x : ℝ} : arccos x < Real.pi ↔ -1 < x

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Real.continuous_arccos : Continuous arccos

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

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

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

def Real.sinPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ

Real.sin as an OpenPartialHomeomorph between (-π / 2, π / 2) and (-1, 1).

def Real.sinPartialEquiv : PartialEquiv ℝ ℝ

Real.sin and Real.arcsin as a (partial) equivalence from [-(π / 2), (π / 2)] to [-1, 1]

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

@[simp]

theorem Real.arcsin_image_Icc : arcsin '' Set.Icc (-1) 1 = Set.Icc (-(Real.pi / 2)) (Real.pi / 2)

def Real.cosPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ

Real.cos as an OpenPartialHomeomorph between (0, π) and (-1, 1).

noncomputable def Real.cosPartialEquiv : PartialEquiv ℝ ℝ

Real.cos and Real.arccos as a (partial) equivalence from [0, π] to [-1, 1]

@[simp]

theorem Real.cosPartialEquiv_apply (θ : ℝ) : ↑cosPartialEquiv θ = cos θ

@[simp]

theorem Real.cosPartialEquiv_source : cosPartialEquiv.source = Set.Icc 0 Real.pi

@[simp]

theorem Real.cosPartialEquiv_symm_apply (x : ℝ) : ↑cosPartialEquiv.symm x = arccos x

@[simp]

theorem Real.cosPartialEquiv_target : cosPartialEquiv.target = Set.Icc (-1) 1

theorem Real.mapsTo_cos_Ioo : Set.MapsTo cos (Set.Ioo 0 Real.pi) (Set.Ioo (-1) 1)

@[simp]

theorem Real.arccos_image_Icc : arccos '' Set.Icc (-1) 1 = Set.Icc 0 Real.pi

Convenience dot notation lemmas

theorem Filter.Tendsto.arcsin {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ} (h : Tendsto f l (nhds x)) : Tendsto (fun (x : α) => Real.arcsin (f x)) l (nhds (Real.arcsin x))

theorem Filter.Tendsto.arcsin_nhdsLE {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ} (h : Tendsto f l (nhdsWithin x (Set.Iic x))) : Tendsto (fun (x : α) => Real.arcsin (f x)) l (nhdsWithin (Real.arcsin x) (Set.Iic (Real.arcsin x)))

theorem Filter.Tendsto.arcsin_nhdsGE {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ} (h : Tendsto f l (nhdsWithin x (Set.Ici x))) : Tendsto (fun (x : α) => Real.arcsin (f x)) l (nhdsWithin (Real.arcsin x) (Set.Ici (Real.arcsin x)))

theorem Filter.Tendsto.arccos {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ} (h : Tendsto f l (nhds x)) : Tendsto (fun (x : α) => Real.arccos (f x)) l (nhds (Real.arccos x))

theorem Filter.Tendsto.arccos_nhdsLE {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ} (h : Tendsto f l (nhdsWithin x (Set.Iic x))) : Tendsto (fun (x : α) => Real.arccos (f x)) l (nhdsWithin (Real.arccos x) (Set.Ici (Real.arccos x)))

theorem Filter.Tendsto.arccos_nhdsGE {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ} (h : Tendsto f l (nhdsWithin x (Set.Ici x))) : Tendsto (fun (x : α) => Real.arccos (f x)) l (nhdsWithin (Real.arccos x) (Set.Iic (Real.arccos x)))

theorem ContinuousWithinAt.arcsin {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {s : Set X} {x : X} (h : ContinuousWithinAt f s x) : ContinuousWithinAt (fun (x : X) => Real.arcsin (f x)) s x

theorem ContinuousWithinAt.arccos {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {s : Set X} {x : X} (h : ContinuousWithinAt f s x) : ContinuousWithinAt (fun (x : X) => Real.arccos (f x)) s x

theorem ContinuousAt.arcsin {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {x : X} (h : ContinuousAt f x) : ContinuousAt (fun (x : X) => Real.arcsin (f x)) x

theorem ContinuousAt.arccos {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {x : X} (h : ContinuousAt f x) : ContinuousAt (fun (x : X) => Real.arccos (f x)) x

theorem ContinuousOn.arcsin {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {s : Set X} (h : ContinuousOn f s) : ContinuousOn (fun (x : X) => Real.arcsin (f x)) s

theorem ContinuousOn.arccos {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {s : Set X} (h : ContinuousOn f s) : ContinuousOn (fun (x : X) => Real.arccos (f x)) s

theorem Continuous.arcsin {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} (h : Continuous f) : Continuous fun (x : X) => Real.arcsin (f x)

theorem Continuous.arccos {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} (h : Continuous f) : Continuous fun (x : X) => Real.arccos (f x)