English
A simplified Faà di Bruno expansion for the third derivative of a composition inside sets.
Русский
Упрощённое разложение для третьей производной композиции внутри множеств.
LaTeX
$$$\\forall {g,f}{s}{x},\\ ContDiffWithinAt 𝕜 3 g t (f x) \\to ContDiffWithinAt 𝕜 3 f s x \\Rightarrow \n iteratedDerivWithin 3 (g \\circ f) s x = \\sum_ {c \\in OrderedFinpartition 3} (\\cdots)$$$
Lean4
theorem iteratedDeriv_scomp_three (hg : ContDiffAt 𝕜 3 g (f x)) (hf : ContDiffAt 𝕜 3 f x) :
iteratedDeriv 3 (g ∘ f) x =
deriv f x ^ 3 • iteratedDeriv 3 g (f x) + 3 • iteratedDeriv 2 f x • deriv f x • iteratedDeriv 2 g (f x) +
iteratedDeriv 3 f x • deriv g (f x) :=
by
simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]
exact iteratedDerivWithin_scomp_three hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _) (mapsTo_univ _ _)
