mathlib3 documentation

analysis.complex.real_deriv

Real differentiability of complex-differentiable functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Warning #

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

Differentiability of the restriction to ℝ of complex functions #

source
theorem has_strict_deriv_at.real_of_complex {e : ℂ → ℂ} {e' : ℂ} {z : ℝ} (h : has_strict_deriv_at e e' ↑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.

source
theorem has_deriv_at.real_of_complex {e : ℂ → ℂ} {e' : ℂ} {z : ℝ} (h : has_deriv_at e e' ↑z) :
has_deriv_at (λ (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.

source
theorem cont_diff_at.real_of_complex {e : ℂ → ℂ} {z : ℝ} {n : ℕ∞} (h : cont_diff_at ℂ n e ↑z) :
cont_diff_at ℝ n (λ (x : ℝ), (e ↑x).re) z
source
theorem cont_diff.real_of_complex {e : ℂ → ℂ} {n : ℕ∞} (h : cont_diff ℂ n e) :
cont_diff ℝ n (λ (x : ℝ), (e ↑x).re)
source
theorem has_strict_deriv_at.complex_to_real_fderiv' {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {f : ℂ → E} {x : ℂ} {f' : E} (h : has_strict_deriv_at f f' x) :
has_strict_fderiv_at f (complex.re_clm.smul_right f' + complex.I • complex.im_clm.smul_right f') x
source
theorem has_deriv_at.complex_to_real_fderiv' {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {f : ℂ → E} {x : ℂ} {f' : E} (h : has_deriv_at f f' x) :
has_fderiv_at f (complex.re_clm.smul_right f' + complex.I • complex.im_clm.smul_right f') x
source
theorem has_deriv_within_at.complex_to_real_fderiv' {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {f : ℂ → E} {s : set ℂ} {x : ℂ} {f' : E} (h : has_deriv_within_at f f' s x) :
has_fderiv_within_at f (complex.re_clm.smul_right f' + complex.I • complex.im_clm.smul_right f') s x
source
theorem has_strict_deriv_at.complex_to_real_fderiv {f : ℂ → ℂ} {f' x : ℂ} (h : has_strict_deriv_at f f' x) :
has_strict_fderiv_at f (f' • 1) x
source
theorem has_deriv_at.complex_to_real_fderiv {f : ℂ → ℂ} {f' x : ℂ} (h : has_deriv_at f f' x) :
has_fderiv_at f (f' • 1) x
source
theorem has_deriv_within_at.complex_to_real_fderiv {f : ℂ → ℂ} {s : set ℂ} {f' x : ℂ} (h : has_deriv_within_at f f' s x) :
has_fderiv_within_at f (f' • 1) s x
source
theorem has_deriv_at.comp_of_real {e : ℂ → ℂ} {e' : ℂ} {z : ℝ} (hf : has_deriv_at e e' ↑z) :
has_deriv_at (λ (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.

source
theorem has_deriv_at.of_real_comp {z : ℝ} {f : ℝ → ℝ} {u : ℝ} (hf : has_deriv_at f u z) :
has_deriv_at (λ (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 #

source
theorem differentiable_at.conformal_at {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {z : ℂ} {f : ℂ → E} (h : differentiable_at ℂ f z) (hf' : deriv f z ≠ 0) :
conformal_at f 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.

source
theorem conformal_at_iff_differentiable_at_or_differentiable_at_comp_conj {f : ℂ → ℂ} {z : ℂ} :
conformal_at f z ↔ (differentiable_at ℂ f z ∨ differentiable_at ℂ (f ∘ ⇑(star_ring_end ℂ)) (⇑(star_ring_end ℂ) z)) ∧ fderiv ℝ f z ≠ 0

A complex function is conformal if and only if the function is holomorphic or antiholomorphic with a nonvanishing differential.