# mathlibdocumentation

analysis.special_functions.sqrt

# Smoothness of real.sqrt#

In this file we prove that real.sqrt is infinitely smooth at all points x ≠ 0 and provide some dot-notation lemmas.

## Tags #

sqrt, differentiable

noncomputable def real.sq_local_homeomorph  :

Local homeomorph between (0, +∞) and (0, +∞) with to_fun = λ x, x ^ 2 and inv_fun = sqrt.

Equations
theorem real.deriv_sqrt_aux {x : } (hx : x 0) :
(1 / (2 * real.sqrt x)) x ∀ (n : ℕ∞),
theorem real.has_strict_deriv_at_sqrt {x : } (hx : x 0) :
(1 / (2 * real.sqrt x)) x
theorem real.cont_diff_at_sqrt {x : } {n : ℕ∞} (hx : x 0) :
theorem real.has_deriv_at_sqrt {x : } (hx : x 0) :
(1 / (2 * real.sqrt x)) x
theorem has_deriv_within_at.sqrt {f : } {s : set } {f' x : } (hf : s x) (hx : f x 0) :
has_deriv_within_at (λ (y : ), real.sqrt (f y)) (f' / (2 * real.sqrt (f x))) s x
theorem has_deriv_at.sqrt {f : } {f' x : } (hf : f' x) (hx : f x 0) :
has_deriv_at (λ (y : ), real.sqrt (f y)) (f' / (2 * real.sqrt (f x))) x
theorem has_strict_deriv_at.sqrt {f : } {f' x : } (hf : x) (hx : f x 0) :
has_strict_deriv_at (λ (t : ), real.sqrt (f t)) (f' / (2 * real.sqrt (f x))) x
theorem deriv_within_sqrt {f : } {s : set } {x : } (hf : x) (hx : f x 0) (hxs : x) :
deriv_within (λ (x : ), real.sqrt (f x)) s x = s x / (2 * real.sqrt (f x))
@[simp]
theorem deriv_sqrt {f : } {x : } (hf : x) (hx : f x 0) :
deriv (λ (x : ), real.sqrt (f x)) x = x / (2 * real.sqrt (f x))
theorem has_fderiv_at.sqrt {E : Type u_1} [ E] {f : E → } {x : E} {f' : E →L[] } (hf : f' x) (hx : f x 0) :
has_fderiv_at (λ (y : E), real.sqrt (f y)) ((1 / (2 * real.sqrt (f x))) f') x
theorem has_strict_fderiv_at.sqrt {E : Type u_1} [ E] {f : E → } {x : E} {f' : E →L[] } (hf : x) (hx : f x 0) :
has_strict_fderiv_at (λ (y : E), real.sqrt (f y)) ((1 / (2 * real.sqrt (f x))) f') x
theorem has_fderiv_within_at.sqrt {E : Type u_1} [ E] {f : E → } {s : set E} {x : E} {f' : E →L[] } (hf : s x) (hx : f x 0) :
has_fderiv_within_at (λ (y : E), real.sqrt (f y)) ((1 / (2 * real.sqrt (f x))) f') s x
theorem differentiable_within_at.sqrt {E : Type u_1} [ E] {f : E → } {s : set E} {x : E} (hf : x) (hx : f x 0) :
(λ (y : E), real.sqrt (f y)) s x
theorem differentiable_at.sqrt {E : Type u_1} [ E] {f : E → } {x : E} (hf : x) (hx : f x 0) :
(λ (y : E), real.sqrt (f y)) x
theorem differentiable_on.sqrt {E : Type u_1} [ E] {f : E → } {s : set E} (hf : s) (hs : ∀ (x : E), x sf x 0) :
(λ (y : E), real.sqrt (f y)) s
theorem differentiable.sqrt {E : Type u_1} [ E] {f : E → } (hf : f) (hs : ∀ (x : E), f x 0) :
(λ (y : E), real.sqrt (f y))
theorem fderiv_within_sqrt {E : Type u_1} [ E] {f : E → } {s : set E} {x : E} (hf : x) (hx : f x 0) (hxs : x) :
(λ (x : E), real.sqrt (f x)) s x = (1 / (2 * real.sqrt (f x))) s x
@[simp]
theorem fderiv_sqrt {E : Type u_1} [ E] {f : E → } {x : E} (hf : x) (hx : f x 0) :
(λ (x : E), real.sqrt (f x)) x = (1 / (2 * real.sqrt (f x))) f x
theorem cont_diff_at.sqrt {E : Type u_1} [ E] {f : E → } {n : ℕ∞} {x : E} (hf : f x) (hx : f x 0) :
(λ (y : E), real.sqrt (f y)) x
theorem cont_diff_within_at.sqrt {E : Type u_1} [ E] {f : E → } {n : ℕ∞} {s : set E} {x : E} (hf : s x) (hx : f x 0) :
(λ (y : E), real.sqrt (f y)) s x
theorem cont_diff_on.sqrt {E : Type u_1} [ E] {f : E → } {n : ℕ∞} {s : set E} (hf : f s) (hs : ∀ (x : E), x sf x 0) :
(λ (y : E), real.sqrt (f y)) s
theorem cont_diff.sqrt {E : Type u_1} [ E] {f : E → } {n : ℕ∞} (hf : f) (h : ∀ (x : E), f x 0) :
(λ (y : E), real.sqrt (f y))