Changing origin in a power series #
If a function is analytic in a disk D(x, R), then it is analytic in any disk contained in that
one. Indeed, one can write
$$ f (x + y + z) = \sum_{n} p_n (y + z)^n = \sum_{n, k} \binom{n}{k} p_n y^{n-k} z^k = \sum_{k} \Bigl(\sum_{n} \binom{n}{k} p_n y^{n-k}\Bigr) z^k. $$
The corresponding power series has thus a k-th coefficient equal to
$\sum_{n} \binom{n}{k} p_n y^{n-k}$. In the general case where pₙ is a multilinear map, this has
to be interpreted suitably: instead of having a binomial coefficient, one should sum over all
possible subsets s of Fin n of cardinality k, and attribute z to the indices in s and
y to the indices outside of s.
In this file, we implement this. The new power series is called p.changeOrigin y. Then, we
check its convergence and the fact that its sum coincides with the original sum. The outcome of this
discussion is that the set of points where a function is analytic is open. All these arguments
require the target space to be complete, as otherwise the series might not converge.
Main results #
In a complete space, if a function admits a power series in a ball, then it is analytic at any
point y of this ball, and the power series there can be expressed in terms of the initial power
series p as p.changeOrigin y. See HasFPowerSeriesOnBall.changeOrigin. It follows in particular
that the set of points at which a given function is analytic is open, see isOpen_analyticAt.
A term of FormalMultilinearSeries.changeOriginSeries.
Given a formal multilinear series p and a point x in its ball of convergence,
p.changeOrigin x is a formal multilinear series such that
p.sum (x+y) = (p.changeOrigin x).sum y when this makes sense. Each term of p.changeOrigin x
is itself an analytic function of x given by the series p.changeOriginSeries. Each term in
changeOriginSeries is the sum of changeOriginSeriesTerm's over all s of cardinality l.
The definition is such that p.changeOriginSeriesTerm k l s hs (fun _ ↦ x) (fun _ ↦ y) = p (k + l) (s.piecewise (fun _ ↦ x) (fun _ ↦ y))
Equations
- p.changeOriginSeriesTerm k l s hs = (ContinuousMultilinearMap.curryFinFinset 𝕜 E F hs ⋯) (p (k + l))
Instances For
The power series for f.changeOrigin k.
Given a formal multilinear series p and a point x in its ball of convergence,
p.changeOrigin x is a formal multilinear series such that
p.sum (x+y) = (p.changeOrigin x).sum y when this makes sense. Its k-th term is the sum of
the series p.changeOriginSeries k.
Equations
Instances For
Changing the origin of a formal multilinear series p, so that
p.sum (x+y) = (p.changeOrigin x).sum y when this makes sense.
Equations
- p.changeOrigin x k = (p.changeOriginSeries k).sum x
Instances For
An auxiliary equivalence useful in the proofs about
FormalMultilinearSeries.changeOriginSeries: the set of triples (k, l, s), where s is a
Finset (Fin (k + l)) of cardinality l is equivalent to the set of pairs (n, s), where s is a
Finset (Fin n).
The forward map sends (k, l, s) to (k + l, s) and the inverse map sends (n, s) to
(n - Finset.card s, Finset.card s, s). The actual definition is less readable because of problems
with non-definitional equalities.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The radius of convergence of p.changeOrigin x is at least p.radius - ‖x‖. In other words,
p.changeOrigin x is well defined on the largest ball contained in the original ball of
convergence.
derivSeries p is a power series for fderiv 𝕜 f if p is a power series for f,
see HasFPowerSeriesOnBall.fderiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Summing the series p.changeOrigin x at a point y gives back p (x + y).
Power series terms are analytic as we vary the origin
If a function admits a power series expansion p within a set s on a ball B (x, r), then
it also admits a power series on any subball of this ball (even with a different center provided
it belongs to s), given by p.changeOrigin.
If a function admits a power series expansion p on a ball B (x, r), then it also admits a
power series on any subball of this ball (even with a different center), given by p.changeOrigin.
If a function admits a power series expansion p on an open ball B (x, r), then
it is analytic at every point of this ball.
If a function admits a power series expansion p on an open ball B (x, r), then
it is analytic at every point of this ball.
Alias of HasFPowerSeriesOnBall.analyticOnNhd.
For any function f from a normed vector space to a Banach space, the set of points x such
that f is analytic at x is open.
Alias of AnalyticAt.exists_mem_nhds_analyticOnNhd.
If we're analytic at a point, we're analytic in a nonempty ball
Alias of AnalyticAt.exists_ball_analyticOnNhd.
If we're analytic at a point, we're analytic in a nonempty ball