ftaylorSeries — Mathlib

English

Formal Taylor series associated to a function f is the map ftaylorSeries(f)(x) sending n to iteratedFDeriv 𝕜 n f x.

Русский

Формальная серия Тейлора, связанная с функцией f, задаётся как ftaylorSeries f x = (n ↦ iteratedFDeriv 𝕜 n f x).

LaTeX

$$$\text{ftaylorSeries}(f)(x) = \lambda n. iteratedFDeriv 𝕜 n f x$$$

Lean4

/-- Formal Taylor series associated to a function. -/
def ftaylorSeries (f : E → F) (x : E) : FormalMultilinearSeries 𝕜 E F := fun n => iteratedFDeriv 𝕜 n f x

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