We specialize the theory of analytic functions to the case of functions that admit a development given by a finite formal multilinear series. We call them "continuously polynomial", which is abbreviated to CPolynomial. One reason to do that is that we no longer need a completeness assumption on the target space F to make the series converge, so some of the results are more general. The class of continuously polynomial functions includes functions defined by polynomials on a normed 𝕜-algebra and continuous multilinear maps.

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 : ℕ, and let f be a function from E to F.

• HasFiniteFPowerSeriesOnBall f p x n r: on the ball of center x with radius r, f (x + y) = ∑'_n pₘ yᵐ, and moreover pₘ = 0 if n ≤ m.
• HasFiniteFPowerSeriesAt f p x n: on some ball of center x with positive radius, holds HasFiniteFPowerSeriesOnBall f p x n r.
• CPolynomialAt 𝕜 f x: there exists a power series p and a natural number n such that holds HasFPowerSeriesAt f p x n.
• CPolynomialOn 𝕜 f s: the function f is analytic at every point of s.

In this file, we develop the basic properties of these notions, notably:

• If a function is continuously polynomial, then it is analytic, see HasFiniteFPowerSeriesOnBall.hasFPowerSeriesOnBall, HasFiniteFPowerSeriesAt.hasFPowerSeriesAt, CPolynomialAt.analyticAt and CPolynomialOn.analyticOnNhd.
• The sum of a finite formal power series with positive radius is well defined on the whole space, see FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite.
• If a function admits a finite power series in a ball, then it is continuously polynomial 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, which is finite (with the same bound as p) by changeOrigin_finite_of_finite. See HasFiniteFPowerSeriesOnBall.changeOrigin. It follows in particular that the set of points at which a given function is continuously polynomial is open, see isOpen_cpolynomialAt.

More API is available in the file Mathlib/Analysis/Analytic/CPolynomial.lean, with heavier imports.

structure HasFiniteFPowerSeriesOnBall {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (p : FormalMultilinearSeries 𝕜 E F) (x : E) (n : ℕ) (r : ENNReal) extends HasFPowerSeriesOnBall f p x r : Prop

Given a function f : E → F, a formal multilinear series p and n : ℕ, we say that f has p as a finite power series on the ball of radius r > 0 around x if f (x + y) = ∑' pₘ yᵐ for all ‖y‖ < r and pₙ = 0 for n ≤ m.

• r_le : r ≤ p.radius
• r_pos : 0 < r
• hasSum {y : E} : y ∈ Metric.eball 0 r → HasSum (fun (n : ℕ) => (p n) fun (x : Fin n) => y) (f (x + y))
• finite (m : ℕ) : n ≤ m → p m = 0

theorem HasFiniteFPowerSeriesOnBall.mk' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} {r : ENNReal} (finite : ∀ (m : ℕ), n ≤ m → p m = 0) (pos : 0 < r) (sum_eq : ∀ y ∈ Metric.eball 0 r, (∑ i ∈ Finset.range n, (p i) fun (x : Fin i) => y) = f (x + y)) : HasFiniteFPowerSeriesOnBall f p x n r

def HasFiniteFPowerSeriesAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (p : FormalMultilinearSeries 𝕜 E F) (x : E) (n : ℕ) : Prop

Given a function f : E → F, a formal multilinear series p and n : ℕ, we say that f has p as a finite power series around x if f (x + y) = ∑' pₙ yⁿ for all y in a neighborhood of 0 and pₙ = 0 for n ≤ m.

Equations

• HasFiniteFPowerSeriesAt f p x n = ∃ (r : ENNReal), HasFiniteFPowerSeriesOnBall f p x n r

theorem HasFiniteFPowerSeriesAt.hasFPowerSeriesAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} (hf : HasFiniteFPowerSeriesAt f p x n) : HasFPowerSeriesAt f p x

theorem HasFiniteFPowerSeriesAt.finite {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} (hf : HasFiniteFPowerSeriesAt f p x n) (m : ℕ) : n ≤ m → p m = 0

