# mathlibdocumentation

analysis.complex.real_deriv

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

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.

## TODO #

• The classical form of Cauchy-Riemann equations
• On a connected open set u, a function which is conformal_at 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 has_strict_deriv_at.real_of_complex {e : } {e' : } {z : } (h : z) :
has_strict_deriv_at (λ (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 has_deriv_at.real_of_complex {e : } {e' : } {z : } (h : e' z) :
has_deriv_at (λ (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 cont_diff_at.real_of_complex {e : } {z : } {n : with_top } (h : e z) :
(λ (x : ), (e x).re) z
theorem cont_diff.real_of_complex {e : } {n : with_top } (h : e) :
(λ (x : ), (e x).re)
theorem has_strict_deriv_at.complex_to_real_fderiv' {E : Type u_1} [normed_group E] [ E] {f : → E} {x : } {f' : E} (h : x) :
theorem has_deriv_at.complex_to_real_fderiv' {E : Type u_1} [normed_group E] [ E] {f : → E} {x : } {f' : E} (h : f' x) :
x
theorem has_deriv_within_at.complex_to_real_fderiv' {E : Type u_1} [normed_group E] [ E] {f : → E} {s : set } {x : } {f' : E} (h : s x) :
x
theorem has_strict_deriv_at.complex_to_real_fderiv {f : } {f' x : } (h : x) :
(f' 1) x
theorem has_deriv_at.complex_to_real_fderiv {f : } {f' x : } (h : f' x) :
(f' 1) x
theorem has_deriv_within_at.complex_to_real_fderiv {f : } {s : set } {f' x : } (h : s x) :
(f' 1) s x

### Conformality of real-differentiable complex maps #

theorem differentiable_at.conformal_at {E : Type u_1} [normed_group E] [ E] {z : } {f : → E} (h : z) (hf' : z 0) :
z

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.