Good zeros of entire power series

Let f be a power series over a commutative topological ring R and write Δᵏ f for its Hasse derivatives (PowerSeries.hasseDeriv). The series f has a good zero of order h at a : R if (Δʲ f)(a) = 0 for every j < h and (Δʰ f)(a) is a unit. Order zero means that f(a) itself is a unit. Over a field this is a zero of multiplicity exactly h; over a general coefficient ring, the unit condition on the first nonvanishing Hasse derivative is what allows X - a to be split off exactly h times, as needed for the spectral projectors attached to zeros of Fredholm determinants. No factorial is inverted, so the notion keeps its meaning in positive characteristic and over rings with nilpotents.

For an entire series over a complete normed ring, the good zeros of order h at a are exactly the factorisations f = (X - a)ʰ g with g entire and g(a) a unit (PowerSeries.IsEntire.isGoodZero_iff). This follows from the evaluated Leibniz rule (Δʲ ((X - a)ᵐ g))(a) = (Δʲ⁻ᵐ g)(a) for m ≤ j, and 0 otherwise (PowerSeries.IsEntire.evalAt_hasseDeriv_X_sub_C_pow_mul), together with the factor theorem for entire series (PowerSeries.IsEntire.exists_eq_X_sub_C_pow_mul). Consequently orders add under products, and when f(0) = 1 a good zero of positive order is a unit, so the factor (X - a)ʰ may be renormalised to (1 - a⁻¹ X)ʰ.

Over a complete normed field every zero of a nonzero entire series has a finite order (PowerSeries.IsEntire.exists_isGoodZero). The values (Δⁿ f)(a) are the coefficients of the Taylor translate of f at a, which is nonzero because Taylor translation is injective on entire series (PowerSeries.IsEntire.taylor_eq_zero_iff); the order is the first index of a nonzero coefficient. No discreteness of the valuation, Weierstrass product or identity theorem is used.

Main definitions

• PowerSeries.IsGoodZero f a h: f has a good zero of order h at a.

Main results

• PowerSeries.IsGoodZero.unique: over a nontrivial ring the order of a good zero is unique.
• PowerSeries.isGoodZero_coe_iff, PowerSeries.isGoodZero_coe_iff_of_field: for polynomials the order is the root multiplicity, and over a ring the quotient by (X - a)ʰ must be a unit at a.
• PowerSeries.isGoodZero_iff_associated_taylor: a good zero of order h at a is a Taylor translate at a of the form Xʰ times a unit of R⟦X⟧.
• PowerSeries.isGoodZero_iff_order_taylor_eq: over a field, the order of a good zero at a is the order of the Taylor translate at a.
• PowerSeries.IsEntire.isGoodZero_iff: factorisation of an entire series at a good zero.
• PowerSeries.IsGoodZero.mul: the orders of good zeros of entire series add under products.
• PowerSeries.IsEntire.isGoodZero_mul_iff_of_isUnit: a factor which is a unit at a does not change good zeros at a.
• PowerSeries.IsGoodZero.isUnit and PowerSeries.IsGoodZero.exists_eq_one_sub_C_mul_X_pow_mul: for f(0) = 1, a good zero a of positive order h is a unit and f = (1 - a⁻¹ X)ʰ G with G entire, G(0) = 1 and G(a) a unit.
• PowerSeries.IsGoodZero.map: good zeros of entire series are preserved by continuous coefficient homomorphisms.
• PowerSeries.IsEntire.exists_isGoodZero, PowerSeries.IsEntire.exists_pos_isGoodZero_of_evalAt_eq_zero: over a complete normed field, a nonzero entire series has a good zero of some order at every point, of positive order at a zero.

References

• R. Coleman, p-adic Banach spaces and families of modular forms, Invent. Math. 127 (1997), 417–479, Appendix A4.
• C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, Algebra Number Theory 13 (2019), §2.2.

def PowerSeries.IsGoodZero {R : Type u_1} [CommRing R] [TopologicalSpace R] (f : PowerSeries R) (a : R) (h : ℕ) : Prop

A power series f has a good zero of order h at a if its Hasse derivatives of order less than h vanish at a and its Hasse derivative of order h is a unit at a. For h = 0 this says that f(a) is a unit. Values at a are the infinite sums PowerSeries.evalAt, so the notion is meaningful for entire series over a complete normed ring.

