Linear functions are analytic #
In this file we prove that a ContinuousLinearMap
defines an analytic function with
the formal power series f x = f a + f (x - a)
. We also prove similar results for bilinear maps.
We deduce this fact from the stronger result that continuous linear maps are continuously polynomial, i.e., they admit a finite power series.
Alias of ContinuousLinearMap.cpolynomialOn
.
Alias of ContinuousLinearMap.analyticOn
.
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'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Formal multilinear series expansion of a bilinear function f : E โL[๐] F โL[๐] G
.
Equations
- f.fpowerSeriesBilinear x 0 = ContinuousMultilinearMap.uncurry0 ๐ (E ร F) ((f x.1) x.2)
- f.fpowerSeriesBilinear x 1 = (continuousMultilinearCurryFin1 ๐ (E ร F) G).symm (f.derivโ x)
- f.fpowerSeriesBilinear x 2 = f.uncurryBilinear
- f.fpowerSeriesBilinear x xโ = 0
Instances For
id
is entire
Alias of analyticOn_id
.
fst
is analytic
snd
is analytic
fst
is entire
Alias of analyticOn_fst
.
snd
is entire
Alias of analyticOn_snd
.
Alias of ContinuousLinearEquiv.analyticOn
.
Alias of LinearIsometryEquiv.analyticOn
.