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)) x ∧ ContDiffAt ℝ ⊤ Real.arcsin x

theorem Real.hasStrictDerivAt_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : HasStrictDerivAt Real.arcsin (1 / √(1 - x ^ 2)) x

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 : ℕ∞} : ContDiffAt ℝ n Real.arcsin x

theorem Real.hasDerivWithinAt_arcsin_Ici {x : ℝ} (h : x ≠ -1) : HasDerivWithinAt Real.arcsin (1 / √(1 - x ^ 2)) (Set.Ici x) x

theorem Real.hasDerivWithinAt_arcsin_Iic {x : ℝ} (h : x ≠ 1) : HasDerivWithinAt Real.arcsin (1 / √(1 - x ^ 2)) (Set.Iic x) x

theorem Real.differentiableWithinAt_arcsin_Ici {x : ℝ} : DifferentiableWithinAt ℝ Real.arcsin (Set.Ici x) x ↔ x ≠ -1

theorem Real.differentiableWithinAt_arcsin_Iic {x : ℝ} : DifferentiableWithinAt ℝ Real.arcsin (Set.Iic x) x ↔ x ≠ 1

theorem Real.differentiableAt_arcsin {x : ℝ} : DifferentiableAt ℝ Real.arcsin x ↔ x ≠ -1 ∧ x ≠ 1

@[simp]

theorem Real.deriv_arcsin : deriv Real.arcsin = fun (x : ℝ) => 1 / √(1 - x ^ 2)

theorem Real.differentiableOn_arcsin : DifferentiableOn ℝ Real.arcsin {-1, 1}ᶜ

theorem Real.contDiffOn_arcsin {n : ℕ∞} : ContDiffOn ℝ n Real.arcsin {-1, 1}ᶜ

theorem Real.contDiffAt_arcsin_iff {x : ℝ} {n : ℕ∞} : ContDiffAt ℝ n Real.arcsin x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1

theorem Real.hasStrictDerivAt_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : HasStrictDerivAt Real.arccos (-(1 / √(1 - x ^ 2))) x

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 : ℕ∞} : ContDiffAt ℝ n Real.arccos x

theorem Real.hasDerivWithinAt_arccos_Ici {x : ℝ} (h : x ≠ -1) : HasDerivWithinAt Real.arccos (-(1 / √(1 - x ^ 2))) (Set.Ici x) x

theorem Real.hasDerivWithinAt_arccos_Iic {x : ℝ} (h : x ≠ 1) : HasDerivWithinAt Real.arccos (-(1 / √(1 - x ^ 2))) (Set.Iic x) x

theorem Real.differentiableWithinAt_arccos_Ici {x : ℝ} : DifferentiableWithinAt ℝ Real.arccos (Set.Ici x) x ↔ x ≠ -1

theorem Real.differentiableWithinAt_arccos_Iic {x : ℝ} : DifferentiableWithinAt ℝ Real.arccos (Set.Iic x) x ↔ x ≠ 1

theorem Real.differentiableAt_arccos {x : ℝ} : DifferentiableAt ℝ Real.arccos x ↔ x ≠ -1 ∧ x ≠ 1

@[simp]

theorem Real.deriv_arccos : deriv Real.arccos = fun (x : ℝ) => -(1 / √(1 - x ^ 2))

theorem Real.differentiableOn_arccos : DifferentiableOn ℝ Real.arccos {-1, 1}ᶜ

theorem Real.contDiffOn_arccos {n : ℕ∞} : ContDiffOn ℝ n Real.arccos {-1, 1}ᶜ

theorem Real.contDiffAt_arccos_iff {x : ℝ} {n : ℕ∞} : ContDiffAt ℝ n Real.arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1