theorem PowerSeries.isGoodZero_iff {R : Type u_1} [CommRing R] [TopologicalSpace R] {f : PowerSeries R} {a : R} {h : ℕ} : f.IsGoodZero a h ↔ (∀ j < h, ((hasseDeriv j) f).evalAt a = 0) ∧ IsUnit (((hasseDeriv h) f).evalAt a)

Unfolding of PowerSeries.IsGoodZero.

@[simp]

theorem PowerSeries.isGoodZero_zero_iff {R : Type u_1} [CommRing R] [TopologicalSpace R] {f : PowerSeries R} {a : R} : f.IsGoodZero a 0 ↔ IsUnit (f.evalAt a)

A good zero of order 0 is a point at which the value is a unit.

theorem PowerSeries.IsGoodZero.evalAt_hasseDeriv_eq_zero {R : Type u_1} [CommRing R] [TopologicalSpace R] {f : PowerSeries R} {a : R} {h : ℕ} (hf : f.IsGoodZero a h) {j : ℕ} (hj : j < h) : ((hasseDeriv j) f).evalAt a = 0

At a good zero of order h, the Hasse derivatives of order less than h vanish.

theorem PowerSeries.IsGoodZero.isUnit_evalAt_hasseDeriv {R : Type u_1} [CommRing R] [TopologicalSpace R] {f : PowerSeries R} {a : R} {h : ℕ} (hf : f.IsGoodZero a h) : IsUnit (((hasseDeriv h) f).evalAt a)

At a good zero of order h, the Hasse derivative of order h is a unit.

theorem PowerSeries.IsGoodZero.evalAt_eq_zero {R : Type u_1} [CommRing R] [TopologicalSpace R] {f : PowerSeries R} {a : R} {h : ℕ} (hf : f.IsGoodZero a h) (hh : 0 < h) : f.evalAt a = 0

At a good zero of positive order, the series vanishes.

theorem PowerSeries.IsGoodZero.unique {R : Type u_1} [CommRing R] [TopologicalSpace R] {f : PowerSeries R} {a : R} {h k : ℕ} [Nontrivial R] (hh : f.IsGoodZero a h) (hk : f.IsGoodZero a k) : h = k

Over a nontrivial ring, the order of a good zero is unique.

@[simp]

theorem PowerSeries.isGoodZero_X_sub_C_pow {R : Type u_1} [CommRing R] [TopologicalSpace R] {a : R} {h : ℕ} : ((X - C a) ^ h).IsGoodZero a h

The series (X - a)ʰ has a good zero of order h at a.

theorem PowerSeries.isGoodZero_coe_iff {R : Type u_1} [CommRing R] [TopologicalSpace R] {a : R} {h : ℕ} [Nontrivial R] {p : Polynomial R} : (↑p).IsGoodZero a h ↔ Polynomial.rootMultiplicity a p = h ∧ IsUnit (Polynomial.eval a (p /ₘ (Polynomial.X - Polynomial.C a) ^ h))

Good zeros of polynomials. Over a nontrivial ring, a polynomial p has a good zero of order h at a exactly when h is the multiplicity of a as a root of p and the quotient of p by (X - a)ʰ is a unit at a.

theorem PowerSeries.isGoodZero_coe_iff_of_field {K : Type u_2} [Field K] [TopologicalSpace K] {p : Polynomial K} {a : K} {h : ℕ} : (↑p).IsGoodZero a h ↔ p ≠ 0 ∧ Polynomial.rootMultiplicity a p = h

Over a field, a polynomial has a good zero of order h at a exactly when it is nonzero and a is a root of multiplicity h.

theorem PowerSeries.isGoodZero_iff_associated_taylor {R : Type u_1} [CommRing R] [TopologicalSpace R] {f : PowerSeries R} {a : R} {h : ℕ} : f.IsGoodZero a h ↔ Associated (X ^ h) (taylor a f)

Over any coefficient ring, f has a good zero of order h at a exactly when its Taylor translate at a is Xʰ times a unit of R⟦X⟧.

theorem PowerSeries.isGoodZero_iff_order_taylor_eq {K : Type u_2} [Field K] [TopologicalSpace K] {f : PowerSeries K} {a : K} {h : ℕ} : f.IsGoodZero a h ↔ (taylor a f).order = ↑h

Over a field, f has a good zero of order h at a exactly when its Taylor translate at a has order h.

@[simp]

