Newton polygons of products

The Newton polygon of a product of polynomials is the Minkowski sum of the Newton polygons of the factors, given by the min-convolution TauCeti.minkowskiSum. When both Newton polygons are nonempty, for example when both factors are nonzero over a field, the finite slopes of the product are those of the two factors together. These are the identities from which the slopes of a split polynomial are read off its linear factors.

One inequality is the ultrametric inequality for the coefficients of a product, and holds for power series with admissible coefficient heights. For the other, fix a slope σ and take the first index at which the coefficient heights of each factor touch their supporting line of slope σ. At the sum of these two indices the coefficient of the product has a unique dominant term, so its valuation is the sum of the two valuations. Hence the supporting values of the product are the sums of the supporting values of the factors, and a convex sequence is determined by its supporting values.

The same dominant-term argument works for power series at any slope where supporting lines touch the coefficient heights of both factors, with no convergence hypothesis. There the supporting values of the product are again the sums of those of the factors. When v comes from an absolute value, this is the multiplicativity of Gauss norms at the corresponding radius. If such contacts exist at every slope, the Newton polygon of the product is the Minkowski sum of the Newton polygons of the factors; the polynomial identity is the case of finitely many finite heights.

At a common slope where both power-series polygons have finite faces, the product has the finite face whose absolute endpoints are the sums of those of the factors. This local law requires no convergence hypothesis and does not assert a global product identity outside the face. Singleton faces are allowed and contribute width zero; endpoints include any initial order of vanishing.

Main results

• PowerSeries.addValuation_coeff_mul_eq_add_of_isLeast and PowerSeries.addValuation_coeff_mul_eq_add_of_isGreatest: at the sum of the first, respectively last, contact indices of supporting lines of a common slope, the valuation of the coefficient of a product is the sum of the valuations of the two coefficients; PowerSeries.addValuation_coeff_mul_eq_add_of_lt is the general unique-dominant-term form.
• PowerSeries.minkowskiSum_le_addValuation_coeff_mul: the coefficient heights of a product lie above the Minkowski sum of the coefficient heights of the factors.
• PowerSeries.supportingValue_addValuation_coeff_mul: supporting values of coefficient heights add under multiplication, at any slope where both factors touch a supporting line.
• PowerSeries.minkowskiSum_newtonPolygon_le_newtonPolygon_mul: for admissible coefficient heights, the Minkowski sum of the Newton polygons of two power series lies below the Newton polygon of their product.
• PowerSeries.supportingValue_newtonPolygon_mul: the same additivity for the supporting values of the Newton polygons.
• PowerSeries.newtonPolygon_mul_of_forall_exists_mem_supportingFace: if the coefficient heights of both factors touch supporting lines of every slope, the Newton polygon of the product is the Minkowski sum of the Newton polygons of the factors.
• PowerSeries.isFiniteFace_newtonPolygon_mul: finite faces at a common slope add under multiplication, with both absolute endpoints adding.
• Polynomial.newtonPolygon_mul: the Newton polygon of a product of polynomials is the Minkowski sum of the Newton polygons of the factors. No hypothesis is needed: if either factor has the empty polygon, so does the product.
• Polynomial.supportingValue_addValuation_coeff_mul: supporting values of coefficient heights add under multiplication of polynomials, at every slope.
• Polynomial.newtonSlopes_mul, Polynomial.newtonSlopes_prod and Polynomial.newtonSlopes_finprod: when the factors have nonempty Newton polygons, the finite slope multiset of a product of polynomials is the sum of the finite slope multisets of the factors.
• Polynomial.newtonSlopes_le_of_dvd: the finite slopes of a factor of a polynomial with a nonempty Newton polygon are among those of the polynomial, with multiplicity.

References

• M. Lazard, Les zéros d'une fonction analytique d'une variable sur un corps valué complet, Publications Mathématiques de l'IHÉS 14 (1962), §1, Proposition 1.
• K. S. Kedlaya, Newton polygons, MIT 18.787, fall 2007, §§1–2. Kedlaya plots coefficient points at negative indices; our convention uses positive indices, so the slopes have the opposite sign.
• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, second edition, Graduate Texts in Mathematics 58, Springer, 1984, Chapter IV §§3–4.

theorem PowerSeries.addValuation_coeff_mul_eq_add_of_lt {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) {f g : PowerSeries R} {σ c d : ℝ} {i j : ℕ} (hf : TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) f)) σ c) (hi : i ∈ TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) f)) σ c) (hg : TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) g)) σ d) (hj : j ∈ TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) g)) σ d) (hsplit : ∀ (p q : ℕ), p + q = i + j → p ≠ i → ↑(c + σ * ↑p) < v ((coeff p) f) ∨ ↑(d + σ * ↑q) < v ((coeff q) g)) : v ((coeff (i + j)) (f * g)) = v ((coeff i) f) + v ((coeff j) g)

The unique dominant term of a coefficient of a product. Suppose the coefficient heights of f and g touch supporting lines of a common slope σ at i and j, and every other split p + q = i + j has p or q strictly above its line. Then the valuation of the coefficient of f * g at i + j is the sum of the valuations of the coefficients of f at i and of g at j.

