From 83303bba748946d2ed7a4fe1bc6234fa3603fcc9 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sun, 14 Jan 2024 22:59:12 +0100 Subject: [PATCH 1/6] feat: iteratedDeriv_{c,}exp_const_mul The only added import is Mathlib.Analysis.Calculus.IteratedDeriv itself; its dependencies are already imported. Co-authored-by: Chris Birkbeck --- .../Analysis/SpecialFunctions/ExpDeriv.lean | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean index c3b7fc9070809..e45f6261b5417 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 #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,20 @@ theorem ContDiffWithinAt.cexp {n} (hf : ContDiffWithinAt π•œ n f s x) : end +theorem iteratedDeriv_cexp_const_mul (n : β„•) (c : β„‚) : + (iteratedDeriv n fun s : β„‚ => Complex.exp (c * s)) = fun s => c ^ n * Complex.exp (c * s) := by + induction n with + | zero => simp + | succ n ih => + funext x + rw [pow_succ, iteratedDeriv_succ, ih, deriv_const_mul_field, + deriv_cexp (differentiableAt_id'.const_mul _), deriv_const_mul _ differentiableAt_id', + deriv_id''] + ring + + +/-! ## `Real.exp` -/ + namespace Real variable {x y z : ℝ} @@ -319,3 +336,14 @@ theorem fderiv_exp (hc : DifferentiableAt ℝ f x) : #align fderiv_exp fderiv_exp end + +theorem iteratedDeriv_exp_const_mul (n : β„•) (c : ℝ) : + (iteratedDeriv n fun s => Real.exp (c * s)) = fun s => c ^ n * Real.exp (c * s) := by + induction n with + | zero => simp + | succ n ih => + funext x + rw [pow_succ, iteratedDeriv_succ, ih, deriv_const_mul_field, + deriv_exp (differentiableAt_id'.const_mul _), deriv_const_mul _ differentiableAt_id', + deriv_id''] + ring From a0bec2823e51781d7c6c0cbe3e12d95d9afe6c6f Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 16 Jan 2024 22:21:10 +0100 Subject: [PATCH 2/6] Generalize --- Mathlib/Analysis/Calculus/IteratedDeriv.lean | 22 +++++++++++++++++ .../Analysis/SpecialFunctions/ExpDeriv.lean | 24 +++++-------------- 2 files changed, 28 insertions(+), 18 deletions(-) diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv.lean b/Mathlib/Analysis/Calculus/IteratedDeriv.lean index 8c9de9cb4df2c..e60ed8a35ccf2 100644 --- a/Mathlib/Analysis/Calculus/IteratedDeriv.lean +++ b/Mathlib/Analysis/Calculus/IteratedDeriv.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: SΓ©bastien GouΓ«zel -/ import Mathlib.Analysis.Calculus.Deriv.Comp +import Mathlib.Analysis.Calculus.Deriv.Mul import Mathlib.Analysis.Calculus.ContDiff.Defs #align_import analysis.calculus.iterated_deriv from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe" @@ -304,3 +305,24 @@ derivative. -/ theorem iteratedDeriv_succ' : iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f) := by rw [iteratedDeriv_eq_iterate, iteratedDeriv_eq_iterate]; rfl #align iterated_deriv_succ' iteratedDeriv_succ' + +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 e45f6261b5417..1771e77481250 100644 --- a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean @@ -177,16 +177,10 @@ theorem ContDiffWithinAt.cexp {n} (hf : ContDiffWithinAt π•œ n f s x) : end +open Complex in theorem iteratedDeriv_cexp_const_mul (n : β„•) (c : β„‚) : - (iteratedDeriv n fun s : β„‚ => Complex.exp (c * s)) = fun s => c ^ n * Complex.exp (c * s) := by - induction n with - | zero => simp - | succ n ih => - funext x - rw [pow_succ, iteratedDeriv_succ, ih, deriv_const_mul_field, - deriv_cexp (differentiableAt_id'.const_mul _), deriv_const_mul _ differentiableAt_id', - deriv_id''] - ring + (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` -/ @@ -337,13 +331,7 @@ theorem fderiv_exp (hc : DifferentiableAt ℝ f x) : end +open Real in theorem iteratedDeriv_exp_const_mul (n : β„•) (c : ℝ) : - (iteratedDeriv n fun s => Real.exp (c * s)) = fun s => c ^ n * Real.exp (c * s) := by - induction n with - | zero => simp - | succ n ih => - funext x - rw [pow_succ, iteratedDeriv_succ, ih, deriv_const_mul_field, - deriv_exp (differentiableAt_id'.const_mul _), deriv_const_mul _ differentiableAt_id', - deriv_id''] - ring + (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] From 304870d84e5247dc4d3897b91fa4a9e1d5e611fa Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri, 19 Jan 2024 20:48:40 +0100 Subject: [PATCH 3/6] fix --- Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean index 1771e77481250..e466e931693f7 100644 --- a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean @@ -5,7 +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 +import Mathlib.Analysis.Calculus.IteratedDeriv.Basic #align_import analysis.special_functions.exp_deriv from "leanprover-community/mathlib"@"6a5c85000ab93fe5dcfdf620676f614ba8e18c26" From 2d7f139fae06abea4bb6eb92b04d612c18f6137f Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri, 19 Jan 2024 21:20:10 +0100 Subject: [PATCH 4/6] fix --- Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean index e466e931693f7..53a5df2245875 100644 --- a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean @@ -5,7 +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.Basic +import Mathlib.Analysis.Calculus.IteratedDeriv.Defs #align_import analysis.special_functions.exp_deriv from "leanprover-community/mathlib"@"6a5c85000ab93fe5dcfdf620676f614ba8e18c26" From d2d41109085a578cdb21c84171043dcbc78ef955 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri, 19 Jan 2024 21:29:56 +0100 Subject: [PATCH 5/6] move --- .../Analysis/Calculus/IteratedDeriv/Defs.lean | 22 ------------------ .../Calculus/IteratedDeriv/Lemmas.lean | 23 +++++++++++++++++++ .../Analysis/SpecialFunctions/ExpDeriv.lean | 2 +- 3 files changed, 24 insertions(+), 23 deletions(-) diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean index cb59fcc5855e2..9acf9125275c4 100644 --- a/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean +++ b/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: SΓ©bastien GouΓ«zel -/ import Mathlib.Analysis.Calculus.Deriv.Basic -import Mathlib.Analysis.Calculus.Deriv.Mul import Mathlib.Analysis.Calculus.ContDiff.Defs #align_import analysis.calculus.iterated_deriv from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe" @@ -305,24 +304,3 @@ derivative. -/ theorem iteratedDeriv_succ' : iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f) := by rw [iteratedDeriv_eq_iterate, iteratedDeriv_eq_iterate]; rfl #align iterated_deriv_succ' iteratedDeriv_succ' - -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/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 53a5df2245875..6974918eb904a 100644 --- a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean @@ -5,7 +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.Defs +import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas #align_import analysis.special_functions.exp_deriv from "leanprover-community/mathlib"@"6a5c85000ab93fe5dcfdf620676f614ba8e18c26" From d92a73afd43f2ab59741e3208063e4c9cf8a858a Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri, 26 Jan 2024 19:18:55 +0100 Subject: [PATCH 6/6] Apply suggestions from code review Co-authored-by: Jireh Loreaux --- Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean index 6974918eb904a..3458cfd0e5c67 100644 --- a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean @@ -178,6 +178,7 @@ 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] @@ -332,6 +333,7 @@ theorem fderiv_exp (hc : DifferentiableAt ℝ f x) : 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]