English
For x ≠ 0, sqrt has a strict derivative at x equal to 1/(2√x), and sqrt is ContDiffAt for all orders at x.
Русский
Для x ≠ 0 функция sqrt имеет строгую производную в точке x, равную 1/(2√x), и sqrt гладкая в точке x для любого порядка.
LaTeX
$$$$ \forall x \neq 0,\ HasStrictDerivAt(\sqrt{\cdot})(\frac{1}{2\sqrt{x}})(x) \land \forall n,\ ContDiffAt(\mathbb{R}, n, \sqrt{\cdot}, x). $$$$
Lean4
theorem deriv_sqrt_aux {x : ℝ} (hx : x ≠ 0) : HasStrictDerivAt (√·) (1 / (2 * √x)) x ∧ ∀ n, ContDiffAt ℝ n (√·) x :=
by
rcases hx.lt_or_gt with hx | hx
· rw [sqrt_eq_zero_of_nonpos hx.le, mul_zero, div_zero]
have : (√·) =ᶠ[𝓝 x] fun _ => 0 := (gt_mem_nhds hx).mono fun x hx => sqrt_eq_zero_of_nonpos hx.le
exact
⟨(hasStrictDerivAt_const x (0 : ℝ)).congr_of_eventuallyEq this.symm, fun n =>
contDiffAt_const.congr_of_eventuallyEq this⟩
· have : ↑2 * √x ^ (2 - 1) ≠ 0 := by simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]
constructor
· simpa using sqPartialHomeomorph.hasStrictDerivAt_symm hx this (hasStrictDerivAt_pow 2 _)
· exact fun n => sqPartialHomeomorph.contDiffAt_symm_deriv this hx (hasDerivAt_pow 2 (√x)) (contDiffAt_id.pow 2)
