[Merged by Bors] - feat: iteratedDeriv_const_{s,}mul, iteratedDeriv_{c,}exp_const_mul

Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean

@@ -5,6 +5,8 @@ Authors: Chris Birkbeck, Ruben Van de Velde
 -/
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.Analysis.Calculus.Deriv.Add
+import Mathlib.Analysis.Calculus.Deriv.Comp
+import Mathlib.Analysis.Calculus.Deriv.Mul
 import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
 
 /-!
@@ -78,3 +80,24 @@ theorem iteratedDerivWithin_sub (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 
       iteratedDerivWithin n f s x - iteratedDerivWithin n g s x := by
   rw [sub_eq_add_neg, sub_eq_add_neg, Pi.neg_def, iteratedDerivWithin_add hx h hf hg.neg,
     iteratedDerivWithin_neg' hx h hg]
+
+theorem iteratedDeriv_const_smul {n : ℕ} {f : 𝕜 → F} (h : ContDiff 𝕜 n f) (c : 𝕜) :
+    iteratedDeriv n (fun x => f (c * x)) = fun x => c ^ n • iteratedDeriv n f (c * x) := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    funext x
+    have h₀ : DifferentiableAt 𝕜 (iteratedDeriv n f) (c * x) :=
+      h.differentiable_iteratedDeriv n (Nat.cast_lt.mpr n.lt_succ_self) |>.differentiableAt
+    have h₁ : DifferentiableAt 𝕜 (fun x => iteratedDeriv n f (c * x)) x := by
+      rw [← Function.comp_def]
+      apply DifferentiableAt.comp
+      · exact h.differentiable_iteratedDeriv n (Nat.cast_lt.mpr n.lt_succ_self) |>.differentiableAt
+      · exact differentiableAt_id'.const_mul _
+    rw [iteratedDeriv_succ, ih h.of_succ, deriv_const_smul _ h₁, iteratedDeriv_succ,
+      ← Function.comp_def, deriv.scomp x h₀ (differentiableAt_id'.const_mul _),
+      deriv_const_mul _ differentiableAt_id', deriv_id'', smul_smul, mul_one, pow_succ']
+
+theorem iteratedDeriv_const_mul {n : ℕ} {f : 𝕜 → 𝕜} (h : ContDiff 𝕜 n f) (c : 𝕜) :
+    iteratedDeriv n (fun x => f (c * x)) = fun x => c ^ n * iteratedDeriv n f (c * x) := by
+  simpa only [smul_eq_mul] using iteratedDeriv_const_smul h c

Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean

@@ -5,6 +5,7 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne
 -/
 import Mathlib.Analysis.Complex.RealDeriv
 import Mathlib.Analysis.Calculus.ContDiff.IsROrC
+import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
 
 #align_import analysis.special_functions.exp_deriv from "leanprover-community/mathlib"@"6a5c85000ab93fe5dcfdf620676f614ba8e18c26"
 
@@ -25,6 +26,8 @@ open Filter Asymptotics Set Function
 
 open scoped Classical Topology
 
+/-! ## `Complex.exp` -/
+
 namespace Complex
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 ℂ]
@@ -174,6 +177,15 @@ theorem ContDiffWithinAt.cexp {n} (hf : ContDiffWithinAt 𝕜 n f s x) :
 
 end
 
+open Complex in
+@[simp]
+theorem iteratedDeriv_cexp_const_mul (n : ℕ) (c : ℂ) :
+    (iteratedDeriv n fun s : ℂ => exp (c * s)) = fun s => c ^ n * exp (c * s) := by
+  rw [iteratedDeriv_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]
+
+
+/-! ## `Real.exp` -/
+
 namespace Real
 
 variable {x y z : ℝ}
@@ -319,3 +331,9 @@ theorem fderiv_exp (hc : DifferentiableAt ℝ f x) :
 #align fderiv_exp fderiv_exp
 
 end
+
+open Real in
+@[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_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]