# 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`.

source
def FormalMultilinearSeries.changeOriginSeriesTerm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) :
ContinuousMultilinearMap 𝕜 (fun (i : Fin l) => E) (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) => E) F)

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

source
theorem FormalMultilinearSeries.changeOriginSeriesTerm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) (x y : E) :
(((p.changeOriginSeriesTerm k l s hs) fun (x_1 : Fin l) => x) fun (x : Fin k) => y) = (p (k + l)) (s.piecewise (fun (x_1 : Fin (k + l)) => x) fun (x : Fin (k + l)) => y)
source
@[simp]
theorem FormalMultilinearSeries.norm_changeOriginSeriesTerm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) :
‖p.changeOriginSeriesTerm k l s hs‖ = ‖p (k + l)‖
source
@[simp]
theorem FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) :
‖p.changeOriginSeriesTerm k l s hs‖₊ = ‖p (k + l)‖₊
source
theorem FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) (x y : E) :
‖((p.changeOriginSeriesTerm k l s hs) fun (x_1 : Fin l) => x) fun (x : Fin k) => y‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k
source
def FormalMultilinearSeries.changeOriginSeries {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ) :
FormalMultilinearSeries 𝕜 E (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) => E) F)

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

- p.changeOriginSeries k l = ∑ s : { s : Finset (Fin (k + l)) // s.card = l }, p.changeOriginSeriesTerm k l ↑s ⋯

Instances For

source
theorem FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) :
‖p.changeOriginSeries k l‖₊ ≤ ∑' (x : { s : Finset (Fin (k + l)) // s.card = l }), ‖p (k + l)‖₊
source
theorem FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (x : E) :
‖(p.changeOriginSeries k l) fun (x_1 : Fin l) => x‖₊ ≤ ∑' (x_1 : { s : Finset (Fin (k + l)) // s.card = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l
source
def FormalMultilinearSeries.changeOrigin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (x : E) :
FormalMultilinearSeries 𝕜 E F

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

source
def FormalMultilinearSeries.changeOriginIndexEquiv :
(k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l } ≃ (n : ℕ) × Finset (Fin n)

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

source
@[simp]
theorem FormalMultilinearSeries.changeOriginIndexEquiv_apply_snd (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) :
(changeOriginIndexEquiv s).snd = ↑s.snd.snd
source
@[simp]
theorem FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_snd_snd_coe (s : (n : ℕ) × Finset (Fin n)) :
↑(changeOriginIndexEquiv.symm s).snd.snd = Finset.map (finCongr ⋯).toEmbedding s.snd
source
@[simp]
theorem FormalMultilinearSeries.changeOriginIndexEquiv_apply_fst (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) :
(changeOriginIndexEquiv s).fst = s.fst + s.snd.fst
source
@[simp]
theorem FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_snd_fst (s : (n : ℕ) × Finset (Fin n)) :
(changeOriginIndexEquiv.symm s).snd.fst = s.snd.card
source
@[simp]
theorem FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_fst (s : (n : ℕ) × Finset (Fin n)) :
(changeOriginIndexEquiv.symm s).fst = s.fst - s.snd.card
source
theorem FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {x y : E} (n : ℕ) (t : Finset (Fin n)) :
have s := changeOriginIndexEquiv.symm ⟨n, t⟩; (((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun (x_1 : Fin s.snd.fst) => x) fun (x : Fin s.fst) => y) = (p n) (t.piecewise (fun (x_1 : Fin n) => x) fun (x : Fin n) => y)
source
theorem FormalMultilinearSeries.changeOriginSeries_summable_aux₁ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r r' : NNReal} (hr : ↑r + ↑r' < p.radius) :
Summable fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) => ‖p (s.fst + s.snd.fst)‖₊ * r ^ s.snd.fst * r' ^ s.fst
source
theorem FormalMultilinearSeries.changeOriginSeries_summable_aux₂ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (hr : ↑r < p.radius) (k : ℕ) :
Summable fun (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) => ‖p (k + s.fst)‖₊ * r ^ s.fst
source
theorem FormalMultilinearSeries.changeOriginSeries_summable_aux₃ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (hr : ↑r < p.radius) (k : ℕ) :
Summable fun (l : ℕ) => ‖p.changeOriginSeries k l‖₊ * r ^ l
source
theorem FormalMultilinearSeries.le_changeOriginSeries_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ) :
p.radius ≤ (p.changeOriginSeries k).radius
source
theorem FormalMultilinearSeries.nnnorm_changeOrigin_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (k : ℕ) (h : ↑‖x‖₊ < p.radius) :
‖p.changeOrigin x k‖₊ ≤ ∑' (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst
source
theorem FormalMultilinearSeries.changeOrigin_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} :
p.radius - ↑‖x‖₊ ≤ (p.changeOrigin x).radius

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.

