English
Let f: 𝕜 → F and n ∈ ℕ. For any s ∈ 𝕜, shifting the argument to the right before applying the n-th iterated derivative is the same as applying the n-th iterated derivative and then shifting: iteratedDeriv n (z ↦ f(z + s)) = t ↦ iteratedDeriv n f (t + s).
Русский
Пусть f: 𝕜 → F и n ∈ ℕ. При любом s ∈ 𝕜 сдвиг аргумента справа перед применением n-й кратной производной эквивалентен применению n-й кратной производной с последующим сдвигом: iteratedDeriv n (z ↦ f(z + s)) = t ↦ iteratedDeriv n f (t + s).
LaTeX
$$$ \\forall n \\in \\mathbb{N},\\ f:\\\\mathbb{K} \\to F,\\ s \\in \\mathbb{K},\\quad \\text{iteratedDeriv } n (z \\mapsto f(z+s)) = (t \\mapsto \\text{iteratedDeriv } n f (t+s))$$$
Lean4
/-- The iterated derivative commutes with shifting the function by a constant on the right. -/
theorem iteratedDeriv_comp_add_const (n : ℕ) (f : 𝕜 → F) (s : 𝕜) :
iteratedDeriv n (fun z ↦ f (z + s)) = fun t ↦ iteratedDeriv n f (t + s) := by
induction n with
| zero => simp only [iteratedDeriv_zero]
| succ n IH => simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_add_const _ s
