English
For ContDiffOn f, the nth derivative of f under inner scaling by c yields a scaled result with c^n.
Русский
Для ContDiffOn f n-я повторная производная при внутреннем масштабировании на c приводит к результату, умноженному на c^n.
LaTeX
$$$\\operatorname{iteratedDerivWithin}_n (\\lambda x. f (c \\cdot x)) s x = c^n \\cdot \\operatorname{iteratedDerivWithin}_n f s (c x)$$$
Lean4
theorem iteratedDeriv_comp_neg (n : ℕ) (f : 𝕜 → F) (a : 𝕜) :
iteratedDeriv n (fun x ↦ f (-x)) a = (-1 : 𝕜) ^ n • iteratedDeriv n f (-a) := by
induction n generalizing a with
| zero => simp only [iteratedDeriv_zero, pow_zero, one_smul]
| succ n
ih =>
have ih' : iteratedDeriv n (fun x ↦ f (-x)) = fun x ↦ (-1 : 𝕜) ^ n • iteratedDeriv n f (-x) := funext ih
rw [iteratedDeriv_succ, iteratedDeriv_succ, ih', pow_succ', neg_mul, one_mul,
deriv_comp_neg (f := fun x ↦ (-1 : 𝕜) ^ n • iteratedDeriv n f x), deriv_fun_const_smul', neg_smul]
