Documentation

Mathlib.Analysis.Analytic.CPolynomial

We specialize the theory fo 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.

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

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 :

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 ∈ EMetric.ball 0 r → HasSum (fun (n : ℕ) => (p n) fun (x : Fin n) => y) (f (x + y))
finite : ∀ (m : ℕ), n ≤ m → p m = 0

Instances For

theorem HasFiniteFPowerSeriesOnBall.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 : ℕ} {r : ENNReal} (self : HasFiniteFPowerSeriesOnBall f p x n r) (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 ∈ EMetric.ball 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 : ℕ) :

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 0and pₙ = 0 for n ≤ m.

Equations

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

Instances For

theorem HasFiniteFPowerSeriesAt.toHasFPowerSeriesAt {𝕜 : 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) :

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

Instances For

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) :

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

Instances For

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 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 : E → 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 (EMetric.ball x r)) :

HasFiniteFPowerSeriesOnBall g p x n r

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 : ENNReal} {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 : E → 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 hasFiniteFPowerSeriesOnBall_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {c : F} {e : E} :

HasFiniteFPowerSeriesOnBall (fun (x : E) => c) (constFormalMultilinearSeries 𝕜 E c) e 1 ⊤

theorem hasFiniteFPowerSeriesAt_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {c : F} {e : E} :

HasFiniteFPowerSeriesAt (fun (x : E) => c) (constFormalMultilinearSeries 𝕜 E c) e 1

theorem CPolynomialAt_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {v : F} :

CPolynomialAt 𝕜 (fun (x : E) => v) x

theorem CPolynomialOn_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {v : F} {s : Set E} :

CPolynomialOn 𝕜 (fun (x : E) => v) s

theorem HasFiniteFPowerSeriesOnBall.add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {pg : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} {m : ℕ} (hf : HasFiniteFPowerSeriesOnBall f pf x n r) (hg : HasFiniteFPowerSeriesOnBall g pg x m r) :

HasFiniteFPowerSeriesOnBall (f + g) (pf + pg) x (max n m) r

theorem HasFiniteFPowerSeriesAt.add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {pg : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} {m : ℕ} (hf : HasFiniteFPowerSeriesAt f pf x n) (hg : HasFiniteFPowerSeriesAt g pg x m) :

HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)

theorem CPolynomialAt.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → 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 : E → F} {g : E → F} {x : E} (h : f =ᶠ[nhds x] g) :

CPolynomialAt 𝕜 f x ↔ CPolynomialAt 𝕜 g x

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

CPolynomialAt 𝕜 (f + g) x

theorem HasFiniteFPowerSeriesOnBall.neg {𝕜 : 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} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f pf x n r) :

HasFiniteFPowerSeriesOnBall (-f) (-pf) x n r

theorem HasFiniteFPowerSeriesAt.neg {𝕜 : 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} {n : ℕ} (hf : HasFiniteFPowerSeriesAt f pf x n) :

HasFiniteFPowerSeriesAt (-f) (-pf) x n

theorem CPolynomialAt.neg {𝕜 : 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) :

CPolynomialAt 𝕜 (-f) x

theorem HasFiniteFPowerSeriesOnBall.sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {pg : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} {m : ℕ} (hf : HasFiniteFPowerSeriesOnBall f pf x n r) (hg : HasFiniteFPowerSeriesOnBall g pg x m r) :

HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (max n m) r

theorem HasFiniteFPowerSeriesAt.sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {pg : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} {m : ℕ} (hf : HasFiniteFPowerSeriesAt f pf x n) (hg : HasFiniteFPowerSeriesAt g pg x m) :

HasFiniteFPowerSeriesAt (f - g) (pf - pg) x (max n m)

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

CPolynomialAt 𝕜 (f - 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 : Set E} {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 : E → 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 : E → 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 : E → 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 : E → F} {g : E → F} {s : Set E} (hs : IsOpen s) (h : Set.EqOn f g s) :

CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s

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

CPolynomialOn 𝕜 (f + g) s

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

CPolynomialOn 𝕜 (f - 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 ∈ EMetric.ball 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 ∈ EMetric.ball 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 ∈ EMetric.ball 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 ∈ EMetric.ball 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 ∈ EMetric.ball 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 (EMetric.ball 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) :

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 ∈ EMetric.ball 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 : E) (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 : E} {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 : E} {y : E} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (h : y ∈ EMetric.ball 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 (EMetric.ball 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.