Analytic functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 largestr : ℝ≥0∞such that‖p n‖ * r^ngrows subexponentially.p.le_radius_of_bound,p.le_radius_of_bound_nnreal,p.le_radius_of_is_O: if‖p n‖ * r ^ nis bounded above, thenr ≤ p.radius;p.is_o_of_lt_radius,p.norm_mul_pow_le_mul_pow_of_lt_radius,p.is_o_one_of_lt_radius,p.norm_mul_pow_le_of_lt_radius,p.nnnorm_mul_pow_le_of_lt_radius: ifr < p.radius, then‖p n‖ * r ^ ntends to zero exponentially;p.lt_radius_of_is_O: ifr ≠ 0and‖p n‖ * r ^ n = O(a ^ n)for some-1 < a < 1, thenr < p.radius;p.partial_sum 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.
has_fpower_series_on_ball f p x r: on the ball of centerxwith radiusr,f (x + y) = ∑'_n pₙ yⁿ.has_fpower_series_at f p x: on some ball of centerxwith positive radius, holdshas_fpower_series_on_ball f p x r.analytic_at 𝕜 f x: there exists a power seriespsuch that holdshas_fpower_series_at f p x.analytic_on 𝕜 f s: the functionfis analytic at every point ofs.
We develop the basic properties of these notions, notably:
- If a function admits a power series, it is continuous (see
has_fpower_series_on_ball.continuous_onandhas_fpower_series_at.continuous_atandanalytic_at.continuous_at). - In a complete space, the sum of a formal power series with positive radius is well defined on the
disk of convergence, see
formal_multilinear_series.has_fpower_series_on_ball. - If a function admits a power series in a ball, then it is analytic at any point
yof this ball, and the power series there can be expressed in terms of the initial power seriespasp.change_origin y. Seehas_fpower_series_on_ball.change_origin. It follows in particular that the set of points at which a given function is analytic is open, seeis_open_analytic_at.
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.
Given a formal multilinear series p and a vector x, then p.sum x is the sum Σ pₙ xⁿ. A
priori, it only behaves well when ‖x‖ < p.radius.
Given a formal multilinear series p and a vector x, then p.partial_sum n x is the sum
Σ pₖ xᵏ for k ∈ {0,..., n-1}.
Equations
- p.partial_sum n x = (finset.range n).sum (λ (k : ℕ), ⇑(p k) (λ (i : fin k), x))
The partial sums of a formal multilinear series are continuous.
The radius of a formal multilinear series #
The radius of a formal multilinear series is the largest r such that the sum Σ ‖pₙ‖ ‖y‖ⁿ
converges for all ‖y‖ < r. This implies that Σ pₙ yⁿ converges for all ‖y‖ < r, but these
definitions are not equivalent in general.
If ‖pₙ‖ rⁿ is bounded in n, then the radius of p is at least r.
If ‖pₙ‖ rⁿ is bounded in n, then the radius of p is at least r.
If ‖pₙ‖ rⁿ = O(1), as n → ∞, then the radius of p is at least r.
For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ tends to zero exponentially:
for some 0 < a < 1, ‖p n‖ rⁿ = o(aⁿ).
For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ = o(1).
For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ tends to zero exponentially:
for some 0 < a < 1 and C > 0, ‖p n‖ * r ^ n ≤ C * a ^ n.
If r ≠ 0 and ‖pₙ‖ rⁿ = O(aⁿ) for some -1 < a < 1, then r < p.radius.
For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ is bounded.
For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ is bounded.
For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ is bounded.
If the radius of p is positive, then ‖pₙ‖ grows at most geometrically.
The radius of the sum of two formal series is at least the minimum of their two radii.
Expanding a function as a power series #
- r_le : r ≤ p.radius
- r_pos : 0 < r
- has_sum : ∀ {y : E}, y ∈ emetric.ball 0 r → has_sum (λ (n : ℕ), ⇑(p n) (λ (i : fin n), y)) (f (x + y))
Given a function f : E → F and a formal multilinear series p, we say that f has p as
a power series on the ball of radius r > 0 around x if f (x + y) = ∑' pₙ yⁿ for all ‖y‖ < r.
Given a function f : E → F and a formal multilinear series p, we say that f has p as
a power series around x if f (x + y) = ∑' pₙ yⁿ for all y in a neighborhood of 0.
Equations
- has_fpower_series_at f p x = ∃ (r : ennreal), has_fpower_series_on_ball f p x r
Given a function f : E → F, we say that f is analytic at x if it admits a convergent power
series expansion around x.
Equations
- analytic_at 𝕜 f x = ∃ (p : formal_multilinear_series 𝕜 E F), has_fpower_series_at f p x
Given a function f : E → F, we say that f is analytic on a set s if it is analytic around
every point of s.
Equations
- analytic_on 𝕜 f s = ∀ (x : E), x ∈ s → analytic_at 𝕜 f x
If a function f has a power series p around x, then the function z ↦ f (z - y) has the
same power series around x + y.
If a function f has a power series p on a ball and g is linear, then g ∘ f has the
power series g ∘ p on the same ball.
If a function f is analytic on a set s and g is linear, then g ∘ f is analytic
on s.
If a function admits a power series expansion, then it is exponentially close to the partial sums of this power series on strict subdisks of the disk of convergence.
This version provides an upper estimate that decreases both in ‖y‖ and n. See also
has_fpower_series_on_ball.uniform_geometric_approx for a weaker version.
If a function admits a power series expansion, then it is exponentially close to the partial sums of this power series on strict subdisks of the disk of convergence.
Taylor formula for an analytic function, is_O version.
If f has formal power series ∑ n, pₙ on a ball of radius r, then for y, z in any smaller
ball, the norm of the difference f y - f z - p 1 (λ _, y - z) is bounded above by
C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖. This lemma formulates this property using is_O and
filter.principal on E × E.
If f has formal power series ∑ n, pₙ on a ball of radius r, then for y, z in any smaller
ball, the norm of the difference f y - f z - p 1 (λ _, y - z) is bounded above by
C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖.
If f has formal power series ∑ n, pₙ at x, then
f y - f z - p 1 (λ _, y - z) = O(‖(y, z) - (x, x)‖ * ‖y - z‖) as (y, z) → (x, x).
In particular, f is strictly differentiable at x.
If a function admits a power series expansion at x, then it is the uniform limit of the
partial sums of this power series on strict subdisks of the disk of convergence, i.e., f (x + y)
is the uniform limit of p.partial_sum n y there.
If a function admits a power series expansion at x, then it is the locally uniform limit of
the partial sums of this power series on the disk of convergence, i.e., f (x + y)
is the locally uniform limit of p.partial_sum n y there.
If a function admits a power series expansion at x, then it is the uniform limit of the
partial sums of this power series on strict subdisks of the disk of convergence, i.e., f y
is the uniform limit of p.partial_sum n (y - x) there.
If a function admits a power series expansion at x, then it is the locally uniform limit of
the partial sums of this power series on the disk of convergence, i.e., f y
is the locally uniform limit of p.partial_sum n (y - x) there.
If a function admits a power series expansion on a disk, then it is continuous there.
In a complete space, the sum of a converging power series p admits p as a power series.
This is not totally obvious as we need to check the convergence of the series.
The sum of a converging power series is continuous in its disk of convergence.
Uniqueness of power series #
If a function f : E → F has two representations as power series at a point x : E, corresponding
to formal multilinear series p₁ and p₂, then these representations agree term-by-term. That is,
for any n : ℕ and y : E, p₁ n (λ i, y) = p₂ n (λ i, y). In the one-dimensional case, when
f : 𝕜 → E, the continuous multilinear maps p₁ n and p₂ n are given by
formal_multilinear_series.mk_pi_field, and hence are determined completely by the value of
p₁ n (λ i, 1), so p₁ = p₂. Consequently, the radius of convergence for one series can be
transferred to the other.
If a formal multilinear series p represents the zero function at x : E, then the
terms p n (λ i, y) appearing the in sum are zero for any n : ℕ, y : E.
A one-dimensional formal multilinear series representing the zero function is zero.
One-dimensional formal multilinear series representing the same function are equal.
A one-dimensional formal multilinear series representing a locally zero function is zero.
If a function f : 𝕜 → E has two power series representations at x, then the given radii in
which convergence is guaranteed may be interchanged. This can be useful when the formal multilinear
series in one representation has a particularly nice form, but the other has a larger radius.
If a function f : 𝕜 → E has power series representation p on a ball of some radius and for
each positive radius it has some power series representation, then p converges to f on the whole
𝕜.
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 cardinal k, and attribute z to the indices in s and
y to the indices outside of s.
In this paragraph, we implement this. The new power series is called p.change_origin 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.
A term of formal_multilinear_series.change_origin_series.
Given a formal multilinear series p and a point x in its ball of convergence,
p.change_origin x is a formal multilinear series such that
p.sum (x+y) = (p.change_origin x).sum y when this makes sense. Each term of p.change_origin x
is itself an analytic function of x given by the series p.change_origin_series. Each term in
change_origin_series is the sum of change_origin_series_term's over all s of cardinality l.
The definition is such that
p.change_origin_series_term k l s hs (λ _, x) (λ _, y) = p (k + l) (s.piecewise (λ _, x) (λ _, y))
Equations
- p.change_origin_series_term k l s hs = ⇑(continuous_multilinear_map.curry_fin_finset 𝕜 E F hs _) (p (k + l))
The power series for f.change_origin k.
Given a formal multilinear series p and a point x in its ball of convergence,
p.change_origin x is a formal multilinear series such that
p.sum (x+y) = (p.change_origin x).sum y when this makes sense. Its k-th term is the sum of
the series p.change_origin_series k.
Equations
- p.change_origin_series k = λ (l : ℕ), finset.univ.sum (λ (s : {s // s.card = l}), p.change_origin_series_term k l ↑s _)
Changing the origin of a formal multilinear series p, so that
p.sum (x+y) = (p.change_origin x).sum y when this makes sense.
Equations
- p.change_origin x = λ (k : ℕ), (p.change_origin_series k).sum x
An auxiliary equivalence useful in the proofs about
formal_multilinear_series.change_origin_series: 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
- formal_multilinear_series.change_origin_index_equiv = {to_fun := λ (s : Σ (k l : ℕ), {s // s.card = l}), ⟨s.fst + s.snd.fst, ↑(s.snd.snd)⟩, inv_fun := λ (s : Σ (n : ℕ), finset (fin n)), ⟨s.fst - finset.card s.snd, ⟨finset.card s.snd, ⟨finset.map (fin.cast _).to_equiv.to_embedding s.snd, _⟩⟩⟩, left_inv := formal_multilinear_series.change_origin_index_equiv._proof_3, right_inv := formal_multilinear_series.change_origin_index_equiv._proof_4}
The radius of convergence of p.change_origin x is at least p.radius - ‖x‖. In other words,
p.change_origin x is well defined on the largest ball contained in the original ball of
convergence.
Summing the series p.change_origin x at a point y gives back p (x + y)
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.change_origin.
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.
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.
A function f : 𝕜 → E has p as power series expansion at a point z₀ iff it is the sum of
p in a neighborhood of z₀. This makes some proofs easier by hiding the fact that
has_fpower_series_at depends on p.radius.