Derivatives of exponential functions

Viewed as a function of a real vector variable, Complex.exp has the same iterated derivatives as it has over ℂ, restricted to real scalars. Since every complex derivative of exp is exp, every real iterated derivative of Complex.exp at z has norm ‖exp z‖. This is the input a Faà di Bruno bound needs for compositions Complex.exp ∘ f with a real-differentiable f.

Main results

• TauCeti.norm_iteratedFDeriv_real_cexp: every real iterated derivative of Complex.exp at z has norm ‖exp z‖.
• ContinuousLinearMap.norm_iteratedFDeriv_cexp_comp_le: for a real-linear map ℓ to ℂ, the n-th derivative of x ↦ exp (ℓ x) has norm at most ‖exp (ℓ x)‖ ‖ℓ‖ ^ n.

@[simp]

theorem Real.deriv_exp_mul (a x : ℝ) : deriv (fun (y : ℝ) => exp (a * y)) x = a * exp (a * x)

The derivative of an exponential with linear exponent.

@[simp]

theorem Real.norm_fderiv_exp_mul (a x : ℝ) : ‖fderiv ℝ (fun (y : ℝ) => exp (a * y)) x‖ = |a| * exp (a * x)

The norm of the Fréchet derivative of an exponential with linear exponent.

theorem TauCeti.norm_iteratedFDeriv_real_cexp (n : ℕ) (z : ℂ) : ‖iteratedFDeriv ℝ n Complex.exp z‖ = ‖Complex.exp z‖

Every real iterated derivative of the complex exponential at z has norm ‖exp z‖.

theorem ContinuousLinearMap.norm_iteratedFDeriv_cexp_comp_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ℓ : E →L[ℝ] ℂ) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (fun (y : E) => Complex.exp (ℓ y)) x‖ ≤ ‖Complex.exp (ℓ x)‖ * ‖ℓ‖ ^ n

For a real-linear map ℓ : E →L[ℝ] ℂ, the n-th derivative of x ↦ exp (ℓ x) has norm at most ‖exp (ℓ x)‖ ‖ℓ‖ ^ n. For a purely imaginary ℓ, such as the phase x ↦ 2πi ⟪x, w⟫ of a character, this is ‖ℓ‖ ^ n.