# derivatives of the inverse trigonometric functions #

Derivatives of arcsin and arccos.

theorem Real.deriv_arcsin_aux {x : } (h₁ : x -1) (h₂ : x 1) :
HasStrictDerivAt Real.arcsin (1 / (1 - x ^ 2).sqrt) x
theorem Real.hasStrictDerivAt_arcsin {x : } (h₁ : x -1) (h₂ : x 1) :
HasStrictDerivAt Real.arcsin (1 / (1 - x ^ 2).sqrt) x
theorem Real.hasDerivAt_arcsin {x : } (h₁ : x -1) (h₂ : x 1) :
HasDerivAt Real.arcsin (1 / (1 - x ^ 2).sqrt) x
theorem Real.contDiffAt_arcsin {x : } (h₁ : x -1) (h₂ : x 1) {n : ℕ∞} :
theorem Real.hasDerivWithinAt_arcsin_Ici {x : } (h : x -1) :
HasDerivWithinAt Real.arcsin (1 / (1 - x ^ 2).sqrt) () x
theorem Real.hasDerivWithinAt_arcsin_Iic {x : } (h : x 1) :
HasDerivWithinAt Real.arcsin (1 / (1 - x ^ 2).sqrt) () x
@[simp]
theorem Real.deriv_arcsin :
= fun (x : ) => 1 / (1 - x ^ 2).sqrt
theorem Real.contDiffAt_arcsin_iff {x : } {n : ℕ∞} :
n = 0 x -1 x 1
theorem Real.hasStrictDerivAt_arccos {x : } (h₁ : x -1) (h₂ : x 1) :
HasStrictDerivAt Real.arccos (-(1 / (1 - x ^ 2).sqrt)) x
theorem Real.hasDerivAt_arccos {x : } (h₁ : x -1) (h₂ : x 1) :
HasDerivAt Real.arccos (-(1 / (1 - x ^ 2).sqrt)) x
theorem Real.contDiffAt_arccos {x : } (h₁ : x -1) (h₂ : x 1) {n : ℕ∞} :
theorem Real.hasDerivWithinAt_arccos_Ici {x : } (h : x -1) :
HasDerivWithinAt Real.arccos (-(1 / (1 - x ^ 2).sqrt)) () x
theorem Real.hasDerivWithinAt_arccos_Iic {x : } (h : x 1) :
HasDerivWithinAt Real.arccos (-(1 / (1 - x ^ 2).sqrt)) () x
@[simp]
theorem Real.deriv_arccos :
= fun (x : ) => -(1 / (1 - x ^ 2).sqrt)
theorem Real.contDiffAt_arccos_iff {x : } {n : ℕ∞} :
n = 0 x -1 x 1