English
For x ≠ -1 and x ≠ 1, arcsin has a strict derivative at x equal to 1/√(1 - x^2), and arcsin is cont-differentiable at x.
Русский
Для x ≠ -1 и x ≠ 1 функция arcsin имеет строгую производную в точке x равную 1/√(1 - x^2), и arcsin дифференцируема в окрестности x.
LaTeX
$$HasStrictDerivAt(\arcsin, \frac{1}{\sqrt{1 - x^2}}, x) ∧ ContDiffAt(\mathbb{R}, \omega, arcsin, x)$$
Lean4
theorem deriv_arcsin_aux {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x :=
by
rcases h₁.lt_or_gt with h₁ | h₁
· have : 1 - x ^ 2 < 0 := by nlinarith [h₁]
rw [sqrt_eq_zero'.2 this.le, div_zero]
have : arcsin =ᶠ[𝓝 x] fun _ => -(π / 2) := (gt_mem_nhds h₁).mono fun y hy => arcsin_of_le_neg_one hy.le
exact ⟨(hasStrictDerivAt_const x _).congr_of_eventuallyEq this.symm, contDiffAt_const.congr_of_eventuallyEq this⟩
rcases h₂.lt_or_gt with h₂ | h₂
· have : 0 < √(1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂])
simp only [← cos_arcsin, one_div] at this ⊢
exact
⟨sinPartialHomeomorph.hasStrictDerivAt_symm ⟨h₁, h₂⟩ this.ne' (hasStrictDerivAt_sin _),
sinPartialHomeomorph.contDiffAt_symm_deriv this.ne' ⟨h₁, h₂⟩ (hasDerivAt_sin _) contDiff_sin.contDiffAt⟩
· have : 1 - x ^ 2 < 0 := by nlinarith [h₂]
rw [sqrt_eq_zero'.2 this.le, div_zero]
have : arcsin =ᶠ[𝓝 x] fun _ => π / 2 := (lt_mem_nhds h₂).mono fun y hy => arcsin_of_one_le hy.le
exact ⟨(hasStrictDerivAt_const x _).congr_of_eventuallyEq this.symm, contDiffAt_const.congr_of_eventuallyEq this⟩