theorem PowerSeries.IsEntire.isGoodZero_X_sub_C_pow_mul_iff {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {g : PowerSeries R} {a : R} {h : ℕ} (hg : g.IsEntire) : ((X - C a) ^ h * g).IsGoodZero a h ↔ IsUnit (g.evalAt a)

For entire g, the series (X - a)ʰ g has a good zero of order h at a exactly when g(a) is a unit.

theorem PowerSeries.IsEntire.isGoodZero_iff {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f : PowerSeries R} {a : R} {h : ℕ} (hf : f.IsEntire) : f.IsGoodZero a h ↔ ∃ (g : PowerSeries R), g.IsEntire ∧ f = (X - C a) ^ h * g ∧ IsUnit (g.evalAt a)

Factorisation at a good zero. An entire series f has a good zero of order h at a exactly when f = (X - a)ʰ g for an entire series g with g(a) a unit.

theorem PowerSeries.IsGoodZero.mul {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f g : PowerSeries R} {a : R} {h k : ℕ} (hf : f.IsEntire) (hg : g.IsEntire) (hfa : f.IsGoodZero a h) (hga : g.IsGoodZero a k) : (f * g).IsGoodZero a (h + k)

Orders of good zeros add. If entire series f and g have good zeros of orders h and k at a, then f * g has a good zero of order h + k at a.

theorem PowerSeries.IsEntire.isGoodZero_mul_iff_of_isUnit {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f g : PowerSeries R} {a : R} {h : ℕ} (hf : f.IsEntire) (hg : g.IsEntire) (hga : IsUnit (g.evalAt a)) : (f * g).IsGoodZero a h ↔ f.IsGoodZero a h

Cancelling a unit factor. If g(a) is a unit, then f * g has a good zero of order h at a exactly when f does.

theorem PowerSeries.IsGoodZero.isUnit {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f : PowerSeries R} {a : R} {h : ℕ} (hf : f.IsEntire) (h0 : constantCoeff f = 1) (hfa : f.IsGoodZero a h) (hh : 0 < h) : IsUnit a

Good zeros of normalised series are units. If an entire series f with f(0) = 1 has a good zero of positive order at a, then a is a unit.

theorem PowerSeries.IsGoodZero.exists_eq_one_sub_C_mul_X_pow_mul {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f : PowerSeries R} {a : R} {h : ℕ} (hf : f.IsEntire) (h0 : constantCoeff f = 1) (hfa : f.IsGoodZero a h) : ∃ (G : PowerSeries R), G.IsEntire ∧ constantCoeff G = 1 ∧ IsUnit (G.evalAt a) ∧ f = (1 - C (Ring.inverse a) * X) ^ h * G

Normalised factorisation at a good zero. If an entire series f with f(0) = 1 has a good zero of order h at a, then f = (1 - a⁻¹ X)ʰ G with G entire, G(0) = 1 and G(a) a unit. For h > 0 the point a is a unit (PowerSeries.IsGoodZero.isUnit); for h = 0 the factor (1 - a⁻¹ X)ʰ is 1 and G = f.

theorem PowerSeries.IsGoodZero.map {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f : PowerSeries R} {a : R} {h : ℕ} {S : Type u_2} [CommRing S] [TopologicalSpace S] [T2Space S] (hf : f.IsEntire) (φ : R →+* S) (hφ : Continuous ⇑φ) (hfa : f.IsGoodZero a h) : ((PowerSeries.map φ) f).IsGoodZero (φ a) h

Good zeros under coefficient maps. A continuous ring homomorphism φ sends a good zero a of order h of an entire series f to a good zero φ a of order h of the mapped series.

theorem PowerSeries.IsEntire.exists_isGoodZero {K : Type u_1} [NormedField K] [CompleteSpace K] {f : PowerSeries K} (hf : f.IsEntire) (hf0 : f ≠ 0) (a : K) : ∃ (h : ℕ), f.IsGoodZero a h

Zeros of entire series over a field have finite order. Over a complete normed field, a nonzero entire series f has a good zero at every point a. Its order, unique by PowerSeries.IsGoodZero.unique, is the least h with (Δʰ f)(a) ≠ 0; it is positive exactly when f(a) = 0.

theorem PowerSeries.IsEntire.exists_pos_isGoodZero_of_evalAt_eq_zero {K : Type u_1} [NormedField K] [CompleteSpace K] {f : PowerSeries K} (hf : f.IsEntire) (hf0 : f ≠ 0) {a : K} (ha : f.evalAt a = 0) : ∃ (h : ℕ), 0 < h ∧ f.IsGoodZero a h

A zero of a nonzero entire series over a complete normed field is a good zero of some positive order.