ftaylorSeriesWithin — Mathlib

English

The ftaylorSeriesWithin f s x collects the iterated derivatives of f within s at x into a formal multilinear series.

Русский

ftaylorSeriesWithin f s x формирует из неравномерного набора производных внутри s ряд формальных мультииелинейных членов в точке x.

LaTeX

$$$$\text{ftaylorSeriesWithin}(f,s,x) = (n \mapsto \text{iteratedFDerivWithin}(\mathbb{k}, n, f, s)(x))_n.$$$$

Lean4

/-- Formal Taylor series associated to a function within a set. -/
def ftaylorSeriesWithin (f : E → F) (s : Set E) (x : E) : FormalMultilinearSeries 𝕜 E F := fun n =>
  iteratedFDerivWithin 𝕜 n f s x

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