def CPolynomialAt (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (x : E) : Prop

Given a function f : E → F, we say that f is continuously polynomial (cpolynomial) at x if it admits a finite power series expansion around x.

Equations

• CPolynomialAt 𝕜 f x = ∃ (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ), HasFiniteFPowerSeriesAt f p x n

def CPolynomialOn (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (s : Set E) : Prop

Given a function f : E → F, we say that f is continuously polynomial on a set s if it is continuously polynomial around every point of s.

Equations

• CPolynomialOn 𝕜 f s = ∀ x ∈ s, CPolynomialAt 𝕜 f x

theorem HasFiniteFPowerSeriesOnBall.hasFiniteFPowerSeriesAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f p x n r) : HasFiniteFPowerSeriesAt f p x n

theorem HasFiniteFPowerSeriesAt.cpolynomialAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} (hf : HasFiniteFPowerSeriesAt f p x n) : CPolynomialAt 𝕜 f x

theorem HasFiniteFPowerSeriesOnBall.cpolynomialAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f p x n r) : CPolynomialAt 𝕜 f x

theorem CPolynomialAt.analyticAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (hf : CPolynomialAt 𝕜 f x) : AnalyticAt 𝕜 f x

theorem CPolynomialAt.analyticWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} (hf : CPolynomialAt 𝕜 f x) : AnalyticWithinAt 𝕜 f s x

theorem CPolynomialOn.analyticOnNhd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOnNhd 𝕜 f s

theorem CPolynomialOn.analyticOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOn 𝕜 f s

theorem HasFiniteFPowerSeriesOnBall.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (hg : Set.EqOn f g (Metric.eball x r)) : HasFiniteFPowerSeriesOnBall g p x n r

theorem HasFiniteFPowerSeriesOnBall.of_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {m n : ℕ} (h : HasFiniteFPowerSeriesOnBall f p x n r) (hmn : n ≤ m) : HasFiniteFPowerSeriesOnBall f p x m r

theorem HasFiniteFPowerSeriesAt.of_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {m n : ℕ} (h : HasFiniteFPowerSeriesAt f p x n) (hmn : n ≤ m) : HasFiniteFPowerSeriesAt f p x m

theorem HasFiniteFPowerSeriesOnBall.comp_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (y : E) : HasFiniteFPowerSeriesOnBall (fun (z : E) => f (z - y)) p (x + y) n r

If a function f has a finite power series p around x, then the function z ↦ f (z - y) has the same finite power series around x + y.

theorem HasFiniteFPowerSeriesOnBall.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r r' : ENNReal} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (r'_pos : 0 < r') (hr : r' ≤ r) : HasFiniteFPowerSeriesOnBall f p x n r'

theorem HasFiniteFPowerSeriesAt.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} (hf : HasFiniteFPowerSeriesAt f p x n) (hg : f =ᶠ[nhds x] g) : HasFiniteFPowerSeriesAt g p x n

theorem HasFiniteFPowerSeriesAt.eventually {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} (hf : HasFiniteFPowerSeriesAt f p x n) : ∀ᶠ (r : ENNReal) in nhdsWithin 0 (Set.Ioi 0), HasFiniteFPowerSeriesOnBall f p x n r

theorem CPolynomialAt.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {x : E} (hf : CPolynomialAt 𝕜 f x) (hg : f =ᶠ[nhds x] g) : CPolynomialAt 𝕜 g x

theorem CPolynomialAt_congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {x : E} (h : f =ᶠ[nhds x] g) : CPolynomialAt 𝕜 f x ↔ CPolynomialAt 𝕜 g x

theorem CPolynomialOn.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s t : Set E} (hf : CPolynomialOn 𝕜 f t) (hst : s ⊆ t) : CPolynomialOn 𝕜 f s

theorem CPolynomialOn.congr' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {s : Set E} (hf : CPolynomialOn 𝕜 f s) (hg : f =ᶠ[nhdsSet s] g) : CPolynomialOn 𝕜 g s

theorem CPolynomialOn_congr' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {s : Set E} (h : f =ᶠ[nhdsSet s] g) : CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s

theorem CPolynomialOn.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {s : Set E} (hs : IsOpen s) (hf : CPolynomialOn 𝕜 f s) (hg : Set.EqOn f g s) : CPolynomialOn 𝕜 g s

theorem CPolynomialOn_congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {s : Set E} (hs : IsOpen s) (h : Set.EqOn f g s) : CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s

