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.

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 : WithTop ℕ∞} (h : ContDiffAt ℂ n e ↑z) : ContDiffAt ℝ n (fun (x : ℝ) => (e ↑x).re) z

theorem ContDiff.real_of_complex {e : ℂ → ℂ} {n : WithTop ℕ∞} (h : ContDiff ℂ n e) : ContDiff ℝ n fun (x : ℝ) => (e ↑x).re

theorem HasStrictDerivAt.complexToReal_fderiv' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {f' : E} (h : HasStrictDerivAt f f' x) : HasStrictFDerivAt f (Complex.reCLM.smulRight f' + Complex.I • Complex.imCLM.smulRight f') x

theorem HasDerivAt.complexToReal_fderiv' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {f' : E} (h : HasDerivAt f f' x) : HasFDerivAt f (Complex.reCLM.smulRight f' + Complex.I • Complex.imCLM.smulRight f') x

theorem HasDerivWithinAt.complexToReal_fderiv' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {s : Set ℂ} {x : ℂ} {f' : E} (h : HasDerivWithinAt f f' s x) : HasFDerivWithinAt f (Complex.reCLM.smulRight f' + Complex.I • Complex.imCLM.smulRight f') s x

theorem HasStrictDerivAt.complexToReal_fderiv {f : ℂ → ℂ} {f' x : ℂ} (h : HasStrictDerivAt f f' x) : HasStrictFDerivAt f (f' • 1) x

theorem HasDerivAt.complexToReal_fderiv {f : ℂ → ℂ} {f' x : ℂ} (h : HasDerivAt f f' x) : HasFDerivAt f (f' • 1) x

theorem HasDerivWithinAt.complexToReal_fderiv {f : ℂ → ℂ} {s : Set ℂ} {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 ℝ → ℂ.