feat(Analysis/Calculus/{Iterated}Deriv/*): add lemmas on composition …

…with negation (#11173)

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

@@ -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

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

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]

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]