# 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.sqPartialHomeomorph :

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
theorem Real.deriv_sqrt_aux {x : } (hx : x 0) :
HasStrictDerivAt (fun (x : ) => x) (1 / (2 * x)) x ∀ (n : ℕ∞), ContDiffAt n (fun (x : ) => x) x
theorem Real.hasStrictDerivAt_sqrt {x : } (hx : x 0) :
HasStrictDerivAt (fun (x : ) => x) (1 / (2 * x)) x
theorem Real.contDiffAt_sqrt {x : } {n : ℕ∞} (hx : x 0) :
ContDiffAt n (fun (x : ) => x) x
theorem Real.hasDerivAt_sqrt {x : } (hx : x 0) :
HasDerivAt (fun (x : ) => x) (1 / (2 * x)) x
theorem HasDerivWithinAt.sqrt {f : } {s : } {f' : } {x : } (hf : HasDerivWithinAt f f' s x) (hx : f x 0) :
HasDerivWithinAt (fun (y : ) => (f y)) (f' / (2 * (f x))) s x
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
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
theorem derivWithin_sqrt {f : } {s : } {x : } (hf : ) (hx : f x 0) (hxs : ) :
derivWithin (fun (x : ) => (f x)) s x = derivWithin f s x / (2 * (f x))
@[simp]
theorem deriv_sqrt {f : } {x : } (hf : ) (hx : f x 0) :
deriv (fun (x : ) => (f x)) x = deriv f x / (2 * (f x))
theorem HasFDerivAt.sqrt {E : Type u_1} [] {f : E} {x : E} {f' : } (hf : HasFDerivAt f f' x) (hx : f x 0) :
HasFDerivAt (fun (y : E) => (f y)) ((1 / (2 * (f x))) f') x
theorem HasStrictFDerivAt.sqrt {E : Type u_1} [] {f : E} {x : E} {f' : } (hf : ) (hx : f x 0) :
HasStrictFDerivAt (fun (y : E) => (f y)) ((1 / (2 * (f x))) f') x
theorem HasFDerivWithinAt.sqrt {E : Type u_1} [] {f : E} {s : Set E} {x : E} {f' : } (hf : HasFDerivWithinAt f f' s x) (hx : f x 0) :
HasFDerivWithinAt (fun (y : E) => (f y)) ((1 / (2 * (f x))) f') s x
theorem DifferentiableWithinAt.sqrt {E : Type u_1} [] {f : E} {s : Set E} {x : E} (hf : ) (hx : f x 0) :
DifferentiableWithinAt (fun (y : E) => (f y)) s x
theorem DifferentiableAt.sqrt {E : Type u_1} [] {f : E} {x : E} (hf : ) (hx : f x 0) :
DifferentiableAt (fun (y : E) => (f y)) x
theorem DifferentiableOn.sqrt {E : Type u_1} [] {f : E} {s : Set E} (hf : ) (hs : xs, f x 0) :
DifferentiableOn (fun (y : E) => (f y)) s
theorem Differentiable.sqrt {E : Type u_1} [] {f : E} (hf : ) (hs : ∀ (x : E), f x 0) :
Differentiable fun (y : E) => (f y)
theorem fderivWithin_sqrt {E : Type u_1} [] {f : E} {s : Set E} {x : E} (hf : ) (hx : f x 0) (hxs : ) :
fderivWithin (fun (x : E) => (f x)) s x = (1 / (2 * (f x)))
@[simp]
theorem fderiv_sqrt {E : Type u_1} [] {f : E} {x : E} (hf : ) (hx : f x 0) :
fderiv (fun (x : E) => (f x)) x = (1 / (2 * (f x))) fderiv f x
theorem ContDiffAt.sqrt {E : Type u_1} [] {f : E} {n : ℕ∞} {x : E} (hf : ContDiffAt n f x) (hx : f x 0) :
ContDiffAt n (fun (y : E) => (f y)) x
theorem ContDiffWithinAt.sqrt {E : Type u_1} [] {f : E} {n : ℕ∞} {s : Set E} {x : E} (hf : ) (hx : f x 0) :
ContDiffWithinAt n (fun (y : E) => (f y)) s x
theorem ContDiffOn.sqrt {E : Type u_1} [] {f : E} {n : ℕ∞} {s : Set E} (hf : ContDiffOn n f s) (hs : xs, f x 0) :
ContDiffOn n (fun (y : E) => (f y)) s
theorem ContDiff.sqrt {E : Type u_1} [] {f : E} {n : ℕ∞} (hf : ) (h : ∀ (x : E), f x 0) :
ContDiff n fun (y : E) => (f y)