Division of entire power series by polynomials with invertible leading coefficient

Let p be a monic polynomial of degree d over a complete normed commutative ring R, and let ∑ bₖ Xᵏ be the inverse of its reverse Xᵈ p(1/X), a power series with constant coefficient 1. For an entire series f = ∑ aₙ Xⁿ, the series

q = ∑ₙ (∑ₖ a_{n+d+k} bₖ) Xⁿ

converges coefficientwise, is again entire, and satisfies f = p * q + r for a polynomial r of degree less than d. The coefficients bₖ grow at most geometrically, which is what makes the inner sums converge however fast the radius of f is tested (PowerSeries.norm_coeff_invOfUnit_coe_le). When f is a polynomial, q and r are the quotient and remainder of ordinary polynomial division. Over an ultrametric ring with ‖1‖ = 1, a monic polynomial is distinguished of its degree at every large radius, so the Weierstrass division estimate makes q and r unique among divisions with entire quotient.

Normalising a polynomial with invertible leading coefficient reduces division to the monic case. The resulting entire quotient and polynomial remainder of smaller degree exist without an ultrametric hypothesis and are unique over an ultrametric ring with ‖1‖ = 1. The coefficient norm need not be multiplicative, and the coefficient ring may have nilpotents.

This is the division of entire series by polynomials used in the Fredholm theory of compact operators, whose Fredholm determinants are entire series.

Main definitions

• PowerSeries.divByMonic: the quotient q above, given by the explicit coefficient formula.
• PowerSeries.modByMonic: the remainder f - p * q, truncated to a polynomial of degree less than d.
• PowerSeries.IsEntire.mkAdjoinRoot: over an ultrametric ring with ‖1‖ = 1, reduction of entire series modulo p, as a surjective ring homomorphism to AdjoinRoot p whose kernel consists of the multiples of p by entire series.

Main results

• PowerSeries.hasSum_coeff_divByMonic: for entire f, the coefficients of q are the sums ∑ₖ a_{n+d+k} bₖ.
• PowerSeries.IsEntire.divByMonic: the quotient of an entire series is entire.
• PowerSeries.IsEntire.modByMonic_add_divByMonic: the division identity r + p * q = f.
• PowerSeries.IsEntire.add_divByMonic and PowerSeries.IsEntire.smul_divByMonic, with their modByMonic companions: on entire series, quotient and remainder are additive and R-linear.
• PowerSeries.IsEntire.tendsto_coeff_divByMonic_trunc and PowerSeries.IsEntire.tendsto_coeff_modByMonic_trunc: the quotients and remainders of the polynomial truncations converge coefficientwise.
• PowerSeries.IsEntire.map_divByMonic and PowerSeries.IsEntire.map_modByMonic: continuous coefficient homomorphisms commute with quotient and remainder.
• PowerSeries.divByMonic_coe and PowerSeries.modByMonic_coe: on polynomials, these are Polynomial.divByMonic and Polynomial.modByMonic.
• PowerSeries.IsEntire.evalAt_eq_eval_modByMonic: at a root of p, an entire series takes the value of its remainder.
• PowerSeries.IsEntire.evalAt_eq_zero_iff: the factor theorem; an entire series vanishes at a exactly when it is X - a times an entire series.
• PowerSeries.IsEntire.exists_eq_X_sub_C_pow_mul: if the Hasse derivatives of order less than h of an entire series vanish at a, then it is (X - a)ʰ times an entire series.
• PowerSeries.IsEntire.evalAt_hasseDeriv_mul_of_forall_lt: if the Hasse derivatives of order less than k of an entire series f vanish at a, then (Δᵏ (f g))(a) = (Δᵏ f)(a) g(a).
• PowerSeries.divByMonic_modByMonic_unique: over an ultrametric ring with ‖1‖ = 1, a division with entire quotient and remainder of degree less than d is this one.
• PowerSeries.IsEntire.coe_mul_divByMonic_cancel_left: over an ultrametric ring with ‖1‖ = 1, dividing p * q by p returns q for entire q.
• PowerSeries.IsEntire.modByMonic_coe_add_coe_mul: over an ultrametric ring with ‖1‖ = 1, the remainder of g + p * q, for a polynomial g and entire q, is g %ₘ p.
• PowerSeries.IsEntire.modByMonic_eq_zero_iff: over an ultrametric ring with ‖1‖ = 1, the remainder vanishes exactly when p divides f with entire quotient.
• TauCeti.PowerSeries.exists_entire_mul_add_eq: division by a polynomial with invertible leading coefficient, with entire quotient and polynomial remainder of smaller degree.
• TauCeti.PowerSeries.IsMulDistinguished.isEntire_of_isEntire_coe_mul: over an ultrametric ring, a series restricted at c whose product with a Weierstrass polynomial at c is entire is itself entire.
• TauCeti.PowerSeries.eq_and_eq_of_entire_mul_add_eq and TauCeti.PowerSeries.existsUnique_entire_mul_add_eq: uniqueness over an ultrametric ring with ‖1‖ = 1.

