English
For second order, the iterated derivative of a composition equals a quadratic combination of derivatives of f and g.
Русский
Для второго порядка: итеративная производная композиции равна квадратичной комбинации производных f и g.
LaTeX
$$$\\forall {g,f}{s}{x},\\ ContDiffWithinAt 𝕜 2 g t (f x) \\to ContDiffWithinAt 𝕜 2 f s x \\Rightarrow \n iteratedDerivWithin 2 (g \\circ f) s x = derivWithin f s x ^ 2 • iteratedDerivWithin 2 g t (f x) + iteratedDerivWithin 2 f s x • derivWithin g t (f x)$$$
Lean4
theorem iteratedDerivWithin_scomp_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 =
derivWithin f s x ^ 2 • iteratedDerivWithin 2 g t (f x) + iteratedDerivWithin 2 f s x • derivWithin g t (f x) :=
by
rw [iteratedDerivWithin_vcomp_two hg hf ht hs hx hst]
simp [← derivWithin_fderivWithin, iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod]
