English
Third-order Faà di Bruno-type decomposition inside sets for derivatives of a composition.
Русский
Разложение третий порядок Фаàди Бруно внутри множеств для композиции производной.
LaTeX
$$$\\forall {g,f}{s,t}{x},\\ ContDiffWithinAt 𝕜 3 g t (f x) \\to ContDiffWithinAt 𝕜 3 f s x \\Rightarrow \n iteratedDerivWithin 3 (Function.comp g f) s x = \\text{копия формулы с тремя членами}$$$
Lean4
theorem iteratedDerivWithin_scomp_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 =
derivWithin f s x ^ 3 • iteratedDerivWithin 3 g t (f x) +
3 • iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x) +
iteratedDerivWithin 3 f s x • derivWithin g t (f x) :=
by
rw [iteratedDerivWithin_vcomp_three hg hf ht hs hx hst]
simp [← derivWithin_fderivWithin, mul_smul, smul_comm (iteratedDerivWithin 2 f s x),
iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod]
abel
