Real differentiability of complex-differentiable functions #
has_deriv_at.real_of_complex expresses that, if a function on
ℂ is differentiable (over
then its restriction to
ℝ is differentiable over
ℝ, with derivative the real part of the
differentiable_at.conformal_at states that a real-differentiable function with a nonvanishing
differential from the complex plane into an arbitrary complex-normed space is conformal at a point
if it's holomorphic at that point. This is a version of Cauchy-Riemann equations.
conformal_at_iff_differentiable_at_or_differentiable_at_comp_conj proves that a real-differential
function with a nonvanishing differential between the complex plane is conformal at a point if and
only if it's holomorphic or antiholomorphic at that point.
- The classical form of Cauchy-Riemann equations
- On a connected open set
u, a function which is
conformal_ateach point is either holomorphic throughout or antiholomorphic throughout.
We do NOT require conformal functions to be orientation-preserving in this file.
Differentiability of the restriction to
ℝ of complex functions #
If a complex function is differentiable at a real point, then the induced real function is also differentiable at this point, with a derivative equal to the real part of the complex derivative.
If a complex function
e is differentiable at a real point, then the function
ℝ → ℝ given by
the real part of
e is also differentiable at this point, with a derivative equal to the real part
of the complex derivative.
If a complex function
e is differentiable at a real point, then its restriction to
differentiable there as a function
ℝ → ℂ, with the same derivative.
If a function
f : ℝ → ℝ is differentiable at a (real) point
x, then it is also
differentiable as a function
ℝ → ℂ.
Conformality of real-differentiable complex maps #
A real differentiable function of the complex plane into some complex normed space
conformal at a point
z if it is holomorphic at that point with a nonvanishing differential.
This is a version of the Cauchy-Riemann equations.
A complex function is conformal if and only if the function is holomorphic or antiholomorphic with a nonvanishing differential.