hasFPowerSeriesOnBall — Mathlib

English

For a bilinear f, the function (x,y) ↦ f x.1 y.2 has a finite power-series expansion around any point, with the corresponding fpowerSeriesBilinear giving its coefficients on the bilinear level, and radius ∞.

Русский

Для билинейного отображения f существует конечное разложение степенного ряда вокруг любой точки; fpowerSeriesBilinear задаёт коэффициенты, и радиус ∞.

LaTeX

$$$ HasFPowerSeriesOnBall (\lambda (x,y) \mapsto f x.1 y.2) (f.fpowerSeriesBilinear x) x \infty $$$

Lean4

protected theorem hasFPowerSeriesOnBall (f : E →L[𝕜] F) (x : E) : HasFPowerSeriesOnBall f (f.fpowerSeries x) x ∞ :=
  (f.hasFiniteFPowerSeriesOnBall x).toHasFPowerSeriesOnBall

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