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) :

has_strict_deriv_at real.arcsin (1 / √ (1 - x ^ 2)) x ∧ cont_diff_at ℝ ⊤ real.arcsin x

theorem real.has_strict_deriv_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :

has_strict_deriv_at real.arcsin (1 / √ (1 - x ^ 2)) x

theorem real.has_deriv_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :

has_deriv_at real.arcsin (1 / √ (1 - x ^ 2)) x

theorem real.cont_diff_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : ℕ∞} :

cont_diff_at ℝ n real.arcsin x

theorem real.has_deriv_within_at_arcsin_Ici {x : ℝ} (h : x ≠ -1) :

has_deriv_within_at real.arcsin (1 / √ (1 - x ^ 2)) (set.Ici x) x

theorem real.has_deriv_within_at_arcsin_Iic {x : ℝ} (h : x ≠ 1) :

has_deriv_within_at real.arcsin (1 / √ (1 - x ^ 2)) (set.Iic x) x

theorem real.differentiable_within_at_arcsin_Ici {x : ℝ} :

differentiable_within_at ℝ real.arcsin (set.Ici x) x ↔ x ≠ -1

theorem real.differentiable_within_at_arcsin_Iic {x : ℝ} :

differentiable_within_at ℝ real.arcsin (set.Iic x) x ↔ x ≠ 1

theorem real.differentiable_at_arcsin {x : ℝ} :

differentiable_at ℝ real.arcsin x ↔ x ≠ -1 ∧ x ≠ 1

@[simp]

theorem real.deriv_arcsin :

deriv real.arcsin = λ (x : ℝ), 1 / √ (1 - x ^ 2)

theorem real.differentiable_on_arcsin :

differentiable_on ℝ real.arcsin {-1, 1}ᶜ

theorem real.cont_diff_on_arcsin {n : ℕ∞} :

cont_diff_on ℝ n real.arcsin {-1, 1}ᶜ

theorem real.cont_diff_at_arcsin_iff {x : ℝ} {n : ℕ∞} :

cont_diff_at ℝ n real.arcsin x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1

theorem real.has_strict_deriv_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :

has_strict_deriv_at real.arccos (-(1 / √ (1 - x ^ 2))) x

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 : ℕ∞} :

cont_diff_at ℝ n real.arccos x

theorem real.has_deriv_within_at_arccos_Ici {x : ℝ} (h : x ≠ -1) :

has_deriv_within_at real.arccos (-(1 / √ (1 - x ^ 2))) (set.Ici x) x

theorem real.has_deriv_within_at_arccos_Iic {x : ℝ} (h : x ≠ 1) :

has_deriv_within_at real.arccos (-(1 / √ (1 - x ^ 2))) (set.Iic x) x

theorem real.differentiable_within_at_arccos_Ici {x : ℝ} :

differentiable_within_at ℝ real.arccos (set.Ici x) x ↔ x ≠ -1

theorem real.differentiable_within_at_arccos_Iic {x : ℝ} :

differentiable_within_at ℝ real.arccos (set.Iic x) x ↔ x ≠ 1

theorem real.differentiable_at_arccos {x : ℝ} :

differentiable_at ℝ real.arccos x ↔ x ≠ -1 ∧ x ≠ 1

@[simp]

theorem real.deriv_arccos :

deriv real.arccos = λ (x : ℝ), -(1 / √ (1 - x ^ 2))

theorem real.differentiable_on_arccos :

differentiable_on ℝ real.arccos {-1, 1}ᶜ

theorem real.cont_diff_on_arccos {n : ℕ∞} :

cont_diff_on ℝ n real.arccos {-1, 1}ᶜ

theorem real.cont_diff_at_arccos_iff {x : ℝ} {n : ℕ∞} :

cont_diff_at ℝ n real.arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1