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