Derivatives of Complex.sqrt

This file proves that Complex.sqrt is differentiable on the slit plane Complex.slitPlane and computes its derivative.

Main results

• Complex.hasDerivAt_sqrt: the derivative of Complex.sqrt at z ∈ slitPlane is z ^ (-1 / 2 : ℂ) / 2.
• Complex.differentiableOn_sqrt: Complex.sqrt is differentiable on slitPlane.
• Complex.deriv_sqrt: the derivative equals z ^ (-1 / 2 : ℂ) / 2.

theorem Complex.hasStrictDerivAt_sqrt {z : ℂ} (hz : z ∈ slitPlane) : HasStrictDerivAt sqrt (z ^ (-1 / 2) / 2) z

theorem Complex.hasDerivAt_sqrt {z : ℂ} (hz : z ∈ slitPlane) : HasDerivAt sqrt (z ^ (-1 / 2) / 2) z

theorem Complex.hasDerivWithinAt_sqrt {z : ℂ} {s : Set ℂ} (hz : z ∈ slitPlane) : HasDerivWithinAt sqrt (z ^ (-1 / 2) / 2) s z

theorem Complex.differentiableAt_sqrt {z : ℂ} (hz : z ∈ slitPlane) : DifferentiableAt ℂ sqrt z

theorem Complex.differentiableWithinAt_sqrt {z : ℂ} {s : Set ℂ} (hz : z ∈ slitPlane) : DifferentiableWithinAt ℂ sqrt s z

theorem Complex.differentiableOn_sqrt : DifferentiableOn ℂ sqrt slitPlane

theorem Complex.deriv_sqrt {z : ℂ} (hz : z ∈ slitPlane) : deriv sqrt z = z ^ (-1 / 2) / 2

theorem Complex.derivWithin_sqrt {z : ℂ} (hz : z ∈ slitPlane) : derivWithin sqrt slitPlane z = z ^ (-1 / 2) / 2

theorem Complex.continuousAt_sqrt {z : ℂ} (hz : 0 ≤ z.re ∨ z.im ≠ 0) : ContinuousAt sqrt z

Complex.sqrt is continuous at z provided 0 ≤ z.re or z.im ≠ 0. This is weaker than requiring z ∈ slitPlane, as it additionally includes the imaginary axis and 0.

theorem Complex.continuousOn_sqrt : ContinuousOn sqrt slitPlane