theorem PowerSeries.addValuation_coeff_mul_eq_add_of_isLeast {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) {f g : PowerSeries R} {σ c d : ℝ} {i j : ℕ} (hf : TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) f)) σ c) (hi : IsLeast (TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) f)) σ c) i) (hg : TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) g)) σ d) (hj : IsLeast (TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) g)) σ d) j) : v ((coeff (i + j)) (f * g)) = v ((coeff i) f) + v ((coeff j) g)

The valuation of the coefficient of a product at the sum of the first contact indices. If i and j are the least indices at which the coefficient heights of f and g touch supporting lines of a common slope, then the valuation of the coefficient of f * g at i + j is the sum of the valuations of the coefficients of f at i and of g at j.

theorem PowerSeries.addValuation_coeff_mul_eq_add_of_isGreatest {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) {f g : PowerSeries R} {σ c d : ℝ} {i j : ℕ} (hf : TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) f)) σ c) (hi : IsGreatest (TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) f)) σ c) i) (hg : TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) g)) σ d) (hj : IsGreatest (TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) g)) σ d) j) : v ((coeff (i + j)) (f * g)) = v ((coeff i) f) + v ((coeff j) g)

The valuation of the coefficient of a product at the sum of the last contact indices. If i and j are the greatest indices at which the coefficient heights of f and g touch supporting lines of a common slope, then the valuation of the coefficient of f * g at i + j is the sum of the valuations of the coefficients of f at i and of g at j.

theorem PowerSeries.minkowskiSum_le_addValuation_coeff_mul {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) {f g : PowerSeries R} (n : ℕ) : TauCeti.minkowskiSum (fun (n : ℕ) => v ((coeff n) f)) (fun (n : ℕ) => v ((coeff n) g)) n ≤ v ((coeff n) (f * g))

The coefficient heights of a product of power series lie above the Minkowski sum of the coefficient heights of the factors.

theorem PowerSeries.supportingValue_addValuation_coeff_mul {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) {f g : PowerSeries R} {σ c d : ℝ} {i j : ℕ} (hf : TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) f)) σ c) (hi : i ∈ TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) f)) σ c) (hg : TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) g)) σ d) (hj : j ∈ TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) g)) σ d) : TauCeti.supportingValue (fun (n : ℕ) => v ((coeff n) (f * g))) σ = TauCeti.supportingValue (fun (n : ℕ) => v ((coeff n) f)) σ + TauCeti.supportingValue (fun (n : ℕ) => v ((coeff n) g)) σ

If supporting lines of a common slope touch the coefficient heights of f and g, then the supporting value of the coefficient heights of f * g at that slope is the sum of those of f and g. When v comes from an absolute value, this is the multiplicativity of Gauss norms at the corresponding radius.

theorem PowerSeries.minkowskiSum_newtonPolygon_le_newtonPolygon_mul {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) {f g : PowerSeries R} (hf : TauCeti.IsAdmissible fun (n : ℕ) => v ((coeff n) f)) (hg : TauCeti.IsAdmissible fun (n : ℕ) => v ((coeff n) g)) : TauCeti.minkowskiSum (f.newtonPolygon v) (g.newtonPolygon v) ≤ (f * g).newtonPolygon v

For admissible coefficient heights, the Minkowski sum of the Newton polygons of two power series lies below the Newton polygon of their product.

theorem PowerSeries.supportingValue_newtonPolygon_mul {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) {f g : PowerSeries R} {σ c d : ℝ} {i j : ℕ} (hf : TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) f)) σ c) (hi : i ∈ TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) f)) σ c) (hg : TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) g)) σ d) (hj : j ∈ TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) g)) σ d) : TauCeti.supportingValue ((f * g).newtonPolygon v) σ = TauCeti.supportingValue (f.newtonPolygon v) σ + TauCeti.supportingValue (g.newtonPolygon v) σ

If supporting lines of a common slope σ touch the coefficient heights of f and g, then the supporting value at σ of the Newton polygon of f * g is the sum of those of the Newton polygons of f and g. No convergence hypothesis is needed beyond these two contacts.

theorem PowerSeries.newtonPolygon_mul_of_forall_exists_mem_supportingFace {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) {f g : PowerSeries R} (hf : ∀ (σ : ℝ), ∃ (c : ℝ) (i : ℕ), TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) f)) σ c ∧ i ∈ TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) f)) σ c) (hg : ∀ (σ : ℝ), ∃ (d : ℝ) (j : ℕ), TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) g)) σ d ∧ j ∈ TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) g)) σ d) : (f * g).newtonPolygon v = TauCeti.minkowskiSum (f.newtonPolygon v) (g.newtonPolygon v)

The Newton polygon of a product is the Minkowski sum of the Newton polygons of the factors, provided that at every slope the coefficient heights of each factor touch a supporting line. This holds for polynomials with nonempty Newton polygons, and for nonzero entire series when the valuation comes from the norm. Without contact the identity can fail: 1 - X and the geometric series ∑ Xⁿ have product 1, a single point, while the Minkowski sum of their polygons is a horizontal half-line.

