iteratedDeriv_comp_two — Mathlib

English

A two-term Faà di Bruno-type formula for the second derivative of a composition.

Русский

Два члена формулы Фаàди Бруно для второй производной композиции.

LaTeX

$$$\\forall {g,f}{x},\\ ContDiffAt 𝕜 2 g (f x) \\to ContDiffAt 𝕜 2 f x \\Rightarrow \n iteratedDeriv 2 (Function.comp g f) x = iteratedDeriv 2 g (f x) * deriv f x ^ 2 + deriv g (f x) * iteratedDeriv 2 f x$$$

Lean4

theorem iteratedDeriv_comp_two (hg : ContDiffAt 𝕜 2 g (f x)) (hf : ContDiffAt 𝕜 2 f x) :
    iteratedDeriv 2 (g ∘ f) x = iteratedDeriv 2 g (f x) * deriv f x ^ 2 + deriv g (f x) * iteratedDeriv 2 f x :=
  by
  simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]
  exact iteratedDerivWithin_comp_two hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _) (mapsTo_univ _ _)

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