English
For any n ∈ ℕ and a ∈ E, the n-th iterated derivative within s of the function z ↦ f(z − a) equals the n-th iterated derivative of f on the set −a +ᵥ s evaluated at x − a: iteratedFDerivWithin 𝕜 n (fun z ↦ f (z − a)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (−a +ᵥ s) (x − a).
Русский
Для любых n и a верно, что n-й повторный производный внутри s функции z ↦ f(z − a) равен 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 subtracting a constant. -/
theorem iteratedFDerivWithin_comp_sub' (n : ℕ) (a : E) :
iteratedFDerivWithin 𝕜 n (fun z ↦ f (z - a)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a) := by
simpa [sub_eq_add_neg] using iteratedFDerivWithin_comp_add_right' n (-a)