References

• R. F. Coleman, p-adic Banach spaces and families of modular forms, Invent. Math. 127 (1997), Appendix A3.

noncomputable def PowerSeries.divByMonic {R : Type u_1} [CommRing R] [TopologicalSpace R] (f : PowerSeries R) (p : Polynomial R) : PowerSeries R

The quotient of a power series f on division by a monic polynomial p of degree d: its coefficient in degree n is ∑ₖ a_{n+d+k} bₖ, where aₘ are the coefficients of f and bₖ those of the inverse of the reverse of p. For entire f these sums converge (PowerSeries.hasSum_coeff_divByMonic) and give the quotient of a division with polynomial remainder (PowerSeries.IsEntire.modByMonic_add_divByMonic). Otherwise the value is not meaningful.

noncomputable def PowerSeries.modByMonic {R : Type u_1} [CommRing R] [TopologicalSpace R] (f : PowerSeries R) (p : Polynomial R) : Polynomial R

The remainder of a power series f on division by a monic polynomial p: the polynomial of degree less than natDegree p given by the coefficients of f - p * f.divByMonic p in those degrees. For entire f, f - p * f.divByMonic p is this polynomial (PowerSeries.IsEntire.modByMonic_add_divByMonic).

theorem PowerSeries.coeff_divByMonic {R : Type u_1} [CommRing R] [TopologicalSpace R] (f : PowerSeries R) (p : Polynomial R) (n : ℕ) : (coeff n) (f.divByMonic p) = ∑' (k : ℕ), (coeff (n + p.natDegree + k)) f * (coeff k) ((↑p.reverse).invOfUnit 1)

The coefficients of f.divByMonic p, as the defining sums.

theorem PowerSeries.coeff_modByMonic {R : Type u_1} [CommRing R] [TopologicalSpace R] (f : PowerSeries R) (p : Polynomial R) (n : ℕ) : (f.modByMonic p).coeff n = if n < p.natDegree then (coeff n) (f - ↑p * f.divByMonic p) else 0

The coefficients of f.modByMonic p are those of f - p * f.divByMonic p in degrees less than natDegree p.

theorem PowerSeries.degree_modByMonic_lt {R : Type u_1} [CommRing R] [TopologicalSpace R] {p : Polynomial R} (f : PowerSeries R) (hp : p ≠ 0) : (f.modByMonic p).degree < p.degree

The remainder has degree less than the divisor.

@[simp]

theorem PowerSeries.divByMonic_one {R : Type u_1} [CommRing R] [TopologicalSpace R] (f : PowerSeries R) : f.divByMonic 1 = f

Division by the polynomial 1 returns the series itself.

@[simp]

theorem PowerSeries.modByMonic_one {R : Type u_1} [CommRing R] [TopologicalSpace R] (f : PowerSeries R) : f.modByMonic 1 = 0

Division by the polynomial 1 leaves no remainder.

@[simp]

theorem PowerSeries.zero_divByMonic {R : Type u_1} [CommRing R] [TopologicalSpace R] (p : Polynomial R) : divByMonic 0 p = 0

The quotient of 0 is 0.

@[simp]

theorem PowerSeries.zero_modByMonic {R : Type u_1} [CommRing R] [TopologicalSpace R] (p : Polynomial R) : modByMonic 0 p = 0

The remainder of 0 is 0.

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

The quotient of an entire series on division by a polynomial is entire.

