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.
AnalyticOnNhd 𝕜 f s: the function f is analytic at every point of s.

We also define versions of HasFPowerSeriesOnBall, AnalyticAt, and AnalyticOnNhd restricted to a set, similar to ContinuousWithinAt. See Mathlib.Analysis.Analytic.Within for basic properties.

AnalyticWithinAt 𝕜 f s x means a power series at x converges to f on 𝓝[s ∪ {x}] x.
AnalyticOn 𝕜 f s t means ∀ x ∈ t, AnalyticWithinAt 𝕜 f s x.

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.

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 #

HasFPowerSeriesOnBall and HasFPowerSeriesWithinOnBall #

Analytic functions #

Composition with linear maps #

Relation between analytic function and the partial sums of its power series #

`HasFPowerSeriesOnBall` and `HasFPowerSeriesWithinOnBall` #