Complex.hasStrictFDerivAt_log_real
theorem Complex.hasStrictFDerivAt_log_real :
∀ {x : ℂ}, x ∈ Complex.slitPlane → HasStrictFDerivAt Complex.log (x⁻¹ • 1) x
This theorem states that for every complex number 'x' belonging to the slit plane (the complex plane with the closed negative real axis removed), the complex logarithm function has a strict derivative at 'x'. The derivative of the complex logarithm at 'x' is given by `1/x`. In other words, this theorem is establishing the derivative of the logarithm function in the context of complex analysis, assuming the input is within the slit complex plane.
More concisely: The complex logarithm function has a strict derivative equal to `1/x` at every complex number 'x' in the slit complex plane.
|
Complex.hasStrictDerivAt_log
theorem Complex.hasStrictDerivAt_log : ∀ {x : ℂ}, x ∈ Complex.slitPlane → HasStrictDerivAt Complex.log x⁻¹ x
The theorem `Complex.hasStrictDerivAt_log` states that for all complex numbers `x` that belong to the slit complex plane (which is the complex plane with the closed negative real axis removed), the function `Complex.log` (which is the complex logarithm function) has a strict derivative at `x` which is equal to the reciprocal of `x`. The strict derivative means that the difference between the function values at two points approaches the product of the difference between the points and the derivative, plus an infinitely small error, as the two points approach each other. In mathematical terms, this is equivalent to saying that, for all `x` in the slit complex plane, the logarithm function `log` is strictly differentiable at `x` with derivative `1/x`.
More concisely: For complex numbers `x` in the slit complex plane, the complex logarithm function `log` is strictly differentiable with derivative `1/x`.
|