Entire power series

A power series f = ∑ aₙ Xⁿ over a normed ring is entire when it is restricted at every real radius, that is, ‖aₙ‖ rⁿ → 0 for every r. Over a complete ultrametric ring the sum ∑ aₙ bⁿ of such a series then converges at every b, not only on a closed disc of some fixed radius. Entire series are the natural home of Fredholm determinants of compact operators and of their factorisations by polynomials.

Restrictedness at a radius r implies restrictedness at every radius s with |s| ≤ |r|, so it suffices to test positive radii (PowerSeries.isEntire_iff_forall_pos), or the radii along any sequence tending to infinity (PowerSeries.isEntire_iff_of_tendsto). Over any normed ring, the entire series form the subring PowerSeries.IsEntire.subring. Entire series are stable under Hasse derivatives, rescaling f(X) ↦ f(aX) and coefficientwise application of bounded ring homomorphisms.

Over a normed ring with ‖a‖ < 1, the series ∑ a^(n²) Xⁿ is entire (PowerSeries.isEntire_mk_pow_sq), while for a ≠ 0 and a multiplicative norm the series ∑ aⁿ Xⁿ is not, failing to be restricted at the radius ‖a‖⁻¹ (PowerSeries.not_isEntire_mk_pow), although it is restricted at every radius r with |r| < ‖a‖⁻¹. These are the standard examples separating entire series from series restricted at a fixed radius.

Main definitions

• PowerSeries.IsEntire: f is restricted at every real radius.
• PowerSeries.IsEntire.subring: the subring of entire series.
• PowerSeries.IsEntire.polynomialHom: the inclusion of polynomials into that subring.

Main results

• PowerSeries.isEntire_iff: the defining condition, for use outside this file.
• PowerSeries.isEntire_iff_forall_pos and PowerSeries.isEntire_iff_of_tendsto: entireness can be tested at positive radii, or along radii tending to infinity.
• PowerSeries.IsEntire.add, PowerSeries.IsEntire.mul, PowerSeries.isEntire_coe and their companions: entire series form a subring containing the polynomials.
• PowerSeries.IsEntire.hasseDeriv, PowerSeries.IsEntire.derivative, PowerSeries.IsEntire.rescale and PowerSeries.IsEntire.map: entireness is preserved by Hasse derivatives, rescaling and bounded coefficient maps.
• PowerSeries.IsEntire.summable_norm_coeff_mul_pow: ∑ ‖aₙ‖ tⁿ converges for every real t.
• PowerSeries.IsEntire.mk_coeff_succ: dropping the constant term and dividing by X keeps a series entire.
• PowerSeries.IsEntire.eq_C_of_mul_eq_one and PowerSeries.IsEntire.isUnit_iff: over an ultrametric normed field, the units of the ring of entire series are the nonzero constants, since the Gauss norm is multiplicative and a nonconstant entire series has unbounded Gauss norms.

References

• R. Coleman, p-adic Banach spaces and families of modular forms, Invent. Math. 127 (1997), 417–479, Appendix A.
• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85.

def PowerSeries.IsEntire {R : Type u_1} [NormedRing R] (f : PowerSeries R) : Prop

A power series ∑ aₙ Xⁿ is entire when it is restricted at every real radius r, that is, ‖aₙ‖ rⁿ → 0.

theorem PowerSeries.isEntire_iff {R : Type u_1} [NormedRing R] {f : PowerSeries R} : f.IsEntire ↔ ∀ (r : ℝ), IsRestricted r f

A series is entire exactly when it is restricted at every real radius.

theorem PowerSeries.IsEntire.isRestricted {R : Type u_1} [NormedRing R] {f : PowerSeries R} (hf : f.IsEntire) (r : ℝ) : IsRestricted r f

An entire series is restricted at every radius.

theorem PowerSeries.isEntire_iff_forall_pos {R : Type u_1} [NormedRing R] {f : PowerSeries R} : f.IsEntire ↔ ∀ (r : ℝ), 0 < r → IsRestricted r f

Entireness only needs to be checked at positive radii.

