derivatives of the inverse trigonometric functions

Derivatives of arcsin and arccos.

theorem Real.deriv_arcsin_aux {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x

theorem Real.hasStrictDerivAt_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x

theorem Real.hasDerivAt_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : HasDerivAt arcsin (1 / √(1 - x ^ 2)) x

theorem Real.contDiffAt_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : WithTop ℕ∞} : ContDiffAt ℝ n arcsin x

theorem Real.hasDerivWithinAt_arcsin_Ici {x : ℝ} (h : x ≠ -1) : HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Set.Ici x) x

theorem Real.hasDerivWithinAt_arcsin_Iic {x : ℝ} (h : x ≠ 1) : HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Set.Iic x) x

theorem Real.differentiableWithinAt_arcsin_Ici {x : ℝ} : DifferentiableWithinAt ℝ arcsin (Set.Ici x) x ↔ x ≠ -1

theorem Real.differentiableWithinAt_arcsin_Iic {x : ℝ} : DifferentiableWithinAt ℝ arcsin (Set.Iic x) x ↔ x ≠ 1

theorem Real.differentiableAt_arcsin {x : ℝ} : DifferentiableAt ℝ arcsin x ↔ x ≠ -1 ∧ x ≠ 1

@[simp]

theorem Real.deriv_arcsin : deriv arcsin = fun (x : ℝ) => 1 / √(1 - x ^ 2)

theorem Real.differentiableOn_arcsin : DifferentiableOn ℝ arcsin {-1, 1}ᶜ

theorem Real.contDiffOn_arcsin {n : WithTop ℕ∞} : ContDiffOn ℝ n arcsin {-1, 1}ᶜ

theorem Real.contDiffAt_arcsin_iff {x : ℝ} {n : WithTop ℕ∞} : ContDiffAt ℝ n arcsin x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1

theorem Real.hasStrictDerivAt_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : HasStrictDerivAt arccos (-(1 / √(1 - x ^ 2))) x

theorem Real.hasDerivAt_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : HasDerivAt arccos (-(1 / √(1 - x ^ 2))) x

theorem Real.contDiffAt_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : WithTop ℕ∞} : ContDiffAt ℝ n arccos x

theorem Real.hasDerivWithinAt_arccos_Ici {x : ℝ} (h : x ≠ -1) : HasDerivWithinAt arccos (-(1 / √(1 - x ^ 2))) (Set.Ici x) x

theorem Real.hasDerivWithinAt_arccos_Iic {x : ℝ} (h : x ≠ 1) : HasDerivWithinAt arccos (-(1 / √(1 - x ^ 2))) (Set.Iic x) x

theorem Real.differentiableWithinAt_arccos_Ici {x : ℝ} : DifferentiableWithinAt ℝ arccos (Set.Ici x) x ↔ x ≠ -1

theorem Real.differentiableWithinAt_arccos_Iic {x : ℝ} : DifferentiableWithinAt ℝ arccos (Set.Iic x) x ↔ x ≠ 1

theorem Real.differentiableAt_arccos {x : ℝ} : DifferentiableAt ℝ arccos x ↔ x ≠ -1 ∧ x ≠ 1

@[simp]

theorem Real.deriv_arccos : deriv arccos = fun (x : ℝ) => -(1 / √(1 - x ^ 2))

theorem Real.differentiableOn_arccos : DifferentiableOn ℝ arccos {-1, 1}ᶜ

theorem Real.contDiffOn_arccos {n : WithTop ℕ∞} : ContDiffOn ℝ n arccos {-1, 1}ᶜ

theorem Real.contDiffAt_arccos_iff {x : ℝ} {n : WithTop ℕ∞} : ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1