Derivative offset by a constant

Stream: Is there code for X?

[Mark Andrew Gerads]

I have ruesDiffIteratedDeriv, but need it offset by a constant.
MWE:

import all
-- import RootOfUnityExponentialSum

open classical complex asymptotics real normed_space finset
open_locale classical big_operators nat

-----------
-- This section is properly defined without any sorry elsewhere.

def ruesDiff : ℕ → ℤ → ℂ → ℂ := sorry

lemma ruesDiffIteratedDeriv (k n : ℕ) (m : ℤ) : iterated_deriv k (ruesDiff n m) = ruesDiff n (k + m) := sorry

-----------
-- The following needs help.


lemma ruesDiffIteratedDerivOffset (k n : ℕ) (m : ℤ) (z₁ : ℂ): iterated_deriv k (λ (z : ℂ), ruesDiff n m (z + z₁)) = (λ (z : ℂ), ruesDiff n (m + k) (z + z₁)) :=
begin
  induction k with km ih,
  {
    simp only [iterated_deriv_zero, zmod.nat_cast_self, add_zero],
  },
  {
    rw iterated_deriv_succ,
    rw ih,
    clear ih,
    simp only [nat.cast_succ],
    sorry,
  },
end

The following is the state just before the sorry:
image.png

[Yury G. Kudryashov]

It seems that we don't have this lemma (please open a github issue or better a PR).

[Yury G. Kudryashov]

I mean, a lemma about iterated (Fréchet) derivatives of fun x => f (x + a).

[Yury G. Kudryashov]

However, if you have all the necessary differentiable/cont_diff assumptions, then you can use deriv_comp or has_deriv_at.comp _ (has_deriv_at_id.add_const _) (not tested, so the syntax may be slightly incorrect).

[Mark Andrew Gerads]

Okay, I work more on specific examples, and not their generalizations, and thus need help generalizing this lemma to something that is a generalization of both \R and \C. Thanks for all the help.

[Mark Andrew Gerads]

Should the Github issue be added to mathlib3 or mathlib4? It seems like maybe it would save time and energy overall to add it to mathlib4, and many mathlib3 files are frozen by the port. Do we need to wait until the port is done before contributing novel code to mathlib4?

[Mario Carneiro]

no to the last sentence

[Mark Andrew Gerads]

I am guessing that has_mfderiv_at.comp (The chain rule) or something similar would solve my problem.

[Yury G. Kudryashov]

You don't need manifold derivatives here, just docs4#HasFDerivAt.comp