ftaylorSeriesWithin_univ — Mathlib

English

The (n+1)-st iterated derivative is the composition of a curry-right equiv with the n-th derivative of f's derivative.

Русский

(n+1)-я итеративная производная есть композиция карри-правого эквивалента с n-й производной производной f.

LaTeX

$$$\operatorname{iteratedFDeriv}_{\mathbb{k}}(n+1)\ f\ x =\big(\text{continuousMultilinearCurryRightEquiv'}_{\mathbb{k}}\ n\ E\ F\big)^{\mathrm{symm}}\circ \operatorname{iteratedFDeriv}_{\mathbb{k}} n (\lambda y.\ fderiv_{\mathbb{k}} f\ y)\ x$$$

Lean4

theorem ftaylorSeriesWithin_univ : ftaylorSeriesWithin 𝕜 f univ = ftaylorSeries 𝕜 f :=
  by
  ext1 x; ext1 n
  change iteratedFDerivWithin 𝕜 n f univ x = iteratedFDeriv 𝕜 n f x
  rw [iteratedFDerivWithin_univ]

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