English
The second derivative of a composition equals the product of the second derivative of g and the square of the derivative of f plus the derivative of g times the second derivative of f.
Русский
Вторая производная композиции равна произведению второй производной g на квадрат производной f плюс производная g умноженная на вторую производную f.
LaTeX
$$$iteratedDerivWithin 2 (g \\circ f) s x = iteratedDerivWithin 2 g t (f x) * derivWithin f s x ^ 2 + derivWithin g t (f x) * iteratedDerivWithin 2 f s x$$$
Lean4
theorem iteratedDerivWithin_comp_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 =
iteratedDerivWithin 2 g t (f x) * derivWithin f s x ^ 2 + derivWithin g t (f x) * iteratedDerivWithin 2 f s x :=
by
rw [iteratedDerivWithin_scomp_two hg hf ht hs hx hst]
simp only [smul_eq_mul, mul_comm]
