mathlib documentation

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.

Differentiability of the restriction to of complex functions #

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.

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 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 times_cont_diff_at.real_of_complex {e : } {z : } {n : with_top } (h : times_cont_diff_at n e z) :
times_cont_diff_at n (λ (x : ), (e x).re) z
theorem times_cont_diff.real_of_complex {e : } {n : with_top } (h : times_cont_diff n e) :
times_cont_diff n (λ (x : ), (e x).re)