mathlib3 documentation

analysis.special_functions.sqrt

Smoothness of real.sqrt #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.deriv_sqrt_aux {x : } (hx : x 0) :
theorem real.has_strict_deriv_at_sqrt {x : } (hx : x 0) :
theorem real.cont_diff_at_sqrt {x : } {n : ℕ∞} (hx : x 0) :
theorem real.has_deriv_at_sqrt {x : } (hx : x 0) :
has_deriv_at (1 / (2 * x)) 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 : ), (f y)) (f' / (2 * (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 : ), (f y)) (f' / (2 * (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 : ), (f t)) (f' / (2 * (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 : ), (f x)) s x = deriv_within f s x / (2 * (f x))
@[simp]
theorem deriv_sqrt {f : } {x : } (hf : differentiable_at f x) (hx : f x 0) :
deriv (λ (x : ), (f x)) x = deriv f x / (2 * (f x))
theorem has_fderiv_at.sqrt {E : Type u_1} [normed_add_comm_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), (f y)) ((1 / (2 * (f x))) f') x
theorem has_strict_fderiv_at.sqrt {E : Type u_1} [normed_add_comm_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), (f y)) ((1 / (2 * (f x))) f') x
theorem has_fderiv_within_at.sqrt {E : Type u_1} [normed_add_comm_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), (f y)) ((1 / (2 * (f x))) f') s x
theorem differentiable_within_at.sqrt {E : Type u_1} [normed_add_comm_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), (f y)) s x
theorem differentiable_at.sqrt {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hf : differentiable_at f x) (hx : f x 0) :
differentiable_at (λ (y : E), (f y)) x
theorem differentiable_on.sqrt {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} (hf : differentiable_on f s) (hs : (x : E), x s f x 0) :
differentiable_on (λ (y : E), (f y)) s
theorem differentiable.sqrt {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } (hf : differentiable f) (hs : (x : E), f x 0) :
differentiable (λ (y : E), (f y))
theorem fderiv_within_sqrt {E : Type u_1} [normed_add_comm_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), (f x)) s x = (1 / (2 * (f x))) fderiv_within f s x
@[simp]
theorem fderiv_sqrt {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hf : differentiable_at f x) (hx : f x 0) :
fderiv (λ (x : E), (f x)) x = (1 / (2 * (f x))) fderiv f x
theorem cont_diff_at.sqrt {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} {x : E} (hf : cont_diff_at n f x) (hx : f x 0) :
cont_diff_at n (λ (y : E), (f y)) x
theorem cont_diff_within_at.sqrt {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} {s : set E} {x : E} (hf : cont_diff_within_at n f s x) (hx : f x 0) :
cont_diff_within_at n (λ (y : E), (f y)) s x
theorem cont_diff_on.sqrt {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} {s : set E} (hf : cont_diff_on n f s) (hs : (x : E), x s f x 0) :
cont_diff_on n (λ (y : E), (f y)) s
theorem cont_diff.sqrt {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} (hf : cont_diff n f) (h : (x : E), f x 0) :
cont_diff n (λ (y : E), (f y))