English
A vector-valued Faà di Bruno formula expresses iterated derivatives of a composition via a universal sum over partitions, with coefficients given by iterated derivatives of g and derivatives of f.
Русский
Векторная версия формулы Фаàdi Бруно выражает повторные производные композиции через сумму по разбиениям и коэффициентами из производных g и f.
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 Eq (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 iteratedDerivWithin_vcomp_two (hg : ContDiffWithinAt 𝕜 2 g t (f x)) (hf : ContDiffWithinAt 𝕜 2 f s x)
(ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hst : MapsTo f s t) :
iteratedDerivWithin 2 (g ∘ f) s x =
iteratedFDerivWithin 𝕜 2 g t (f x) (fun _ ↦ derivWithin f s x) +
fderivWithin 𝕜 g t (f x) (iteratedDerivWithin 2 f s x) :=
by
rw [iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf ht hs hx hst le_rfl]
simp only [← (OrderedFinpartition.extendEquiv 1).sum_comp, Fintype.sum_sigma, Fintype.sum_unique,
OrderedFinpartition.default_eq, OrderedFinpartition.atomic_length, Fintype.sum_option]
have : (Fin.cons 1 (fun _ ↦ 1) : Fin 2 → ℕ) = fun _ ↦ 1 := funext <| Fin.forall_fin_two.mpr ⟨rfl, rfl⟩
simp [OrderedFinpartition.extendEquiv, OrderedFinpartition.extend, OrderedFinpartition.extendLeft,
OrderedFinpartition.extendMiddle, ht _ (hst hx), OrderedFinpartition.atomic, this]
