English
For any f: E →L[𝕜] F, at any x, HasFiniteFPowerSeriesOnBall (f as a function) (f.fpowerSeries x) x 2 ∞, with finiteness condition showing only terms up to order 1 are nonzero.
Русский
Для отображения f существует конечное степенное разложение вокруг точки x: HasFiniteFPowerSeriesOnBall ..., и коэффициенты нулевой и первой степеней могут быть не нулевые, остальные равны нулю.
LaTeX
$$$ HasFiniteFPowerSeriesOnBall f (f.fpowerSeries x) x 2 \infty$$$
Lean4
/-- Reinterpret a bilinear map `f : E →L[𝕜] F →L[𝕜] G` as a multilinear map
`(E × F) [×2]→L[𝕜] G`. This multilinear map is the second term in the formal
multilinear series expansion of `uncurry f`. It is given by
`f.uncurryBilinear ![(x, y), (x', y')] = f x y'`. -/
def uncurryBilinear (f : E →L[𝕜] F →L[𝕜] G) : E × F [×2]→L[𝕜] G :=
@ContinuousLinearMap.uncurryLeft 𝕜 1 (fun _ => E × F) G _ _ _ _ _ <|
(↑(continuousMultilinearCurryFin1 𝕜 (E × F) G).symm : (E × F →L[𝕜] G) →L[𝕜] _).comp <|
f.bilinearComp (fst _ _ _) (snd _ _ _)
