mathlib documentation

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

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

Equations
theorem real.has_deriv_at_sqrt {x : } (hx : x 0) :
theorem measurable.sqrt {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.sqrt (f x))
theorem has_deriv_within_at.sqrt {f : } {s : set } {f' x : } (hf : has_deriv_within_at f f' 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 : has_deriv_at f 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 : has_strict_deriv_at f f' 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 : differentiable_within_at f s x) (hx : f x 0) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.sqrt (f x)) s x = deriv_within f s x / 2 * real.sqrt (f x)
@[simp]
theorem deriv_sqrt {f : } {x : } (hf : differentiable_at f x) (hx : f x 0) :
deriv (λ (x : ), real.sqrt (f x)) x = deriv f x / 2 * real.sqrt (f x)
theorem has_fderiv_at.sqrt {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {f' : E →L[] } (hf : has_fderiv_at f 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} [normed_group E] [normed_space E] {f : E → } {x : E} {f' : E →L[] } (hf : has_strict_fderiv_at f f' 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} [normed_group E] [normed_space E] {f : E → } {s : set E} {x : E} {f' : E →L[] } (hf : has_fderiv_within_at f f' 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} [normed_group E] [normed_space E] {f : E → } {s : set E} {x : E} (hf : differentiable_within_at f s x) (hx : f x 0) :
differentiable_within_at (λ (y : E), real.sqrt (f y)) s x
theorem differentiable_at.sqrt {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hf : differentiable_at f x) (hx : f x 0) :
differentiable_at (λ (y : E), real.sqrt (f y)) x
theorem differentiable_on.sqrt {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hf : differentiable_on f s) (hs : ∀ (x : E), x sf x 0) :
differentiable_on (λ (y : E), real.sqrt (f y)) s
theorem differentiable.sqrt {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hf : differentiable f) (hs : ∀ (x : E), f x 0) :
differentiable (λ (y : E), real.sqrt (f y))
theorem fderiv_within_sqrt {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {x : E} (hf : differentiable_within_at f s x) (hx : f x 0) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.sqrt (f x)) s x = (1 / 2 * real.sqrt (f x)) fderiv_within f s x
@[simp]
theorem fderiv_sqrt {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hf : differentiable_at f x) (hx : f x 0) :
fderiv (λ (x : E), real.sqrt (f x)) x = (1 / 2 * real.sqrt (f x)) fderiv f x
theorem times_cont_diff_at.sqrt {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } {x : E} (hf : times_cont_diff_at n f x) (hx : f x 0) :
times_cont_diff_at n (λ (y : E), real.sqrt (f y)) x
theorem times_cont_diff_within_at.sqrt {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } {s : set E} {x : E} (hf : times_cont_diff_within_at n f s x) (hx : f x 0) :
times_cont_diff_within_at n (λ (y : E), real.sqrt (f y)) s x
theorem times_cont_diff_on.sqrt {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } {s : set E} (hf : times_cont_diff_on n f s) (hs : ∀ (x : E), x sf x 0) :
times_cont_diff_on n (λ (y : E), real.sqrt (f y)) s
theorem times_cont_diff.sqrt {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (hf : times_cont_diff n f) (h : ∀ (x : E), f x 0) :
times_cont_diff n (λ (y : E), real.sqrt (f y))