English
The third iterated derivative of a composition splits into a sum of terms involving third derivative of g, products of lower derivatives of g and f, and derivative of f.
Русский
Третья итеративная производная композиции распадается на сумму членов с третьей производной от g и производными f и g.
LaTeX
$$$\\forall{g,f}{x},\\ ContDiffAt 𝕜 3 g (f x) \\to ContDiffAt 𝕜 3 f x \\Rightarrow \\n iteratedDeriv 3 (Function.comp g f) x = \n iteratedFDeriv 𝕜 3 g (f x) (deriv f x) + \n iteratedFDeriv 𝕜 2 g (f x) ![iteratedDeriv 2 f x, deriv f x] + \n 2 \\cdot iteratedFDeriv 𝕜 2 g (f x) ![deriv f x, iteratedDeriv 2 f x] + \n fderiv 𝕜 g (f x) (iteratedDeriv 3 f x)$$$
Lean4
theorem iteratedDerivWithin_vcomp_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 =
iteratedFDerivWithin 𝕜 3 g t (f x) (fun _ ↦ derivWithin f s x) +
iteratedFDerivWithin 𝕜 2 g t (f x) ![iteratedDerivWithin 2 f s x, derivWithin f s x] +
2 • iteratedFDerivWithin 𝕜 2 g t (f x) ![derivWithin f s x, iteratedDerivWithin 2 f s x] +
fderivWithin 𝕜 g t (f x) (iteratedDerivWithin 3 f s x) :=
by
rw [iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf ht hs hx hst le_rfl]
simp only [← (OrderedFinpartition.extendEquiv 1).sum_comp, ← (OrderedFinpartition.extendEquiv 2).sum_comp,
Fintype.sum_sigma, Fintype.sum_option, Nat.reduceAdd, OrderedFinpartition.extendEquiv_apply,
OrderedFinpartition.extend_none, OrderedFinpartition.extend_some, OrderedFinpartition.extendMiddle_length,
OrderedFinpartition.default_eq, Fintype.sum_unique, OrderedFinpartition.atomic_length,
OrderedFinpartition.extendLeft_length, Fin.sum_univ_two]
simp? [add_assoc, two_smul, iteratedFDerivWithin_one_apply (ht _ <| hst hx)] says
simp only [OrderedFinpartition.extendLeft_partSize, OrderedFinpartition.extendLeft_length,
OrderedFinpartition.atomic_length, Nat.reduceAdd, OrderedFinpartition.atomic_partSize, Fin.isValue,
OrderedFinpartition.extendMiddle_partSize, Fin.cons_zero, Fin.update_cons_zero, Fin.cons_one, Fin.default_eq_zero,
OrderedFinpartition.extendMiddle_length, Fin.cons_update, Fin.succ_zero_eq_one, update_self, update_idem,
iteratedFDerivWithin_one_apply (ht _ <| hst hx), add_assoc, two_smul]
have (j : _) : (Fin.cons 1 (Fin.cons 1 fun _ ↦ 1) : Fin 3 → ℕ) j = 1 := by fin_cases j <;> rfl
congr <;> ext x <;> fin_cases x <;> simp [this]
