# 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

source
noncomputable def Real.sqPartialHomeomorph :
OpenPartialHomeomorph ℝ ℝ

Local homeomorph between `(0, +∞)` and `(0, +∞)` with `toFun = (· ^ 2)` and `invFun = Real.sqrt`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Real.deriv_sqrt_aux {x : ℝ} (hx : x ≠ 0) :
HasStrictDerivAt (fun (x : ℝ) => √x) (1 / (2 * √x)) x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun (x : ℝ) => √x) x
source
theorem Real.hasStrictDerivAt_sqrt {x : ℝ} (hx : x ≠ 0) :
HasStrictDerivAt (fun (x : ℝ) => √x) (1 / (2 * √x)) x
source
theorem Real.contDiffAt_sqrt {x : ℝ} {n : WithTop ℕ∞} (hx : x ≠ 0) :
ContDiffAt ℝ n (fun (x : ℝ) => √x) x
source
theorem Real.hasDerivAt_sqrt {x : ℝ} (hx : x ≠ 0) :
HasDerivAt (fun (x : ℝ) => √x) (1 / (2 * √x)) x
source
theorem HasDerivWithinAt.sqrt {f : ℝ → ℝ} {s : Set ℝ} {f' x : ℝ} (hf : HasDerivWithinAt f f' s x) (hx : f x ≠ 0) :
HasDerivWithinAt (fun (y : ℝ) => √(f y)) (f' / (2 * √(f x))) s x
source
theorem HasDerivAt.sqrt {f : ℝ → ℝ} {f' x : ℝ} (hf : HasDerivAt f f' x) (hx : f x ≠ 0) :
HasDerivAt (fun (y : ℝ) => √(f y)) (f' / (2 * √(f x))) x
source
theorem HasStrictDerivAt.sqrt {f : ℝ → ℝ} {f' x : ℝ} (hf : HasStrictDerivAt f f' x) (hx : f x ≠ 0) :
HasStrictDerivAt (fun (t : ℝ) => √(f t)) (f' / (2 * √(f x))) x
source
theorem derivWithin_sqrt {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0) (hxs : UniqueDiffWithinAt ℝ s x) :
derivWithin (fun (x : ℝ) => √(f x)) s x = derivWithin f s x / (2 * √(f x))
source
@[simp]
theorem deriv_sqrt {f : ℝ → ℝ} {x : ℝ} (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) :
deriv (fun (x : ℝ) => √(f x)) x = deriv f x / (2 * √(f x))
source
theorem HasFDerivAt.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : StrongDual ℝ E} (hf : HasFDerivAt f f' x) (hx : f x ≠ 0) :
HasFDerivAt (fun (y : E) => √(f y)) ((1 / (2 * √(f x))) • f') x
source
theorem HasStrictFDerivAt.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : StrongDual ℝ E} (hf : HasStrictFDerivAt f f' x) (hx : f x ≠ 0) :
HasStrictFDerivAt (fun (y : E) => √(f y)) ((1 / (2 * √(f x))) • f') x
source
theorem HasFDerivWithinAt.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E} {f' : StrongDual ℝ E} (hf : HasFDerivWithinAt f f' s x) (hx : f x ≠ 0) :
HasFDerivWithinAt (fun (y : E) => √(f y)) ((1 / (2 * √(f x))) • f') s x
source
theorem DifferentiableWithinAt.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E} (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0) :
DifferentiableWithinAt ℝ (fun (y : E) => √(f y)) s x
source
theorem DifferentiableAt.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) :
DifferentiableAt ℝ (fun (y : E) => √(f y)) x
source
theorem DifferentiableOn.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (hf : DifferentiableOn ℝ f s) (hs : ∀ x ∈ s, f x ≠ 0) :
DifferentiableOn ℝ (fun (y : E) => √(f y)) s
source
theorem Differentiable.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : Differentiable ℝ f) (hs : ∀ (x : E), f x ≠ 0) :
Differentiable ℝ fun (y : E) => √(f y)
source
theorem fderivWithin_sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E} (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0) (hxs : UniqueDiffWithinAt ℝ s x) :
fderivWithin ℝ (fun (x : E) => √(f x)) s x = (1 / (2 * √(f x))) • fderivWithin ℝ f s x
source
@[simp]
theorem fderiv_sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) :
fderiv ℝ (fun (x : E) => √(f x)) x = (1 / (2 * √(f x))) • fderiv ℝ f x
source
theorem ContDiffAt.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞} {x : E} (hf : ContDiffAt ℝ n f x) (hx : f x ≠ 0) :
ContDiffAt ℝ n (fun (y : E) => √(f y)) x
source
theorem ContDiffWithinAt.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞} {s : Set E} {x : E} (hf : ContDiffWithinAt ℝ n f s x) (hx : f x ≠ 0) :
ContDiffWithinAt ℝ n (fun (y : E) => √(f y)) s x
source
theorem ContDiffOn.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞} {s : Set E} (hf : ContDiffOn ℝ n f s) (hs : ∀ x ∈ s, f x ≠ 0) :
ContDiffOn ℝ n (fun (y : E) => √(f y)) s
source
theorem ContDiff.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞} (hf : ContDiff ℝ n f) (h : ∀ (x : E), f x ≠ 0) :
ContDiff ℝ n fun (y : E) => √(f y)