mathlib documentation

analysis.analytic.basic

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 : ℕ.

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

We develop the basic properties of these notions, notably:

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.

The radius of a formal multilinear series

def formal_multilinear_series.radius {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] :

The radius of a formal multilinear series is the largest r such that the sum Σ pₙ yⁿ converges for all ∥y∥ < r.

Equations
theorem formal_multilinear_series.le_radius_of_bound {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p : formal_multilinear_series 𝕜 E F) (C : ℝ≥0) {r : ℝ≥0} :
(∀ (n : ), (nnnorm (p n)) * r ^ n C)r p.radius

If ∥pₙ∥ rⁿ is bounded in n, then the radius of p is at least r.

theorem formal_multilinear_series.bound_of_lt_radius {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p : formal_multilinear_series 𝕜 E F) {r : ℝ≥0} :
r < p.radius(∃ (C : ℝ≥0), ∀ (n : ), (nnnorm (p n)) * r ^ n C)

For r strictly smaller than the radius of p, then ∥pₙ∥ rⁿ is bounded.

theorem formal_multilinear_series.geometric_bound_of_lt_radius {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p : formal_multilinear_series 𝕜 E F) {r : ℝ≥0} :
r < p.radius(∃ (a C : ℝ≥0), a < 1 ∀ (n : ), (nnnorm (p n)) * r ^ n C * a ^ n)

For r strictly smaller than the radius of p, then ∥pₙ∥ rⁿ tends to zero exponentially.

theorem formal_multilinear_series.min_radius_le_radius_add {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p q : formal_multilinear_series 𝕜 E F) :

The radius of the sum of two formal series is at least the minimum of their two radii.

theorem formal_multilinear_series.radius_neg {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p : formal_multilinear_series 𝕜 E F) :

def formal_multilinear_series.sum {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] :
formal_multilinear_series 𝕜 E FE → F

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.

Equations
def formal_multilinear_series.partial_sum {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] :
formal_multilinear_series 𝕜 E FE → F

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
theorem formal_multilinear_series.partial_sum_continuous {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p : formal_multilinear_series 𝕜 E F) (n : ) :

The partial sums of a formal multilinear series are continuous.

Expanding a function as a power series

structure has_fpower_series_on_ball {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] :
(E → F)formal_multilinear_series 𝕜 E FE → ennreal → Prop

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.

def has_fpower_series_at {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] :
(E → F)formal_multilinear_series 𝕜 E FE → Prop

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
def analytic_at (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] :
(E → F)E → Prop

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
theorem has_fpower_series_on_ball.has_fpower_series_at {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} :

theorem has_fpower_series_at.analytic_at {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} :

theorem has_fpower_series_on_ball.analytic_at {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} :

theorem has_fpower_series_on_ball.radius_pos {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} :

theorem has_fpower_series_at.radius_pos {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} :