theorem PowerSeries.isFiniteFace_newtonPolygon_mul {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) {f g : PowerSeries R} {σ : ℝ} {l u l' u' : ℕ} (hf : TauCeti.IsFiniteFace (f.newtonPolygon v) σ l u) (hg : TauCeti.IsFiniteFace (g.newtonPolygon v) σ l' u') : TauCeti.IsFiniteFace ((f * g).newtonPolygon v) σ (l + l') (u + u')

Finite Newton faces at a common slope add under multiplication, with both absolute endpoints adding. This is a local product law: the polygons need not agree with their Minkowski sum away from this face. No convergence hypothesis is required.

theorem Polynomial.newtonPolygon_mul {R : Type u_1} [Ring R] (f g : Polynomial R) (v : AddValuation R (WithTop ℝ)) : (f * g).newtonPolygon v = TauCeti.minkowskiSum (f.newtonPolygon v) (g.newtonPolygon v)

The Newton polygon of a product of polynomials is the Minkowski sum of the Newton polygons of the factors. If either factor has the empty Newton polygon, for example if it is zero, so does the product.

theorem Polynomial.supportingValue_addValuation_coeff_mul {R : Type u_1} [Ring R] (f g : Polynomial R) (v : AddValuation R (WithTop ℝ)) (σ : ℝ) : TauCeti.supportingValue (fun (n : ℕ) => v ((f * g).coeff n)) σ = TauCeti.supportingValue (fun (n : ℕ) => v (f.coeff n)) σ + TauCeti.supportingValue (fun (n : ℕ) => v (g.coeff n)) σ

Supporting values of coefficient heights add under multiplication of polynomials. When v comes from an absolute value, this is the multiplicativity of Gauss norms at every radius. No hypothesis is needed: if all coefficient heights of a factor are infinite, both sides are ⊤.

theorem Polynomial.newtonSlopes_mul {R : Type u_1} [Ring R] (f g : Polynomial R) (v : AddValuation R (WithTop ℝ)) (hf : f.newtonPolygon v ≠ ⊤) (hg : g.newtonPolygon v ≠ ⊤) : (f * g).newtonSlopes v = f.newtonSlopes v + g.newtonSlopes v

If both factors have nonempty Newton polygons, the finite slope multiset of a product of polynomials is the sum of the finite slope multisets of the factors. The hypotheses exclude zero factors: the product 0 * g has no finite slopes, whatever those of g. If only zero has infinite valuation, a nonzero polynomial has a nonempty Newton polygon by Polynomial.newtonPolygon_ne_top_of_ne_zero.

theorem Polynomial.newtonSlopes_le_of_dvd {R : Type u_1} [Ring R] {f g : Polynomial R} {v : AddValuation R (WithTop ℝ)} (hf : f.newtonPolygon v ≠ ⊤) (hgf : g ∣ f) : g.newtonSlopes v ≤ f.newtonSlopes v

If f has a nonempty Newton polygon, the finite slopes of a factor g of f are among the finite slopes of f, counted with multiplicity. This holds for every nonzero f when only zero has infinite valuation, by Polynomial.newtonPolygon_ne_top_of_ne_zero.

theorem Polynomial.newtonPolygon_ne_top_prod {ι : Type u_1} {R : Type u_2} [CommRing R] (v : AddValuation R (WithTop ℝ)) (s : Finset ι) (g : ι → Polynomial R) (hg : ∀ i ∈ s, (g i).newtonPolygon v ≠ ⊤) : (∏ i ∈ s, g i).newtonPolygon v ≠ ⊤

A finite product of polynomials with nonempty Newton polygons has a nonempty Newton polygon.

theorem Polynomial.newtonSlopes_prod {ι : Type u_1} {R : Type u_2} [CommRing R] (v : AddValuation R (WithTop ℝ)) (s : Finset ι) (g : ι → Polynomial R) (hg : ∀ i ∈ s, (g i).newtonPolygon v ≠ ⊤) : (∏ i ∈ s, g i).newtonSlopes v = ∑ i ∈ s, (g i).newtonSlopes v

The finite slope multiset of a finite product of polynomials with nonempty Newton polygons is the sum of the finite slope multisets of the factors.

theorem Polynomial.newtonSlopes_finprod {ι : Type u_1} {R : Type u_2} [CommRing R] (v : AddValuation R (WithTop ℝ)) (g : ι → Polynomial R) (hfin : (Function.mulSupport g).Finite) (hg : ∀ i ∈ Function.mulSupport g, (g i).newtonPolygon v ≠ ⊤) : (∏ᶠ (i : ι), g i).newtonSlopes v = ∑ i ∈ hfin.toFinset, (g i).newtonSlopes v

The finite slope multiset of a finitely supported product ∏ᶠ i, g i, whose nontrivial factors have nonempty Newton polygons, is the sum of their finite slope multisets.