iteratedDeriv_exp_const_mul — Mathlib

English

For natural n and real c, the nth iterated derivative of s ↦ exp(c s) equals s ↦ c^n exp(c s).

Русский

Для натурального n и константы c производная n-го порядка функции s ↦ exp(c s) равняется s ↦ c^n exp(c s).

LaTeX

$$$$ \text{iteratedDeriv}(n, (s \mapsto \exp(c s))) = (s \mapsto c^n \exp(c s)) $$$$

Lean4

@[simp]
theorem iteratedDeriv_exp_const_mul (n : ℕ) (c : ℝ) :
    (iteratedDeriv n fun s => exp (c * s)) = fun s => c ^ n * exp (c * s) := by
  rw [iteratedDeriv_comp_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]

Похожие утверждения