mathlib documentation

analysis.special_functions.trigonometric.inverse_deriv

derivatives of the inverse trigonometric functions #

Derivatives of arcsin and arccos.

theorem real.deriv_arcsin_aux {x : } (h₁ : x -1) (h₂ : x 1) :
theorem real.has_strict_deriv_at_arcsin {x : } (h₁ : x -1) (h₂ : x 1) :
theorem real.has_deriv_at_arcsin {x : } (h₁ : x -1) (h₂ : x 1) :
theorem real.cont_diff_at_arcsin {x : } (h₁ : x -1) (h₂ : x 1) {n : with_top } :
@[simp]
theorem real.deriv_arcsin  :
deriv real.arcsin = λ (x : ), 1 / real.sqrt (1 - x ^ 2)
theorem real.has_strict_deriv_at_arccos {x : } (h₁ : x -1) (h₂ : x 1) :
theorem real.has_deriv_at_arccos {x : } (h₁ : x -1) (h₂ : x 1) :
theorem real.cont_diff_at_arccos {x : } (h₁ : x -1) (h₂ : x 1) {n : with_top } :
@[simp]
theorem real.deriv_arccos  :
deriv real.arccos = λ (x : ), -(1 / real.sqrt (1 - x ^ 2))