English
For any n ∈ ℕ and a ∈ E, the n-th iterated derivative within s of f(z − a) equals the n-th iterated derivative of f on the translated set −a +ᵥ s at x − a: iteratedFDerivWithin 𝕜 n (fun z ↦ f(z − a)) s x = iteratedFDerivWithin 𝕜 n f (−a +ᵥ s) (x − a).
Русский
Для любых n и a верно, что n-й повторный производный внутри s функции z ↦ f(z − a) равен n-му повторному производному f на множестве −a + s в точке x − a.
LaTeX
$$$\operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{n}(\lambda z\,. f(z- a))\,s\,x = \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 x = iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a) := by
simp [iteratedFDerivWithin_comp_sub']