theorem PowerSeries.isEntire_iff_of_tendsto {R : Type u_1} [NormedRing R] {f : PowerSeries R} {ι : Type u_2} {l : Filter ι} [l.NeBot] {ρ : ι → ℝ} (hρ : Filter.Tendsto ρ l Filter.atTop) : f.IsEntire ↔ ∀ (i : ι), IsRestricted (ρ i) f

Entireness only needs to be checked along a family of radii tending to infinity, for instance at the radii n : ℕ.

@[simp]

theorem PowerSeries.isEntire_zero {R : Type u_1} [NormedRing R] : IsEntire 0

The zero series is entire.

@[simp]

theorem PowerSeries.isEntire_one {R : Type u_1} [NormedRing R] : IsEntire 1

The constant series 1 is entire.

@[simp]

theorem PowerSeries.isEntire_C {R : Type u_1} [NormedRing R] (a : R) : (C a).IsEntire

Constant series are entire.

@[simp]

theorem PowerSeries.isEntire_monomial {R : Type u_1} [NormedRing R] (n : ℕ) (a : R) : ((monomial n) a).IsEntire

Monomials are entire.

@[simp]

theorem PowerSeries.isEntire_X {R : Type u_1} [NormedRing R] : X.IsEntire

The variable X is entire.

@[simp]

theorem PowerSeries.isEntire_coe {R : Type u_1} [NormedRing R] (p : Polynomial R) : (↑p).IsEntire

Every polynomial is entire.

theorem PowerSeries.IsEntire.add {R : Type u_1} [NormedRing R] {f g : PowerSeries R} (hf : f.IsEntire) (hg : g.IsEntire) : (f + g).IsEntire

A sum of entire series is entire.

theorem PowerSeries.IsEntire.neg {R : Type u_1} [NormedRing R] {f : PowerSeries R} (hf : f.IsEntire) : (-f).IsEntire

The negative of an entire series is entire.

theorem PowerSeries.IsEntire.sub {R : Type u_1} [NormedRing R] {f g : PowerSeries R} (hf : f.IsEntire) (hg : g.IsEntire) : (f - g).IsEntire

A difference of entire series is entire.

theorem PowerSeries.IsEntire.smul {R : Type u_1} [NormedRing R] {f : PowerSeries R} (a : R) (hf : f.IsEntire) : (a • f).IsEntire

A scalar multiple a • f of an entire series is entire.

theorem PowerSeries.IsEntire.sum {R : Type u_1} [NormedRing R] {ι : Type u_2} {s : Finset ι} {f : ι → PowerSeries R} (hf : ∀ i ∈ s, (f i).IsEntire) : (∑ i ∈ s, f i).IsEntire

A finite sum of entire series is entire.

theorem PowerSeries.IsEntire.map {R : Type u_1} [NormedRing R] {f : PowerSeries R} {S : Type u_2} [NormedRing S] (hf : f.IsEntire) (φ : R →+* S) {C : ℝ} (hφ : ∀ (x : R), ‖φ x‖ ≤ C * ‖x‖) : ((PowerSeries.map φ) f).IsEntire

A bounded ring homomorphism φ, ‖φ x‖ ≤ C ‖x‖, maps entire series to entire series coefficientwise.

theorem PowerSeries.isEntire_mk_pow_sq {R : Type u_1} [NormedRing R] {a : R} (ha : ‖a‖ < 1) : (mk fun (n : ℕ) => a ^ n ^ 2).IsEntire

Over a normed ring, if ‖a‖ < 1 then ∑ a^(n²) Xⁿ is entire: at the radius r, its weighted coefficient norms are bounded by (‖a‖ⁿ r)ⁿ.

theorem PowerSeries.not_isEntire_mk_pow {R : Type u_1} [NormedRing R] [NormMulClass R] {a : R} (ha : a ≠ 0) : ¬(mk fun (n : ℕ) => a ^ n).IsEntire

Over a ring with multiplicative norm, if a ≠ 0 then ∑ aⁿ Xⁿ is not entire: its weighted coefficient norms at the radius ‖a‖⁻¹ are all 1.

