English
Let f and g be three-times continuously differentiable at x in 𝕜. Then the third iterated derivative of the composition g ∘ f at x is given by a formula involving derivatives of g at f(x) and derivatives of f at x up to order 3.
Русский
Пусть f и g трижды непрерывно дифференцируемы в точке x в полях 𝕜. Тогда третья повторная производная композиции g ∘ f в точке x равна выражению, составленному из производных g в f(x) и производных f в x до порядка 3.
LaTeX
$$$\\operatorname{iteratedDeriv}_3 (g \\circ f) x = \\operatorname{iteratedDeriv}_3 g (f x) \\cdot (\\operatorname{deriv} f x)^3 + 3 \\cdot \\operatorname{iteratedDeriv}_2 g (f x) \\cdot \\operatorname{iteratedDeriv}_2 f x \\cdot \\operatorname{deriv} f x + \\operatorname{deriv} g (f x) \\cdot \\operatorname{iteratedDeriv}_3 f x$$$
Lean4
theorem iteratedDeriv_comp_three (hg : ContDiffAt 𝕜 3 g (f x)) (hf : ContDiffAt 𝕜 3 f x) :
iteratedDeriv 3 (g ∘ f) x =
iteratedDeriv 3 g (f x) * deriv f x ^ 3 + 3 * iteratedDeriv 2 g (f x) * iteratedDeriv 2 f x * deriv f x +
deriv g (f x) * iteratedDeriv 3 f x :=
by
simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]
exact iteratedDerivWithin_comp_three hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _) (mapsTo_univ _ _)
