English
Let f: E → F. For any natural number n and any a ∈ E, the n-th iterated derivative within a set s of the function z ↦ f(z + a) equals the n-th iterated derivative of f computed on the translated set a + s, evaluated at x + a; in symbols: iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a).
Русский
Пусть f: E → F. Для любой n ∈ ℕ и любого a ∈ E верно, что n-й повторный дифференциал функции z ↦ f(z + a), взятый внутри множества s, равен n-му повторному дифференциалу f на сдвинутом множестве a + s, взятому в точке x + a; то есть iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a).
LaTeX
$$$\\operatorname{iteratedFDerivWithin}_{\\mathbb{K}}^{n}(\\lambda z\\,. f(z+a))\\,s \\\\ = \\\\ x \\mapsto \\operatorname{iteratedFDerivWithin}_{\\mathbb{K}}^{n} f\\ (a+\\!s)\\ (x+a)$$$
Lean4
/-- The iterated derivative commutes with shifting the function by a constant on the right. -/
theorem iteratedFDerivWithin_comp_add_right' (n : ℕ) (a : E) :
iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a) := by
simpa [add_comm a] using iteratedFDerivWithin_comp_add_left' n a
