Documentation

Mathlib.Analysis.SpecialFunctions.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

source
noncomputable def Real.sqPartialHomeomorph :
PartialHomeomorph ℝ ℝ

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.sqrt) (1 / (2 * x.sqrt)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n (fun (x : ℝ) => x.sqrt) x
    source
    theorem Real.hasStrictDerivAt_sqrt {x : ℝ} (hx : x ≠ 0) :
    HasStrictDerivAt (fun (x : ℝ) => x.sqrt) (1 / (2 * x.sqrt)) x
    source
    theorem Real.contDiffAt_sqrt {x : ℝ} {n : ℕ∞} (hx : x ≠ 0) :
    ContDiffAt ℝ n (fun (x : ℝ) => x.sqrt) x
    source
    theorem Real.hasDerivAt_sqrt {x : ℝ} (hx : x ≠ 0) :
    HasDerivAt (fun (x : ℝ) => x.sqrt) (1 / (2 * x.sqrt)) 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).sqrt) (f' / (2 * (f x).sqrt)) s x
    source
    theorem HasDerivAt.sqrt {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (hf : HasDerivAt f f' x) (hx : f x ≠ 0) :
    HasDerivAt (fun (y : ℝ) => (f y).sqrt) (f' / (2 * (f x).sqrt)) x
    source
    theorem HasStrictDerivAt.sqrt {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (hf : HasStrictDerivAt f f' x) (hx : f x ≠ 0) :
    HasStrictDerivAt (fun (t : ℝ) => (f t).sqrt) (f' / (2 * (f x).sqrt)) 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).sqrt) s x = derivWithin f s x / (2 * (f x).sqrt)
    source
    @[simp]
    theorem deriv_sqrt {f : ℝ → ℝ} {x : ℝ} (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) :
    deriv (fun (x : ℝ) => (f x).sqrt) x = deriv f x / (2 * (f x).sqrt)
    source
    theorem HasFDerivAt.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : E →L[ℝ] ℝ} (hf : HasFDerivAt f f' x) (hx : f x ≠ 0) :
    HasFDerivAt (fun (y : E) => (f y).sqrt) ((1 / (2 * (f x).sqrt)) • f') x
    source
    theorem HasStrictFDerivAt.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : E →L[ℝ] ℝ} (hf : HasStrictFDerivAt f f' x) (hx : f x ≠ 0) :
    HasStrictFDerivAt (fun (y : E) => (f y).sqrt) ((1 / (2 * (f x).sqrt)) • f') x
    source
    theorem HasFDerivWithinAt.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E} {f' : E →L[ℝ] ℝ} (hf : HasFDerivWithinAt f f' s x) (hx : f x ≠ 0) :
    HasFDerivWithinAt (fun (y : E) => (f y).sqrt) ((1 / (2 * (f x).sqrt)) • 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).sqrt) 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).sqrt) 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).sqrt) 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).sqrt
    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).sqrt) s x = (1 / (2 * (f x).sqrt)) • 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).sqrt) x = (1 / (2 * (f x).sqrt)) • fderiv ℝ f x
    source
    theorem ContDiffAt.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞} {x : E} (hf : ContDiffAt ℝ n f x) (hx : f x ≠ 0) :
    ContDiffAt ℝ n (fun (y : E) => (f y).sqrt) x
    source
    theorem ContDiffWithinAt.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞} {s : Set E} {x : E} (hf : ContDiffWithinAt ℝ n f s x) (hx : f x ≠ 0) :
    ContDiffWithinAt ℝ n (fun (y : E) => (f y).sqrt) s x
    source
    theorem ContDiffOn.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞} {s : Set E} (hf : ContDiffOn ℝ n f s) (hs : ∀ x ∈ s, f x ≠ 0) :
    ContDiffOn ℝ n (fun (y : E) => (f y).sqrt) s
    source
    theorem ContDiff.sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞} (hf : ContDiff ℝ n f) (h : ∀ (x : E), f x ≠ 0) :
    ContDiff ℝ n fun (y : E) => (f y).sqrt