# Documentation

Mathlib.Analysis.Complex.RealDeriv

# Real differentiability of complex-differentiable functions #

HasDerivAt.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 complex derivative.

DifferentiableAt.conformalAt 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.

conformalAt_iff_differentiableAt_or_differentiableAt_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.

## TODO #

• The classical form of Cauchy-Riemann equations
• On a connected open set u, a function which is ConformalAt each point is either holomorphic throughout or antiholomorphic throughout.

## Warning #

We do NOT require conformal functions to be orientation-preserving in this file.

### Differentiability of the restriction to ℝ of complex functions #

theorem HasStrictDerivAt.real_of_complex {e : } {e' : } {z : } (h : HasStrictDerivAt e e' z) :
HasStrictDerivAt (fun x => (e x).re) e'.re z

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.

theorem HasDerivAt.real_of_complex {e : } {e' : } {z : } (h : HasDerivAt e e' z) :
HasDerivAt (fun x => (e x).re) e'.re z

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.

theorem ContDiffAt.real_of_complex {e : } {z : } {n : ℕ∞} (h : ContDiffAt n e z) :
ContDiffAt n (fun x => (e x).re) z
theorem ContDiff.real_of_complex {e : } {n : ℕ∞} (h : ) :
ContDiff n fun x => (e x).re
theorem HasStrictDerivAt.complexToReal_fderiv' {E : Type u_1} [] {f : E} {x : } {f' : E} (h : HasStrictDerivAt f f' x) :
theorem HasDerivAt.complexToReal_fderiv' {E : Type u_1} [] {f : E} {x : } {f' : E} (h : HasDerivAt f f' x) :
theorem HasDerivWithinAt.complexToReal_fderiv' {E : Type u_1} [] {f : E} {s : } {x : } {f' : E} (h : HasDerivWithinAt f f' s x) :
theorem HasStrictDerivAt.complexToReal_fderiv {f : } {f' : } {x : } (h : HasStrictDerivAt f f' x) :
theorem HasDerivAt.complexToReal_fderiv {f : } {f' : } {x : } (h : HasDerivAt f f' x) :
HasFDerivAt f (f' 1) x
theorem HasDerivWithinAt.complexToReal_fderiv {f : } {s : } {f' : } {x : } (h : HasDerivWithinAt f f' s x) :
HasFDerivWithinAt f (f' 1) s x
theorem HasDerivAt.comp_ofReal {e : } {e' : } {z : } (hf : HasDerivAt e e' z) :
HasDerivAt (fun y => e y) e' z

If a complex function e is differentiable at a real point, then its restriction to ℝ is differentiable there as a function ℝ → ℂ, with the same derivative.

theorem HasDerivAt.ofReal_comp {z : } {f : } {u : } (hf : HasDerivAt f u z) :
HasDerivAt (fun y => ↑(f y)) (u) z

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 #

theorem DifferentiableAt.conformalAt {E : Type u_1} [] {z : } {f : E} (h : ) (hf' : deriv f z 0) :

A real differentiable function of the complex plane into some complex normed space E is 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.