Analytic functions #

A function is analytic in one dimension around 0 if it can be written as a converging power series Σ pₙ zⁿ. This definition can be extended to any dimension (even in infinite dimension) by requiring that pₙ is a continuous n-multilinear map. In general, pₙ is not unique (in two dimensions, taking p₂ (x, y) (x', y') = x y' or y x' gives the same map when applied to a vector (x, y) (x, y)). A way to guarantee uniqueness is to take a symmetric pₙ, but this is not always possible in nonzero characteristic (in characteristic 2, the previous example has no symmetric representative). Therefore, we do not insist on symmetry or uniqueness in the definition, and we only require the existence of a converging series.

The general framework is important to say that the exponential map on bounded operators on a Banach space is analytic, as well as the inverse on invertible operators.

Main definitions #

Let p be a formal multilinear series from E to F, i.e., p n is a multilinear map on E^n for n : ℕ.

p.radius: the largest r : ℝ≥0∞ such that ‖p n‖ * r^n grows subexponentially.
p.le_radius_of_bound, p.le_radius_of_bound_nnreal, p.le_radius_of_isBigO: if ‖p n‖ * r ^ n is bounded above, then r ≤ p.radius;
p.isLittleO_of_lt_radius, p.norm_mul_pow_le_mul_pow_of_lt_radius, p.isLittleO_one_of_lt_radius, p.norm_mul_pow_le_of_lt_radius, p.nnnorm_mul_pow_le_of_lt_radius: if r < p.radius, then ‖p n‖ * r ^ n tends to zero exponentially;
p.lt_radius_of_isBigO: if r ≠ 0 and ‖p n‖ * r ^ n = O(a ^ n) for some -1 < a < 1, then r < p.radius;
p.partialSum n x: the sum ∑_{i = 0}^{n-1} pᵢ xⁱ.
p.sum x: the sum ∑'_{i = 0}^{∞} pᵢ xⁱ.

Additionally, let f be a function from E to F.

HasFPowerSeriesOnBall f p x r: on the ball of center x with radius r, f (x + y) = ∑'_n pₙ yⁿ.
HasFPowerSeriesAt f p x: on some ball of center x with positive radius, holds HasFPowerSeriesOnBall f p x r.
AnalyticAt 𝕜 f x: there exists a power series p such that holds HasFPowerSeriesAt f p x.
AnalyticOn 𝕜 f s: the function f is analytic at every point of s.

We develop the basic properties of these notions, notably:

If a function admits a power series, it is continuous (see HasFPowerSeriesOnBall.continuousOn and HasFPowerSeriesAt.continuousAt and AnalyticAt.continuousAt).
In a complete space, the sum of a formal power series with positive radius is well defined on the disk of convergence, see FormalMultilinearSeries.hasFPowerSeriesOnBall.
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.

Implementation details #

We only introduce the radius of convergence of a power series, as p.radius. For a power series in finitely many dimensions, there is a finer (directional, coordinate-dependent) notion, describing the polydisk of convergence. This notion is more specific, and not necessary to build the general theory. We do not define it here.

Analytic functions #

Main definitions #

Implementation details #

The radius of a formal multilinear series #

Expanding a function as a power series #

Uniqueness of power series #

Changing origin in a power series #