source
def FormalMultilinearSeries.derivSeries {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) :
FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)

`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

source
theorem FormalMultilinearSeries.radius_le_radius_derivSeries {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) :
p.radius ≤ p.derivSeries.radius
source
theorem FormalMultilinearSeries.derivSeries_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hp : p (n + 1) = 0) :
p.derivSeries n = 0
source
theorem FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ) (hr : 0 < p.radius) :
HasFPowerSeriesOnBall (fun (x : E) => p.changeOrigin x k) (p.changeOriginSeries k) 0 p.radius
source
theorem FormalMultilinearSeries.changeOrigin_eval {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) {x y : E} (h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius) :
(p.changeOrigin x).sum y = p.sum (x + y)

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

source
theorem FormalMultilinearSeries.analyticAt_changeOrigin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) (rp : p.radius > 0) (n : ℕ) :
AnalyticAt 𝕜 (fun (x : E) => p.changeOrigin x n) 0

Power series terms are analytic as we vary the origin

source
theorem HasFPowerSeriesWithinOnBall.changeOrigin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x y : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : ‖y‖ₑ < r) (hy : x + y ∈ insert x s) :
HasFPowerSeriesWithinOnBall f (p.changeOrigin y) s (x + y) (r - ‖y‖ₑ)

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`.

source
theorem HasFPowerSeriesOnBall.changeOrigin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x y : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (h : ↑‖y‖₊ < r) :
HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ↑‖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.changeOrigin`.

source
theorem HasFPowerSeriesWithinOnBall.analyticWithinAt_of_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x y : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : y ∈ insert x s ∩ EMetric.ball x r) :
AnalyticWithinAt 𝕜 f s y

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.

source
theorem HasFPowerSeriesOnBall.analyticAt_of_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x y : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (h : y ∈ EMetric.ball x r) :
AnalyticAt 𝕜 f y

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.

source
theorem HasFPowerSeriesWithinOnBall.analyticOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) :
AnalyticOn 𝕜 f (insert x s ∩ EMetric.ball x r)
source
theorem HasFPowerSeriesOnBall.analyticOnNhd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) :
AnalyticOnNhd 𝕜 f (EMetric.ball x r)
source
theorem isOpen_analyticAt (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (f : E → F) :
IsOpen {x : E | AnalyticAt 𝕜 f x}

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.

source
theorem AnalyticAt.eventually_analyticAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {x : E} (h : AnalyticAt 𝕜 f x) :
∀ᶠ (y : E) in nhds x, AnalyticAt 𝕜 f y
source
theorem AnalyticAt.exists_mem_nhds_analyticOnNhd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {x : E} (h : AnalyticAt 𝕜 f x) :
∃ s ∈ nhds x, AnalyticOnNhd 𝕜 f s
source
theorem AnalyticAt.exists_ball_analyticOnNhd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {x : E} (h : AnalyticAt 𝕜 f x) :
∃ (r : ℝ), 0 < r ∧ AnalyticOnNhd 𝕜 f (Metric.ball x r)

If we're analytic at a point, we're analytic in a nonempty ball

source
theorem FormalMultilinearSeries.analyticOnNhd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F} :
AnalyticOnNhd 𝕜 p.sum (EMetric.ball 0 p.radius)

Sum of series is analytic on its ball of convergence.