English
A variant of Faà di Bruno for the second derivative of a composition with simplified coefficients.
Русский
Вариант формулы Фаàди Бруно для второй производной композиции с упрощенными коэффициентами.
LaTeX
$$$\\forall {g,f}{x},\\ ContDiffAt 𝕜 2 g (f x) \\to ContDiffAt 𝕜 2 f x \\Rightarrow \n iteratedDeriv 2 (Function.comp g f) x = iteratedDeriv 2 g (f x) * deriv f x ^ 2 + deriv g (f x) * iteratedDeriv 2 f x$$$
Lean4
theorem iteratedDeriv_scomp_two (hg : ContDiffAt 𝕜 2 g (f x)) (hf : ContDiffAt 𝕜 2 f x) :
iteratedDeriv 2 (g ∘ f) x = deriv f x ^ 2 • iteratedDeriv 2 g (f x) + iteratedDeriv 2 f x • deriv g (f x) :=
by
simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]
exact iteratedDerivWithin_scomp_two hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _) (mapsTo_univ _ _)
