fpowerSeries — Mathlib

English

For a linear map f, the formal power series fpowerSeries encodes the constant term f x, the linear term given by curry, and higher terms vanish.

Русский

Для линейного отображения f формальная степенная серия кодирует постоянный член f x, линейный член через карри, и нулевые высшие члены.

LaTeX

$$$ fpowerSeries (f) (x) = \\{ 0 \\text{-th term: } f x, \\ 1 \\text{ -st term: } (continuousMultilinearCurryFin1 𝕜 E F)^{-1} f, \\ n \\ge 2: 0 \\}$$$

Lean4

/-- Formal power series of a continuous linear map `f : E →L[𝕜] F` at `x : E`:
`f y = f x + f (y - x)`. -/
def fpowerSeries (f : E →L[𝕜] F) (x : E) : FormalMultilinearSeries 𝕜 E F
  | 0 => ContinuousMultilinearMap.uncurry0 𝕜 _ (f x)
  | 1 => (continuousMultilinearCurryFin1 𝕜 E F).symm f
  | _ => 0

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