theorem ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (g : F →L[𝕜] G) (h : HasFiniteFPowerSeriesOnBall f p x n r) : HasFiniteFPowerSeriesOnBall (⇑g ∘ f) (g.compFormalMultilinearSeries p) x n r

If a function f has a finite power series p on a ball and g is a continuous linear map, then g ∘ f has the finite power series g ∘ p on the same ball.

theorem ContinuousLinearMap.comp_cpolynomialOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F} {s : Set E} (g : F →L[𝕜] G) (h : CPolynomialOn 𝕜 f s) : CPolynomialOn 𝕜 (⇑g ∘ f) s

If a function f is continuously polynomial on a set s and g is a continuous linear map, then g ∘ f is continuously polynomial on s.

theorem HasFiniteFPowerSeriesOnBall.eq_partialSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (y : E) : y ∈ Metric.eball 0 r → ∀ (m : ℕ), n ≤ m → f (x + y) = p.partialSum m y

If a function admits a finite power series expansion bounded by n, then it is equal to the mth partial sums of this power series at every point of the disk for n ≤ m.

theorem HasFiniteFPowerSeriesOnBall.eq_partialSum' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (y : E) : y ∈ Metric.eball x r → ∀ (m : ℕ), n ≤ m → f y = p.partialSum m (y - x)

Variant of the previous result with the variable expressed as y instead of x + y.

The particular cases where f has a finite power series bounded by 0 or 1.

theorem HasFiniteFPowerSeriesOnBall.eq_zero_of_bound_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFiniteFPowerSeriesOnBall f pf x 0 r) (y : E) : y ∈ Metric.eball x r → f y = 0

If f has a formal power series on a ball bounded by 0, then f is equal to 0 on the ball.

theorem HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : ∀ y ∈ Metric.eball x r, f y = 0) (r_pos : 0 < r) (hp : ∀ (n : ℕ), p n = 0) : HasFiniteFPowerSeriesOnBall f p x 0 r

theorem HasFiniteFPowerSeriesAt.eventually_zero_of_bound_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFiniteFPowerSeriesAt f pf x 0) : f =ᶠ[nhds x] 0

If f has a formal power series at x bounded by 0, then f is equal to 0 in a neighborhood of x.

theorem HasFiniteFPowerSeriesOnBall.eq_const_of_bound_one {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFiniteFPowerSeriesOnBall f pf x 1 r) (y : E) : y ∈ Metric.eball x r → f y = f x

If f has a formal power series on a ball bounded by 1, then f is constant equal to f x on the ball.

theorem HasFiniteFPowerSeriesAt.eventually_const_of_bound_one {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFiniteFPowerSeriesAt f pf x 1) : f =ᶠ[nhds x] fun (x_1 : E) => f x

If f has a formal power series at x bounded by 1, then f is constant equal to f x in a neighborhood of x.

theorem HasFiniteFPowerSeriesOnBall.continuousOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f p x n r) : ContinuousOn f (Metric.eball x r)

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

theorem HasFiniteFPowerSeriesAt.continuousAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} (hf : HasFiniteFPowerSeriesAt f p x n) : ContinuousAt f x

theorem CPolynomialAt.continuousAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (hf : CPolynomialAt 𝕜 f x) : ContinuousAt f x

theorem CPolynomialOn.continuousOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hf : CPolynomialOn 𝕜 f s) : ContinuousOn f s

