English
An alternative Faà di Bruno-type decomposition for the third-order derivative of a composition within sets, with explicit coefficient handling.
Русский
Альтернативное разложение третьей производной композиции внутри множеств с явной обработкой коэффициентов.
LaTeX
$$$\\forall {g,f}{s}{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 iteratedDerivWithin_scomp_eq_sum_orderedFinpartition (hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x) (ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hst : MapsTo f s t)
(hi : i ≤ n) :
iteratedDerivWithin i (g ∘ f) s x =
∑ c : OrderedFinpartition i,
(∏ j, iteratedDerivWithin (c.partSize j) f s x) • iteratedDerivWithin c.length g t (f x) :=
by
rw [iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf ht hs hx hst hi]
simp only [iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod]
