English
A detailed Faà di Bruno-type decomposition for the third-order derivative of a composition within sets, involving multiple derivative terms of f and g.
Русский
Детализированное разложение третьей производной композиции внутри множеств по Фаàди Бруно.
LaTeX
$$$\\forall {g,f}{s,t}{x},\\ ContDiffWithinAt 𝕜 3 g t (f x) \\to ContDiffWithinAt 𝕜 3 f s x \\Rightarrow \\n iteratedDerivWithin 3 (Function.comp g f) s x = \n iteratedFDerivWithin 𝕜 3 g t (f x) (derivWithin f s x) + \n iteratedFDerivWithin 𝕜 2 g t (f x) ![iteratedDerivWithin 2 f s x, derivWithin f s x] + \n 3 • iteratedFDerivWithin 𝕜 2 g t (f x) ![derivWithin f s x, iteratedDerivWithin 2 f s x] + \n fderivWithin 𝕜 g t (f x) (iteratedDerivWithin 3 f s x)$$$
Lean4
theorem iteratedDeriv_vcomp_three (hg : ContDiffAt 𝕜 3 g (f x)) (hf : ContDiffAt 𝕜 3 f x) :
iteratedDeriv 3 (g ∘ f) x =
iteratedFDeriv 𝕜 3 g (f x) (fun _ ↦ deriv f x) + iteratedFDeriv 𝕜 2 g (f x) ![iteratedDeriv 2 f x, deriv f x] +
2 • iteratedFDeriv 𝕜 2 g (f x) ![deriv f x, iteratedDeriv 2 f x] +
fderiv 𝕜 g (f x) (iteratedDeriv 3 f x) :=
by
simp only [← iteratedDerivWithin_univ, ← iteratedFDerivWithin_univ, ← derivWithin_univ, ← fderivWithin_univ]
exact iteratedDerivWithin_vcomp_three hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _)
