English
The iterated derivative inside a product composition can be written as a Faà di Bruno sum over ordered partitions, with each term being a product of derivatives of the inner and outer functions evaluated at x.
Русский
Производная по Faà di Bruno для композиции внутри набора разложений: сумма по упорядоченным разбиениям, каждая с произведением производных inner и outer.
LaTeX
$$$\\forall {g,f}{s,t}{x}{n}{i},\\ ContDiffWithinAt 𝕜 n g t (f x) \\to ContDiffWithinAt 𝕜 n f s x \\to UniqueDiffOn 𝕜 t \\to UniqueDiffOn 𝕜 s \\to x\\in s \\to MapsTo f s t \\to WithTop.preorder.le i.cast n \\Rightarrow \n iteratedDerivWithin i (Function.comp g f) s x = \\sum_{c \\in OrderedFinpartition i} \n (ContinuousMultilinearMap.funLike.coe (iteratedFDerivWithin 𝕜 c.length g t (f x)) (\\lambda j. iteratedDerivWithin (c.partSize j) f s x))$$$
Lean4
theorem iteratedDeriv_vcomp_eq_sum_orderedFinpartition (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContDiffAt 𝕜 n f x)
(hi : i ≤ n) :
iteratedDeriv i (g ∘ f) x =
∑ c : OrderedFinpartition i, iteratedFDeriv 𝕜 c.length g (f x) fun j ↦ iteratedDeriv (c.partSize j) f x :=
by
simp only [← iteratedDerivWithin_univ, ← iteratedFDerivWithin_univ]
exact
iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ x)
(mapsTo_univ f _) hi
