mathlib3 documentation

analysis.special_functions.trigonometric.inverse_deriv

derivatives of the inverse trigonometric functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : ℕ∞} :
@[simp]
theorem real.deriv_arcsin  :
deriv real.arcsin = λ (x : ), 1 / (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) :
has_deriv_at real.arccos (-(1 / (1 - x ^ 2))) x
theorem real.cont_diff_at_arccos {x : } (h₁ : x -1) (h₂ : x 1) {n : ℕ∞} :
@[simp]
theorem real.deriv_arccos  :
deriv real.arccos = λ (x : ), -(1 / (1 - x ^ 2))