English
A two-dimensional Faà di Bruno identity for the derivative of a composition: iteratedDeriv 2 (g∘f) equals the sum of a second-order term in g with derivative of f and a first-order term in g with second derivative of f.
Русский
Двухмерная формула Фаàди Бруно для композиции: второй порядок производной равен сумме членoв с производной f и производной g.
LaTeX
$$$\\forall {g,f}{x},\\ ContDiffAt 𝕜 2 g (f x) \\to ContDiffAt 𝕜 2 f x \\Rightarrow \n iteratedDeriv 2 (Function.comp g f) x = \n iteratedFDeriv 𝕜 2 g (f x) (\\lambda _. deriv f x) + fderiv 𝕜 g (f x) (iteratedDeriv 2 f x)$$$
Lean4
theorem iteratedDeriv_vcomp_two (hg : ContDiffAt 𝕜 2 g (f x)) (hf : ContDiffAt 𝕜 2 f x) :
iteratedDeriv 2 (g ∘ f) x =
iteratedFDeriv 𝕜 2 g (f x) (fun _ ↦ deriv f x) + fderiv 𝕜 g (f x) (iteratedDeriv 2 f x) :=
by
simp only [← iteratedDerivWithin_univ, ← iteratedFDerivWithin_univ, ← derivWithin_univ, ← fderivWithin_univ]
exact iteratedDerivWithin_vcomp_two hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _)
