iteratedFDeriv_comp — Mathlib

English

The first projection from a product to the first factor is C^n for any n.

Русский

Первая проекция из произведения в первый фактор является C^n для любого n.

LaTeX

$$$\ContDiff 𝕜 n (\mathrm{Prod.fst} : E \times F \to E)$$$

Lean4

theorem iteratedFDeriv_comp (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContDiffAt 𝕜 n f x) {i : ℕ} (hi : i ≤ n) :
    iteratedFDeriv 𝕜 i (g ∘ f) x = (ftaylorSeries 𝕜 g (f x)).taylorComp (ftaylorSeries 𝕜 f x) i :=
  by
  simp only [← iteratedFDerivWithin_univ, ← ftaylorSeriesWithin_univ]
  exact
    iteratedFDerivWithin_comp hg.contDiffWithinAt hf.contDiffWithinAt uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _)
      (mapsTo_univ _ _) hi

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