theorem PowerSeries.IsEntire.mul {R : Type u_1} [NormedRing R] {f g : PowerSeries R} (hf : f.IsEntire) (hg : g.IsEntire) : (f * g).IsEntire

A product of entire series is entire.

theorem PowerSeries.IsEntire.pow {R : Type u_1} [NormedRing R] {f : PowerSeries R} (hf : f.IsEntire) (n : ℕ) : (f ^ n).IsEntire

A power of an entire series is entire.

theorem PowerSeries.IsEntire.hasseDeriv {R : Type u_1} [NormedRing R] {f : PowerSeries R} (hf : f.IsEntire) (k : ℕ) : ((PowerSeries.hasseDeriv k) f).IsEntire

Hasse derivatives of entire series are entire. The polynomial growth of the binomial coefficient is absorbed by testing the original series at a larger radius.

theorem PowerSeries.IsEntire.summable_norm_coeff_mul_pow {R : Type u_1} [NormedRing R] {f : PowerSeries R} (hf : f.IsEntire) (t : ℝ) : Summable fun (n : ℕ) => ‖(coeff n) f‖ * t ^ n

For an entire series f = ∑ aₙ Xⁿ, the series ∑ ‖aₙ‖ tⁿ converges for every real t.

theorem PowerSeries.IsEntire.mk_coeff_succ {R : Type u_1} [NormedRing R] {f : PowerSeries R} (hf : f.IsEntire) : (mk fun (n : ℕ) => (coeff (n + 1)) f).IsEntire

The series ∑ aₙ₊₁ Xⁿ obtained from an entire series by dropping the constant term and dividing by X is entire.

noncomputable def PowerSeries.IsEntire.subring (R : Type u_1) [NormedRing R] : Subring (PowerSeries R)

The entire power series form a subring.

@[simp]

theorem PowerSeries.IsEntire.mem_subring {R : Type u_1} [NormedRing R] {f : PowerSeries R} : f ∈ IsEntire.subring R ↔ f.IsEntire

Membership in the subring of entire series is entireness.

noncomputable def PowerSeries.IsEntire.polynomialHom {R : Type u_1} [NormedRing R] : Polynomial R →+* ↥(IsEntire.subring R)

The inclusion of polynomials into entire series.

@[simp]

theorem PowerSeries.IsEntire.coe_polynomialHom {R : Type u_1} [NormedRing R] (p : Polynomial R) : ↑(polynomialHom p) = ↑p

Polynomial inclusion has the usual underlying formal power series.

theorem PowerSeries.IsEntire.subring_le_isRestrictedSubring {R : Type u_1} [NormedRing R] [IsUltrametricDist R] (r : ℝ) : IsEntire.subring R ≤ IsRestricted.subring r

Over an ultrametric ring, every entire series is restricted at each radius r, so the subring of entire series lies in the restricted subring at r.

theorem PowerSeries.IsEntire.rescale {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} (hf : f.IsEntire) (a : R) : ((PowerSeries.rescale a) f).IsEntire

If f(X) is entire, so is f(aX) for every a.

theorem PowerSeries.IsEntire.derivative {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} (hf : f.IsEntire) : (PowerSeries.derivative f).IsEntire

The derivative of an entire series is entire.

theorem PowerSeries.IsEntire.eq_C_of_mul_eq_one {K : Type u_1} [NormedField K] [IsUltrametricDist K] {f g : PowerSeries K} (hf : f.IsEntire) (hg : g.IsEntire) (h : f * g = 1) : f = C (constantCoeff f)

Entire units are constant. Over an ultrametric normed field, if the product of two entire series is 1, then each of them is a constant.

theorem PowerSeries.IsEntire.isUnit_iff {K : Type u_1} [NormedField K] [IsUltrametricDist K] {F : ↥(IsEntire.subring K)} : IsUnit F ↔ ∃ (c : K), c ≠ 0 ∧ ↑F = C c

The units of the ring of entire series over an ultrametric normed field are the nonzero constants.