Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

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.hasStrictDerivAt_arcsin {x : } (h₁ : x -1) (h₂ : x 1) :
theorem Real.hasDerivAt_arcsin {x : } (h₁ : x -1) (h₂ : x 1) :
theorem Real.contDiffAt_arcsin {x : } (h₁ : x -1) (h₂ : x 1) {n : ℕ∞} :
@[simp]
theorem Real.deriv_arcsin :
deriv Real.arcsin = fun (x : ) => 1 / Real.sqrt (1 - x ^ 2)
theorem Real.hasStrictDerivAt_arccos {x : } (h₁ : x -1) (h₂ : x 1) :
theorem Real.hasDerivAt_arccos {x : } (h₁ : x -1) (h₂ : x 1) :
theorem Real.contDiffAt_arccos {x : } (h₁ : x -1) (h₂ : x 1) {n : ℕ∞} :
@[simp]
theorem Real.deriv_arccos :
deriv Real.arccos = fun (x : ) => -(1 / Real.sqrt (1 - x ^ 2))