theorem has_fpower_series_on_ball.mono {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} {r r' : ennreal} :
has_fpower_series_on_ball f p x r0 < r'r' rhas_fpower_series_on_ball f p x r'

theorem has_fpower_series_on_ball.add {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f g : E → F} {pf pg : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} :

theorem has_fpower_series_at.add {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f g : E → F} {pf pg : formal_multilinear_series 𝕜 E F} {x : E} :
has_fpower_series_at f pf xhas_fpower_series_at g pg xhas_fpower_series_at (f + g) (pf + pg) x

theorem analytic_at.add {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f g : E → F} {x : E} :
analytic_at 𝕜 f xanalytic_at 𝕜 g xanalytic_at 𝕜 (f + g) x

theorem has_fpower_series_on_ball.neg {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {pf : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} :

theorem has_fpower_series_at.neg {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {pf : formal_multilinear_series 𝕜 E F} {x : E} :

theorem analytic_at.neg {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {x : E} :
analytic_at 𝕜 f xanalytic_at 𝕜 (-f) x

theorem has_fpower_series_on_ball.sub {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f g : E → F} {pf pg : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} :

theorem has_fpower_series_at.sub {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f g : E → F} {pf pg : formal_multilinear_series 𝕜 E F} {x : E} :
has_fpower_series_at f pf xhas_fpower_series_at g pg xhas_fpower_series_at (f - g) (pf - pg) x

theorem analytic_at.sub {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f g : E → F} {x : E} :
analytic_at 𝕜 f xanalytic_at 𝕜 g xanalytic_at 𝕜 (f - g) x

theorem has_fpower_series_on_ball.coeff_zero {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {pf : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} (hf : has_fpower_series_on_ball f pf x r) (v : fin 0 → E) :
(pf 0) v = f x

theorem has_fpower_series_at.coeff_zero {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {pf : formal_multilinear_series 𝕜 E F} {x : E} (hf : has_fpower_series_at f pf x) (v : fin 0 → E) :
(pf 0) v = f x

theorem has_fpower_series_on_ball.uniform_geometric_approx {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} {r' : ℝ≥0} :
has_fpower_series_on_ball f p x rr' < r(∃ (a C : ℝ≥0), a < 1 ∀ (y : E), y metric.ball 0 r'∀ (n : ), f (x + y) - p.partial_sum n y (C) * a ^ n)

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.

theorem has_fpower_series_on_ball.tendsto_uniformly_on {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} {r' : ℝ≥0} :
has_fpower_series_on_ball f p x rr' < rtendsto_uniformly_on (λ (n : ) (y : E), p.partial_sum n y) (λ (y : E), f (x + y)) filter.at_top (metric.ball 0 r')

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.

theorem has_fpower_series_on_ball.tendsto_locally_uniformly_on {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} :
has_fpower_series_on_ball f p x rtendsto_locally_uniformly_on (λ (n : ) (y : E), p.partial_sum n y) (λ (y : E), f (x + y)) filter.at_top (emetric.ball 0 r)

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.

theorem has_fpower_series_on_ball.tendsto_uniformly_on' {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} {r' : ℝ≥0} :
has_fpower_series_on_ball f p x rr' < rtendsto_uniformly_on (λ (n : ) (y : E), p.partial_sum n (y - x)) f filter.at_top (metric.ball x r')

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.

theorem has_fpower_series_on_ball.tendsto_locally_uniformly_on' {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} :

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.

theorem has_fpower_series_on_ball.continuous_on {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} :

If a function admits a power series expansion on a disk, then it is continuous there.

theorem has_fpower_series_at.continuous_at {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} :

theorem analytic_at.continuous_at {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {x : E} :
analytic_at 𝕜 f xcontinuous_at f x

theorem formal_multilinear_series.has_fpower_series_on_ball {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] (p : formal_multilinear_series 𝕜 E F) :

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.

theorem has_fpower_series_on_ball.sum {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x : E} {r : ennreal} [complete_space F] (h : has_fpower_series_on_ball f p x r) {y : E} :
y emetric.ball 0 rf (x + y) = p.sum y

theorem formal_multilinear_series.continuous_on {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {p : formal_multilinear_series 𝕜 E F} [complete_space F] :

The sum of a converging power series is continuous in its disk of convergence.

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} \choose n k p_n y^{n-k} z^k = sum_{k} (sum_{n} \choose n k p_n y^{n-k}) z^k. $$ The corresponding power series has thus a k-th coefficient equal to \sum_{n} \choose 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.

def formal_multilinear_series.change_origin {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] :

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.

Here, we don't use the bracket notation ⟨n, s, hs⟩ in place of the argument i in the lambda, as this leads to a bad definition with auxiliary _match statements, but we will try to use pattern matching in lambdas as much as possible in the proofs below to increase readability.

Equations
theorem formal_multilinear_series.change_origin_summable_aux1 {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p : formal_multilinear_series 𝕜 E F) {x : E} {r : ℝ≥0} :
(nnnorm x) + r < p.radiussummable (λ (_x : Σ (n : ), finset (fin n)), (λ (_a : Σ (n : ), finset (fin n)), _a.cases_on (λ (fst : ) (snd : finset (fin fst)), id_rhs ((p fst * x ^ (fst - snd.card)) * r ^ snd.card))) _x)

Auxiliary lemma controlling the summability of the sequence appearing in the definition of p.change_origin, first version.

theorem formal_multilinear_series.change_origin_summable_aux2 {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p : formal_multilinear_series 𝕜 E F) {x : E} {r : ℝ≥0} :
(nnnorm x) + r < p.radiussummable (λ (_x : Σ (k n : ), {s // s.card = k}), (λ (_a : Σ (k n : ), {s // s.card = k}), _a.cases_on (λ (fst : ) (snd : Σ (n : ), {s // s.card = fst}), snd.cases_on (λ (snd_fst : ) (snd_snd : {s // s.card = fst}), snd_snd.cases_on (λ (snd_snd_val : finset (fin snd_fst)) (snd_snd_property : snd_snd_val.card = fst), id_rhs ((p snd_fst).restr snd_snd_val snd_snd_property x * r ^ fst))))) _x)

Auxiliary lemma controlling the summability of the sequence appearing in the definition of p.change_origin, second version.

def formal_multilinear_series.change_origin_summable_aux_j (k : ) :
(Σ (n : ), {s // s.card = k})(Σ (k n : ), {s // s.card = k})

An auxiliary definition for change_origin_radius.

Equations
theorem formal_multilinear_series.change_origin_summable_aux3 {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p : formal_multilinear_series 𝕜 E F) {x : E} (k : ) :
(nnnorm x) < p.radiussummable (λ (_x : Σ (n : ), {s // s.card = k}), (λ (_a : Σ (n : ), {s // s.card = k}), _a.cases_on (λ (fst : ) (snd : {s // s.card = k}), snd.cases_on (λ (snd_val : finset (fin fst)) (snd_property : snd_val.card = k), id_rhs (p fst).restr snd_val snd_property x))) _x)

Auxiliary lemma controlling the summability of the sequence appearing in the definition of p.change_origin, third version.

theorem formal_multilinear_series.change_origin_radius {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p : formal_multilinear_series 𝕜 E F) {x : E} :

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.

theorem formal_multilinear_series.change_origin_has_sum {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p : formal_multilinear_series 𝕜 E F) {x : E} [complete_space F] (k : ) :
(nnnorm x) < p.radiushas_sum (λ (i : Σ (n : ), {s // s.card = k}), (p i.fst).restr i.snd.val _ x) (p.change_origin x k)

The k-th coefficient of p.change_origin is the sum of a summable series.

theorem formal_multilinear_series.change_origin_eval {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p : formal_multilinear_series 𝕜 E F) {x y : E} [complete_space F] :
(nnnorm x) + (nnnorm y) < p.radiushas_sum (λ (k : ), (p.change_origin x k) (λ (i : fin k), y)) (p.sum (x + y))

Summing the series p.change_origin x at a point y gives back p (x + y)

theorem has_fpower_series_on_ball.change_origin {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x y : E} {r : ennreal} :

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.

theorem has_fpower_series_on_ball.analytic_at_of_mem {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x y : E} {r : ennreal} :
has_fpower_series_on_ball f p x ry emetric.ball x ranalytic_at 𝕜 f y

theorem is_open_analytic_at (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] (f : E → F) :
is_open {x : E | analytic_at 𝕜 f x}