theorem CPolynomialOn.continuous {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (fa : CPolynomialOn 𝕜 f Set.univ) : Continuous f

Continuously polynomial everywhere implies continuous

theorem FormalMultilinearSeries.sum_of_finite {𝕜 : 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 : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (x : E) : p.sum x = p.partialSum n x

theorem FormalMultilinearSeries.hasSum_of_finite {𝕜 : 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 : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (x : E) : HasSum (fun (n : ℕ) => (p n) fun (x_1 : Fin n) => x) (p.sum x)

A finite formal multilinear series sums to its sum at every point.

theorem FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite {𝕜 : 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 : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) : HasFiniteFPowerSeriesOnBall p.sum p 0 n ⊤

The sum of a finite power series p admits p as a power series.

theorem HasFiniteFPowerSeriesOnBall.sum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (h : HasFiniteFPowerSeriesOnBall f p x n r) {y : E} (hy : y ∈ Metric.eball 0 r) : f (x + y) = p.sum y

theorem FormalMultilinearSeries.continuousOn_of_finite {𝕜 : 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 : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) : Continuous p.sum

The sum of a finite power series is continuous.

We study what happens when we change the origin of a finite formal multilinear series p. The main point is that the new series p.changeOrigin x is still finite, with the same bound.

theorem FormalMultilinearSeries.changeOriginSeriesTerm_bound {𝕜 : 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 : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k l : ℕ) {s : Finset (Fin (k + l))} (hs : s.card = l) (hkl : n ≤ k + l) : p.changeOriginSeriesTerm k l s hs = 0

If p is a formal multilinear series such that p m = 0 for n ≤ m, then p.changeOriginSeriesTerm k l = 0 for n ≤ k + l.

theorem FormalMultilinearSeries.changeOriginSeries_finite_of_finite {𝕜 : 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 : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k : ℕ) {m : ℕ} : n ≤ k + m → p.changeOriginSeries k m = 0

If p is a finite formal multilinear series, then so is p.changeOriginSeries k for every k in ℕ. More precisely, if p m = 0 for n ≤ m, then p.changeOriginSeries k m = 0 for n ≤ k + m.

theorem FormalMultilinearSeries.changeOriginSeries_sum_eq_partialSum_of_finite {𝕜 : 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 : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k : ℕ) : (p.changeOriginSeries k).sum = (p.changeOriginSeries k).partialSum (n - k)

theorem FormalMultilinearSeries.changeOrigin_finite_of_finite {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) {k : ℕ} (hk : n ≤ k) : p.changeOrigin x k = 0

If p is a formal multilinear series such that p m = 0 for n ≤ m, then p.changeOrigin x k = 0 for n ≤ k.

theorem FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_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) {n : ℕ} (k : ℕ) (hn : ∀ (m : ℕ), n + k ≤ m → p m = 0) : HasFiniteFPowerSeriesOnBall (fun (x : E) => p.changeOrigin x k) (p.changeOriginSeries k) 0 n ⊤

theorem FormalMultilinearSeries.changeOrigin_eval_of_finite {𝕜 : 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 : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (x y : E) : (p.changeOrigin x).sum y = p.sum (x + y)

theorem FormalMultilinearSeries.cpolynomialAt_changeOrigin_of_finite {𝕜 : 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 : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k : ℕ) : CPolynomialAt 𝕜 (fun (x : E) => p.changeOrigin x k) 0

The terms of the formal multilinear series p.changeOrigin are continuously polynomial as we vary the origin

theorem HasFiniteFPowerSeriesOnBall.changeOrigin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {x y : E} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (h : ↑‖y‖₊ < r) : HasFiniteFPowerSeriesOnBall f (p.changeOrigin y) (x + y) n (r - ↑‖y‖₊)

theorem HasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {x y : E} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (h : y ∈ Metric.eball x r) : CPolynomialAt 𝕜 f y

If a function admits a finite power series expansion p on an open ball B (x, r), then it is continuously polynomial at every point of this ball.

theorem HasFiniteFPowerSeriesOnBall.cpolynomialOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {x : E} (hf : HasFiniteFPowerSeriesOnBall f p x n r) : CPolynomialOn 𝕜 f (Metric.eball x r)

theorem isOpen_cpolynomialAt (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) : IsOpen {x : E | CPolynomialAt 𝕜 f x}

For any function f from a normed vector space to a normed vector space, the set of points x such that f is continuously polynomial at x is open.

theorem CPolynomialAt.eventually_cpolynomialAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) : ∀ᶠ (y : E) in nhds x, CPolynomialAt 𝕜 f y

theorem CPolynomialAt.exists_mem_nhds_cpolynomialOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) : ∃ s ∈ nhds x, CPolynomialOn 𝕜 f s

theorem CPolynomialAt.exists_ball_cpolynomialOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) : ∃ (r : ℝ), 0 < r ∧ CPolynomialOn 𝕜 f (Metric.ball x r)

If f is continuously polynomial at a point, then it is continuously polynomial in a nonempty ball around that point.