iteratedDeriv_comp_eq_sum_orderedFinpartition

English

Third-order derivative of a composition equals a Faà di Bruno sum over ordered partitions, with terms given by products of derivatives of f and derivatives of g.

Русский

Третья производная композиции равна сумме по упорядоченным разбиениям Фаàди Бруно, с членами, представляющими произведения производных f и g.

LaTeX

$$$\\forall {g,f}{x},\\ ContDiffAt 𝕜 n g (f x) \\to ContDiffAt 𝕜 n f x \\to WithTop.preorder.le i.cast n \\Rightarrow \n Eq (iteratedDeriv i (Function.comp g f) x) (\\sum_{c \\in OrderedFinpartition i} \\text{coeff}(c))$$$

Lean4

theorem iteratedDeriv_comp_eq_sum_orderedFinpartition (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContDiffAt 𝕜 n f x)
    (hi : i ≤ n) :
    iteratedDeriv i (g ∘ f) x =
      ∑ c : OrderedFinpartition i, iteratedDeriv c.length g (f x) * ∏ j, iteratedDeriv (c.partSize j) f x :=
  by
  rw [iteratedDeriv_scomp_eq_sum_orderedFinpartition hg hf hi]
  simp only [smul_eq_mul, mul_comm]

Похожие утверждения