English
A Faà di Bruno-type decomposition for the third derivative of a composition inside sets.
Русский
Разложение третьей производной композиции внутри множеств по формулам Фаàди Бруно.
LaTeX
$$$\\forall {g,f}{s,t}{x},\\ ContDiffWithinAt 𝕜 3 g t (f x) \\to ContDiffWithinAt 𝕜 3 f s x \\Rightarrow \n iteratedDerivWithin 3 (g \\circ f) s x = iteratedDerivWithin 3 g t (f x) * derivWithin f s x ^ 3 + \\n 3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x + \\n derivWithin g t (f x) * iteratedDerivWithin 3 f s x$$$
Lean4
theorem iteratedDerivWithin_comp_three (hg : ContDiffWithinAt 𝕜 3 g t (f x)) (hf : ContDiffWithinAt 𝕜 3 f s x)
(ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hst : MapsTo f s t) :
iteratedDerivWithin 3 (g ∘ f) s x =
iteratedDerivWithin 3 g t (f x) * derivWithin f s x ^ 3 +
3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x +
derivWithin g t (f x) * iteratedDerivWithin 3 f s x :=
by
rw [iteratedDerivWithin_scomp_three hg hf ht hs hx hst]
simp only [nsmul_eq_mul, smul_eq_mul, Nat.cast_ofNat]
ring
