From cdb43dd45063eb7434ccd48d8e1bbe857eab83b3 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Wed, 6 Mar 2024 11:04:40 +0000 Subject: [PATCH] feat(Analysis/Calculus/{Iterated}Deriv/*): add lemmas on composition with negation (#11173) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This adds ```lean lemma deriv_comp_neg (f : π•œ β†’ F) (a : π•œ) : deriv (fun x ↦ f (-x)) a = -deriv f (-a) /-- A variant of `deriv_const_smul` without differentiability assumption when the scalar multiplication is by field elements. -/ lemma deriv_const_smul' {f : π•œ β†’ F} {x : π•œ} {R : Type*} [Field R] [Module R F] [SMulCommClass π•œ R F] [ContinuousConstSMul R F] (c : R) : deriv (fun y ↦ c β€’ f y) x = c β€’ deriv f x lemma iteratedDeriv_neg (n : β„•) (f : π•œ β†’ F) (a : π•œ) : iteratedDeriv n (fun x ↦ -(f x)) a = -(iteratedDeriv n f a) lemma iteratedDeriv_comp_neg (n : β„•) (f : π•œ β†’ F) (a : π•œ) : iteratedDeriv n (fun x ↦ f (-x)) a = (-1 : π•œ) ^ n β€’ iteratedDeriv n f (-a) ``` which will come in handy in some future PRs on L-series. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837) on Zulip. --- Mathlib/Analysis/Calculus/Deriv/Add.lean | 7 +++++++ Mathlib/Analysis/Calculus/Deriv/Mul.lean | 16 +++++++++++++++ Mathlib/Analysis/Calculus/Deriv/Shift.lean | 8 ++++++++ .../Calculus/IteratedDeriv/Lemmas.lean | 20 +++++++++++++++++-- 4 files changed, 49 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Calculus/Deriv/Add.lean b/Mathlib/Analysis/Calculus/Deriv/Add.lean index 5fce50e52a0c4..e83a66c8dcfe8 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Add.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Add.lean @@ -292,6 +292,13 @@ theorem not_differentiableAt_abs_zero : Β¬ DifferentiableAt ℝ (abs : ℝ β†’ (hasDerivWithinAt_neg _ _).congr_of_mem (fun _ h ↦ abs_of_nonpos h) Set.right_mem_Iic linarith +lemma differentiableAt_comp_neg_iff {a : π•œ} : + DifferentiableAt π•œ f (-a) ↔ DifferentiableAt π•œ (fun x ↦ f (-x)) a := by + refine ⟨fun H ↦ H.comp a differentiable_neg.differentiableAt, fun H ↦ ?_⟩ + convert ((neg_neg a).symm β–Έ H).comp (-a) differentiable_neg.differentiableAt + ext + simp only [Function.comp_apply, neg_neg] + end Neg2 section Sub diff --git a/Mathlib/Analysis/Calculus/Deriv/Mul.lean b/Mathlib/Analysis/Calculus/Deriv/Mul.lean index 699bad64518d3..258e6d6e1f0ad 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Mul.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Mul.lean @@ -150,6 +150,22 @@ theorem deriv_const_smul (c : R) (hf : DifferentiableAt π•œ f x) : (hf.hasDerivAt.const_smul c).deriv #align deriv_const_smul deriv_const_smul +/-- A variant of `deriv_const_smul` without differentiability assumption when the scalar +multiplication is by field elements. -/ +lemma deriv_const_smul' {f : π•œ β†’ F} {x : π•œ} {R : Type*} [Field R] [Module R F] [SMulCommClass π•œ R F] + [ContinuousConstSMul R F] (c : R) : + deriv (fun y ↦ c β€’ f y) x = c β€’ deriv f x := by + by_cases hf : DifferentiableAt π•œ f x + Β· exact deriv_const_smul c hf + Β· rcases eq_or_ne c 0 with rfl | hc + Β· simp only [zero_smul, deriv_const'] + Β· have H : Β¬DifferentiableAt π•œ (fun y ↦ c β€’ f y) x := by + contrapose! hf + change DifferentiableAt π•œ (fun y ↦ f y) x + conv => enter [2, y]; rw [← inv_smul_smulβ‚€ hc (f y)] + exact DifferentiableAt.const_smul hf c⁻¹ + rw [deriv_zero_of_not_differentiableAt hf, deriv_zero_of_not_differentiableAt H, smul_zero] + end ConstSMul section Mul diff --git a/Mathlib/Analysis/Calculus/Deriv/Shift.lean b/Mathlib/Analysis/Calculus/Deriv/Shift.lean index 1b9caeee16b80..a8e64225e83c5 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Shift.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Shift.lean @@ -26,3 +26,11 @@ lemma HasDerivAt.comp_add_const {π•œ : Type*} [NontriviallyNormedField π•œ] (x (hh : HasDerivAt h h' (x + a)) : HasDerivAt (fun x ↦ h (x + a)) h' x := by simpa [Function.comp_def] using HasDerivAt.scomp (π•œ := π•œ) x hh <| hasDerivAt_id' x |>.add_const a + +/-- The derivative of `x ↦ f (-x)` at `a` is the negative of the derivative of `f` at `-a`. -/ +lemma deriv_comp_neg {π•œ : Type*} [NontriviallyNormedField π•œ] {F : Type*} [NormedAddCommGroup F] + [NormedSpace π•œ F] (f : π•œ β†’ F) (a : π•œ) : deriv (fun x ↦ f (-x)) a = -deriv f (-a) := by + by_cases h : DifferentiableAt π•œ f (-a) + Β· simpa only [deriv_neg, neg_one_smul] using deriv.scomp a h (differentiable_neg _) + Β· rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_comp_neg_iff.mpr h), + deriv_zero_of_not_differentiableAt h, neg_zero] diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean index 06459fd66c93f..0cb66f7044ced 100644 --- a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean +++ b/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean @@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. 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.Deriv.Shift import Mathlib.Analysis.Calculus.IteratedDeriv.Defs /-! @@ -101,3 +100,20 @@ theorem iteratedDeriv_const_smul {n : β„•} {f : π•œ β†’ F} (h : ContDiff π•œ n 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 + +lemma iteratedDeriv_neg (n : β„•) (f : π•œ β†’ F) (a : π•œ) : + iteratedDeriv n (fun x ↦ -(f x)) a = -(iteratedDeriv n f a) := by + induction' n with n ih generalizing a + Β· simp only [Nat.zero_eq, iteratedDeriv_zero] + Β· have ih' : iteratedDeriv n (fun x ↦ -f x) = fun x ↦ -iteratedDeriv n f x := funext ih + rw [iteratedDeriv_succ, iteratedDeriv_succ, ih', deriv.neg] + +lemma iteratedDeriv_comp_neg (n : β„•) (f : π•œ β†’ F) (a : π•œ) : + iteratedDeriv n (fun x ↦ f (-x)) a = (-1 : π•œ) ^ n β€’ iteratedDeriv n f (-a) := by + induction' n with n ih generalizing a + Β· simp only [Nat.zero_eq, iteratedDeriv_zero, pow_zero, one_smul] + Β· have ih' : iteratedDeriv n (fun x ↦ f (-x)) = fun x ↦ (-1 : π•œ) ^ n β€’ iteratedDeriv n f (-x) := + funext ih + rw [iteratedDeriv_succ, iteratedDeriv_succ, ih', pow_succ, neg_mul, one_mul, + deriv_comp_neg (f := fun x ↦ (-1 : π•œ) ^ n β€’ iteratedDeriv n f x), deriv_const_smul', + neg_smul]