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