Real derivatives of complexified real functions

Composing a real function f on a real normed space with the inclusion ℝ → ℂ does not change its real derivative: D(↑f)(x) v = ↑(Df(x) v). No differentiability is assumed, since both sides vanish when f is not differentiable at x.

Main results

• TauCeti.fderiv_ofReal_comp_apply: the real derivative of y ↦ (f y : ℂ) is the complexification of the real derivative of f.
• DifferentiableAt.ofReal_comp, TauCeti.norm_fderiv_ofReal_comp_le: y ↦ (f y : ℂ) is differentiable where f is, and its real derivative has norm at most ‖Df(x)‖.
• ContDiffAt.hasFDerivAt_fderiv_ofReal_comp_apply: at a C² point of f, the complexified directional derivative y ↦ D(↑f)(y) u has derivative w ↦ ↑(D²f(x)(w, u)).

@[simp]

theorem TauCeti.fderiv_ofReal_comp_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x v : E) : (fderiv ℝ (fun (y : E) => ↑(f y)) x) v = ↑((fderiv ℝ f x) v)

Composing a real function with the inclusion ℝ → ℂ does not change its real derivative. No differentiability is assumed: both sides vanish when f is not differentiable at x.

theorem DifferentiableAt.ofReal_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) : DifferentiableAt ℝ (fun (y : E) => ↑(f y)) x

A real function differentiable at x stays differentiable at x after composing with the inclusion ℝ → ℂ.

theorem TauCeti.norm_fderiv_ofReal_comp_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x : E) : ‖fderiv ℝ (fun (y : E) => ↑(f y)) x‖ ≤ ‖fderiv ℝ f x‖

The real derivative of y ↦ (f y : ℂ) has norm at most that of the real derivative of f.

theorem ContDiffAt.hasFDerivAt_fderiv_ofReal_comp_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) (u : E) : HasFDerivAt (fun (y : E) => (fderiv ℝ (fun (z : E) => ↑(f z)) y) u) (Complex.ofRealCLM ∘SL (fderiv ℝ (fderiv ℝ f) x).flip u) x

At a C² point of a real function f, the complexified directional derivative y ↦ D(↑f)(y) u has derivative w ↦ ↑(D²f(x)(w, u)).