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
- real.sq_local_homeomorph = {to_local_equiv := {to_fun := λ (x : ℝ), x ^ 2, inv_fun := real.sqrt, source := set.Ioi 0, target := set.Ioi 0, map_source' := real.sq_local_homeomorph._proof_1, map_target' := real.sq_local_homeomorph._proof_2, left_inv' := real.sq_local_homeomorph._proof_3, right_inv' := real.sq_local_homeomorph._proof_4}, open_source := real.sq_local_homeomorph._proof_5, open_target := real.sq_local_homeomorph._proof_6, continuous_to_fun := real.sq_local_homeomorph._proof_7, continuous_inv_fun := real.sq_local_homeomorph._proof_8}
theorem
real.has_strict_deriv_at_sqrt
{x : ℝ}
(hx : x ≠ 0) :
has_strict_deriv_at real.sqrt (1 / (2 * real.sqrt x)) x
theorem
real.has_deriv_at_sqrt
{x : ℝ}
(hx : x ≠ 0) :
has_deriv_at real.sqrt (1 / (2 * real.sqrt x)) x
theorem
has_strict_deriv_at.sqrt
{f : ℝ → ℝ}
{f' x : ℝ}
(hf : has_strict_deriv_at f f' x)
(hx : f x ≠ 0) :
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))
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) :
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) :
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) :
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), real.sqrt (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), real.sqrt (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), real.sqrt (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), real.sqrt (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), real.sqrt (f x)) s x = (1 / (2 * real.sqrt (f x))) • fderiv_within ℝ f s 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), real.sqrt (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), real.sqrt (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), real.sqrt (f y)) s