diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean index d5b71e5b13fbb..06459fd66c93f 100644 --- a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean +++ b/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 diff --git a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean index c3b7fc9070809..3458cfd0e5c67 100644 --- a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean +++ b/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]