fpowerSeriesBilinear — Mathlib

English

For a bilinear f, the function x ↦ f x.1 x.2 on E × F has a power-series expansion with the same fpowerSeriesBilinear as its central coefficient description.

Русский

Для билинейного отображения f функция (x,y) ↦ f x y имеет разложение в ряд с коэффициентами, заданными fpowerSeriesBilinear.

LaTeX

$$$ HasFPowerSeriesAt (\lambda x: f x.1 x.2) (f.fpowerSeriesBilinear x) x $$$

Lean4

/-- Formal multilinear series expansion of a bilinear function `f : E →L[𝕜] F →L[𝕜] G`. -/
def fpowerSeriesBilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : FormalMultilinearSeries 𝕜 (E × F) G
  | 0 => ContinuousMultilinearMap.uncurry0 𝕜 _ (f x.1 x.2)
  | 1 => (continuousMultilinearCurryFin1 𝕜 (E × F) G).symm (f.deriv₂ x)
  | 2 => f.uncurryBilinear
  | _ => 0

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