theorem PowerSeries.hasSum_coeff_divByMonic {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (p : Polynomial R) (n : ℕ) : HasSum (fun (k : ℕ) => (coeff (n + p.natDegree + k)) f * (coeff k) ((↑p.reverse).invOfUnit 1)) ((coeff n) (f.divByMonic p))

The coefficient formula for entire division. For an entire series f, the sums defining the coefficients of f.divByMonic p converge.

theorem PowerSeries.IsEntire.modByMonic_add_divByMonic {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} {p : Polynomial R} [CompleteSpace R] (hf : f.IsEntire) (hp : p.Monic) : ↑(f.modByMonic p) + ↑p * f.divByMonic p = f

Division of an entire series by a monic polynomial. An entire series f is r + p * q, with q = f.divByMonic p entire and r = f.modByMonic p of degree less than p.

theorem PowerSeries.IsEntire.add_divByMonic {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] {g : PowerSeries R} (hf : f.IsEntire) (hg : g.IsEntire) (p : Polynomial R) : (f + g).divByMonic p = f.divByMonic p + g.divByMonic p

On entire series, the quotient is additive.

theorem PowerSeries.IsEntire.add_modByMonic {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] {g : PowerSeries R} (hf : f.IsEntire) (hg : g.IsEntire) (p : Polynomial R) : (f + g).modByMonic p = f.modByMonic p + g.modByMonic p

On entire series, the remainder is additive.

theorem PowerSeries.IsEntire.smul_divByMonic {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (a : R) (p : Polynomial R) : (a • f).divByMonic p = a • f.divByMonic p

On entire series, the quotient commutes with scalar multiplication.

theorem PowerSeries.IsEntire.smul_modByMonic {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (a : R) (p : Polynomial R) : (a • f).modByMonic p = a • f.modByMonic p

On entire series, the remainder commutes with scalar multiplication.

theorem PowerSeries.IsEntire.tendsto_coeff_divByMonic_trunc {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (p : Polynomial R) (n : ℕ) : Filter.Tendsto (fun (N : ℕ) => (coeff n) ((↑((trunc N) f)).divByMonic p)) Filter.atTop (nhds ((coeff n) (f.divByMonic p)))

The quotients of the polynomial truncations of an entire series converge coefficientwise to its quotient: each coefficient of the quotient of trunc N f is a partial sum of the series defining that of f.

theorem PowerSeries.IsEntire.tendsto_coeff_modByMonic_trunc {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (p : Polynomial R) (n : ℕ) : Filter.Tendsto (fun (N : ℕ) => ((↑((trunc N) f)).modByMonic p).coeff n) Filter.atTop (nhds ((f.modByMonic p).coeff n))

The remainders of the polynomial truncations of an entire series converge coefficientwise to its remainder.

theorem PowerSeries.IsEntire.map_divByMonic {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} {p : Polynomial R} [CompleteSpace R] {S : Type u_2} [CommRing S] [TopologicalSpace S] [T2Space S] (hf : f.IsEntire) (hp : p.Monic) (φ : R →+* S) (hφ : Continuous ⇑φ) : ((PowerSeries.map φ) f).divByMonic (Polynomial.map φ p) = (PowerSeries.map φ) (f.divByMonic p)

A continuous coefficient homomorphism commutes with the quotient of entire division by a monic polynomial.

theorem PowerSeries.IsEntire.map_modByMonic {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} {p : Polynomial R} [CompleteSpace R] {S : Type u_2} [CommRing S] [TopologicalSpace S] [T2Space S] (hf : f.IsEntire) (hp : p.Monic) (φ : R →+* S) (hφ : Continuous ⇑φ) : ((PowerSeries.map φ) f).modByMonic (Polynomial.map φ p) = Polynomial.map φ (f.modByMonic p)

A continuous coefficient homomorphism commutes with the remainder of entire division by a monic polynomial.

@[simp]

theorem PowerSeries.divByMonic_coe {R : Type u_1} [NormedCommRing R] {p : Polynomial R} [CompleteSpace R] (g : Polynomial R) (hp : p.Monic) : (↑g).divByMonic p = ↑(g /ₘ p)

On a polynomial, the quotient of entire division is the quotient of polynomial division.

@[simp]

theorem PowerSeries.modByMonic_coe {R : Type u_1} [NormedCommRing R] {p : Polynomial R} [CompleteSpace R] (g : Polynomial R) (hp : p.Monic) : (↑g).modByMonic p = g %ₘ p

On a polynomial, the remainder of entire division is the remainder of polynomial division.

theorem PowerSeries.divByMonic_coe_of_degree_lt {R : Type u_1} [NormedCommRing R] {p : Polynomial R} [CompleteSpace R] {g : Polynomial R} (hp : p.Monic) (hg : g.degree < p.degree) : (↑g).divByMonic p = 0

A polynomial of degree less than p has quotient 0 on division by p.

theorem PowerSeries.modByMonic_coe_of_degree_lt {R : Type u_1} [NormedCommRing R] {p : Polynomial R} [CompleteSpace R] {g : Polynomial R} (hp : p.Monic) (hg : g.degree < p.degree) : (↑g).modByMonic p = g

A polynomial of degree less than p is its own remainder on division by p.

theorem PowerSeries.IsEntire.evalAt_eq_eval_modByMonic {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} {p : Polynomial R} [CompleteSpace R] (hf : f.IsEntire) (hp : p.Monic) {a : R} (ha : Polynomial.eval a p = 0) : f.evalAt a = Polynomial.eval a (f.modByMonic p)

At a root a of the monic polynomial p, an entire series takes the value of its remainder on division by p.

theorem PowerSeries.IsEntire.evalAt_eq_zero_iff {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) {a : R} : f.evalAt a = 0 ↔ ∃ (q : PowerSeries R), q.IsEntire ∧ f = (X - C a) * q

Factor theorem for entire series. An entire series vanishes at a exactly when it is X - a times an entire series.

theorem PowerSeries.IsEntire.exists_eq_X_sub_C_pow_mul {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) {a : R} {h : ℕ} (hzero : ∀ j < h, ((PowerSeries.hasseDeriv j) f).evalAt a = 0) : ∃ (g : PowerSeries R), g.IsEntire ∧ f = (X - C a) ^ h * g

If the Hasse derivatives of order less than h of an entire series f vanish at a, then f = (X - a)ʰ g for an entire series g.

theorem PowerSeries.IsEntire.evalAt_hasseDeriv_mul_of_forall_lt {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] {g : PowerSeries R} (hf : f.IsEntire) (hg : g.IsEntire) {a : R} {k : ℕ} (hk : ∀ j < k, ((PowerSeries.hasseDeriv j) f).evalAt a = 0) : ((PowerSeries.hasseDeriv k) (f * g)).evalAt a = ((PowerSeries.hasseDeriv k) f).evalAt a * g.evalAt a

If the Hasse derivatives of order less than k of an entire series f vanish at a, then the Hasse derivative of order k of f * g at a is that of f times g(a).

theorem PowerSeries.divByMonic_modByMonic_unique {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} {p : Polynomial R} [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] (q : PowerSeries R) (r : Polynomial R) (hp : p.Monic) (hq : q.IsEntire) (h : ↑r + ↑p * q = f ∧ r.degree < p.degree) : f.divByMonic p = q ∧ f.modByMonic p = r

Uniqueness of entire division. Over an ultrametric ring with ‖1‖ = 1, if f = r + p * q with q entire and r of degree less than the monic polynomial p, then q and r are the quotient and remainder of f on division by p.

theorem PowerSeries.IsEntire.coe_mul_divByMonic_cancel_left {R : Type u_1} [NormedCommRing R] {p : Polynomial R} [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] {q : PowerSeries R} (hq : q.IsEntire) (hp : p.Monic) : (↑p * q).divByMonic p = q

Over an ultrametric ring with ‖1‖ = 1, dividing p * q by the monic polynomial p, for entire q, returns q.

theorem PowerSeries.IsEntire.coe_mul_modByMonic {R : Type u_1} [NormedCommRing R] {p : Polynomial R} [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] {q : PowerSeries R} (hq : q.IsEntire) (hp : p.Monic) : (↑p * q).modByMonic p = 0

Over an ultrametric ring with ‖1‖ = 1, p * q leaves no remainder on division by the monic polynomial p, for entire q.

theorem PowerSeries.IsEntire.modByMonic_coe_add_coe_mul {R : Type u_1} [NormedCommRing R] {p : Polynomial R} [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] {q : PowerSeries R} (hq : q.IsEntire) (hp : p.Monic) (g : Polynomial R) : (↑g + ↑p * q).modByMonic p = g %ₘ p

Over an ultrametric ring with ‖1‖ = 1, adding p * q to a polynomial g, for entire q, does not change its remainder on division by the monic polynomial p.

theorem PowerSeries.IsEntire.modByMonic_eq_zero_iff {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} {p : Polynomial R} [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] (hf : f.IsEntire) (hp : p.Monic) : f.modByMonic p = 0 ↔ ∃ (q : PowerSeries R), q.IsEntire ∧ f = ↑p * q

Over an ultrametric ring with ‖1‖ = 1, an entire series leaves no remainder on division by a monic polynomial p exactly when it is p times an entire series.

noncomputable def PowerSeries.IsEntire.mkAdjoinRoot {R : Type u_1} [NormedCommRing R] {p : Polynomial R} [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] (hp : p.Monic) : ↥(IsEntire.subring R) →+* AdjoinRoot p

Reduction of entire series modulo a monic polynomial. Over a complete ultrametric ring with ‖1‖ = 1, sending an entire series F to the class of its remainder F.modByMonic p in AdjoinRoot p is a ring homomorphism. It is surjective, with kernel the multiples of p by entire series.

@[simp]

theorem PowerSeries.IsEntire.mkAdjoinRoot_apply {R : Type u_1} [NormedCommRing R] {p : Polynomial R} [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] (hp : p.Monic) (F : ↥(IsEntire.subring R)) : (mkAdjoinRoot hp) F = (AdjoinRoot.mk p) ((↑F).modByMonic p)

Reduction modulo p sends an entire series to the class of its remainder.

theorem PowerSeries.IsEntire.mkAdjoinRoot_coe {R : Type u_1} [NormedCommRing R] {p : Polynomial R} [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] (hp : p.Monic) (g : Polynomial R) : (mkAdjoinRoot hp) ⟨↑g, ⋯⟩ = (AdjoinRoot.mk p) g

On polynomials, reduction modulo p is AdjoinRoot.mk p.

theorem PowerSeries.IsEntire.mkAdjoinRoot_surjective {R : Type u_1} [NormedCommRing R] {p : Polynomial R} [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] (hp : p.Monic) : Function.Surjective ⇑(mkAdjoinRoot hp)

Reduction of entire series modulo p is surjective: polynomials already reach every class.

theorem PowerSeries.IsEntire.mkAdjoinRoot_eq_zero_iff {R : Type u_1} [NormedCommRing R] {p : Polynomial R} [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] (hp : p.Monic) {F : ↥(IsEntire.subring R)} : (mkAdjoinRoot hp) F = 0 ↔ ∃ (q : PowerSeries R), q.IsEntire ∧ ↑F = ↑p * q

An entire series reduces to zero modulo p exactly when it is p times an entire series.

theorem TauCeti.PowerSeries.exists_entire_mul_add_eq {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f : PowerSeries R} {p : Polynomial R} (hf : f.IsEntire) (hp : IsUnit p.leadingCoeff) [Nontrivial R] : ∃ (q : PowerSeries R) (b : Polynomial R), q.IsEntire ∧ b.degree < p.degree ∧ ↑p * q + ↑b = f

An entire series admits division by a polynomial with invertible leading coefficient, with entire quotient and polynomial remainder of degree less than the divisor. No ultrametric hypothesis is needed for existence.

theorem TauCeti.PowerSeries.IsMulDistinguished.isEntire_of_isEntire_coe_mul {R : Type u_1} [NormedCommRing R] [CompleteSpace R] [IsUltrametricDist R] {c : ℝ} {d : ℕ} {ω : Polynomial R} {q : PowerSeries R} (hω : IsMulDistinguished c d ↑ω) (hc : 0 < c) (hωm : ω.IsMonicOfDegree d) (hq : PowerSeries.IsRestricted c q) (h : (↑ω * q).IsEntire) : q.IsEntire

Restricted quotients of entire series by Weierstrass polynomials are entire. Over a complete ultrametric normed commutative ring, let ω be a monic polynomial of degree d which is multiplicatively distinguished of degree d at a positive radius c. If q is restricted at c and ω * q is entire, then q is entire: it is the quotient of the entire division of ω * q by ω. The hypothesis on ω cannot be dropped: (X - 1) * ∑ Xⁿ = -1 is entire.

theorem TauCeti.PowerSeries.eq_and_eq_of_entire_mul_add_eq {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f : PowerSeries R} {p : Polynomial R} [IsUltrametricDist R] [NormOneClass R] (hp : IsUnit p.leadingCoeff) {q q' : PowerSeries R} {b b' : Polynomial R} (hq : q.IsEntire) (hq' : q'.IsEntire) (hb : b.degree < p.degree) (hb' : b'.degree < p.degree) (h : ↑p * q + ↑b = f) (h' : ↑p * q' + ↑b' = f) : q = q' ∧ b = b'

Entire quotients and polynomial remainders of degree less than a polynomial with invertible leading coefficient are unique, over a complete ultrametric norm-one ring.

theorem TauCeti.PowerSeries.existsUnique_entire_mul_add_eq {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f : PowerSeries R} {p : Polynomial R} [IsUltrametricDist R] [NormOneClass R] (hf : f.IsEntire) (hp : IsUnit p.leadingCoeff) : ∃! qb : PowerSeries R × Polynomial R, qb.1.IsEntire ∧ qb.2.degree < p.degree ∧ ↑p * qb.1 + ↑qb.2 = f

Entire division by a polynomial with invertible leading coefficient. Over a complete ultrametric norm-one ring, every entire series has exactly one decomposition as the divisor times an entire quotient plus a polynomial remainder of smaller degree. This includes constant unit divisors, whose remainders are zero.