Newton polygons of polynomials and power series

Given an additive valuation v with real values, a polynomial or power series f has the coefficient heights n ↦ v (coeff n f), plotted at the points (n, v (coeff n f)), with height ⊤ at the vanishing coefficients. Its Newton polygon is the lower convex envelope of these heights. With this orientation slopes increase from left to right, and a slope m corresponds to a nonzero root of valuation -m.

The valuation is real valued. A valuation with values in another ordered group WithTop Γ is normalised first by an order-preserving additive embedding Γ → ℝ, for example through AddValuation.map.

A polynomial has only finitely many nonzero coefficients, so its heights are always admissible and its Newton polygon is their lower convex envelope. A power series need not have admissible heights; its newtonPolygon is then the all-infinite fallback of TauCeti.lowerConvexEnvelope, and geometric statements assume admissibility.

Main definitions

• PowerSeries.newtonPolygon f v: the lower convex envelope of the heights n ↦ v (coeff n f).
• Polynomial.newtonPolygon f v: the same construction for a polynomial; it agrees with the Newton polygon of the power series (f : R⟦X⟧) by Polynomial.newtonPolygon_coe. Both take the valuation as an explicit argument rather than through a global instance.

Main results

• Polynomial.isLowerConvexEnvelope_newtonPolygon: the Newton polygon of a polynomial is the greatest convex minorant of its coefficient heights.
• PowerSeries.supportingValue_newtonPolygon and Polynomial.supportingValue_newtonPolygon: the Newton polygon has the same supporting values as the coefficient heights.
• Polynomial.newtonPolygon_eq_top_iff: the Newton polygon of a polynomial is empty exactly when every coefficient has infinite valuation.
• Polynomial.newtonPolygon_ne_top_iff: if only zero has infinite valuation (for example over a division ring), a nonzero polynomial has a polygon whose finite domain is the interval from its order of vanishing at zero to its degree; in particular the polygon is nonempty by Polynomial.newtonPolygon_ne_top_of_ne_zero. More generally, by Polynomial.newtonPolygon_ne_top_iff_of_ne_top and Polynomial.finiteEdges_newtonPolygon_of_ne_top, the same holds for any valuation as soon as the trailing and leading coefficients have finite valuation.
• Polynomial.Monic.newtonPolygon_ne_top: a monic polynomial has a nonempty Newton polygon, whatever the valuation.
• Polynomial.newtonPolygon_natTrailingDegree and Polynomial.newtonPolygon_natDegree: the polygon begins at the trailing coefficient and ends at the leading coefficient; Polynomial.newtonPolygon_apply_zero and Polynomial.newtonPolygon_eq_of_natDegree_le read its heights at index zero and at any index from the degree on.
• Polynomial.ncard_finiteEdges_newtonPolygon: if only zero has infinite valuation, a polynomial of degree d and order a of vanishing at zero has d - a finite unit edges, and by Polynomial.finiteEdges_newtonPolygon_monomial a monomial has none.
• PowerSeries.newtonPolygon_neg and Polynomial.newtonPolygon_neg: negation preserves the Newton polygon.
• PowerSeries.newtonPolygon_smul, PowerSeries.newtonPolygon_X_pow_mul, PowerSeries.newtonPolygon_rescale and PowerSeries.newtonPolygon_map: multiplication by a scalar translates the heights, multiplication by X ^ k shifts the polygon k places, the substitution X ↦ c X shears it by the valuation of c, and an extension of coefficients compatible with the valuations preserves it. The corresponding polynomial statements are proved as well, with Polynomial.newtonPolygon_comp_C_mul_X for the substitution X ↦ c X.
• PowerSeries.newtonPolygon_map_eq_map_mul and Polynomial.newtonPolygon_map_eq_map_mul: an extension of coefficients multiplying the valuations by a positive real factor multiplies the Newton polygon by that factor.
• Polynomial.newtonPolygon_reflect and Polynomial.newtonPolygon_reverse: reversing a polynomial of degree d, or more generally reflecting its coefficients in any N ≥ d, reflects the Newton polygon by n ↦ N - n.

References

• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, second edition, Graduate Texts in Mathematics 58, Springer, 1984, Chapter IV §§3–4.

noncomputable def PowerSeries.newtonPolygon {R : Type u_1} [Ring R] (f : PowerSeries R) (v : AddValuation R (WithTop ℝ)) : ℕ → WithTop ℝ

The Newton polygon of a power series f with respect to a real additive valuation v: the lower convex envelope of the coefficient heights n ↦ v (coeff n f). If these heights have no real affine lower bound, it is the all-infinite fallback.

theorem PowerSeries.newtonPolygon_def {R : Type u_1} [Ring R] (f : PowerSeries R) (v : AddValuation R (WithTop ℝ)) : f.newtonPolygon v = TauCeti.lowerConvexEnvelope fun (n : ℕ) => v ((coeff n) f)

The Newton polygon is the lower convex envelope of the coefficient heights.

theorem PowerSeries.isConvexSeq_newtonPolygon {R : Type u_1} [Ring R] (f : PowerSeries R) (v : AddValuation R (WithTop ℝ)) : TauCeti.IsConvexSeq (f.newtonPolygon v)

The Newton polygon is convex, including the all-infinite fallback.

theorem PowerSeries.isLowerConvexEnvelope_newtonPolygon {R : Type u_1} [Ring R] {f : PowerSeries R} {v : AddValuation R (WithTop ℝ)} (hf : TauCeti.IsAdmissible fun (n : ℕ) => v ((coeff n) f)) : TauCeti.IsLowerConvexEnvelope (fun (n : ℕ) => v ((coeff n) f)) (f.newtonPolygon v)

For admissible coefficient heights, the Newton polygon is their greatest convex minorant.

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

For admissible coefficient heights, the Newton polygon lies below every coefficient point.

theorem PowerSeries.le_newtonPolygon {R : Type u_1} [Ring R] {f : PowerSeries R} {v : AddValuation R (WithTop ℝ)} {H : ℕ → WithTop ℝ} (hH : TauCeti.IsConvexSeq H) (hHf : ∀ (n : ℕ), H n ≤ v ((coeff n) f)) : H ≤ f.newtonPolygon v

A convex sequence lying below every coefficient height lies below the Newton polygon.

theorem PowerSeries.supportingValue_newtonPolygon {R : Type u_1} [Ring R] {f : PowerSeries R} {v : AddValuation R (WithTop ℝ)} (hf : TauCeti.IsAdmissible fun (n : ℕ) => v ((coeff n) f)) : TauCeti.supportingValue (f.newtonPolygon v) = TauCeti.supportingValue fun (n : ℕ) => v ((coeff n) f)

For admissible coefficient heights, the Newton polygon has the same supporting values as the coefficient heights.

@[simp]

theorem PowerSeries.newtonPolygon_zero {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) : newtonPolygon 0 v = ⊤

The zero power series has the empty Newton polygon.

theorem PowerSeries.newtonPolygon_eq_top_of_lt_order {R : Type u_1} [Ring R] {f : PowerSeries R} (v : AddValuation R (WithTop ℝ)) {n : ℕ} (hn : ↑n < f.order) : f.newtonPolygon v n = ⊤

Every point of the Newton polygon before the order of vanishing at zero is infinite.

theorem PowerSeries.newtonPolygon_eq_of_order_eq {R : Type u_1} [Ring R] {f : PowerSeries R} (v : AddValuation R (WithTop ℝ)) {n : ℕ} (hf : TauCeti.IsAdmissible fun (n : ℕ) => v ((coeff n) f)) (hn : f.order = ↑n) : f.newtonPolygon v n = v ((coeff n) f)

For admissible coefficient heights, the Newton polygon begins at the first nonzero coefficient.

@[simp]

theorem PowerSeries.newtonPolygon_neg {R : Type u_1} [Ring R] (f : PowerSeries R) (v : AddValuation R (WithTop ℝ)) : (-f).newtonPolygon v = f.newtonPolygon v

Negation does not change the Newton polygon.

theorem PowerSeries.newtonPolygon_smul {R : Type u_1} [Ring R] (f : PowerSeries R) (v : AddValuation R (WithTop ℝ)) (c : R) : (c • f).newtonPolygon v = fun (n : ℕ) => v c + f.newtonPolygon v n

Multiplying by a scalar translates the Newton polygon by the valuation of the scalar.

theorem PowerSeries.newtonPolygon_C_mul {R : Type u_1} [Ring R] (f : PowerSeries R) (v : AddValuation R (WithTop ℝ)) (c : R) : (C c * f).newtonPolygon v = fun (n : ℕ) => v c + f.newtonPolygon v n

Multiplying by a constant translates the Newton polygon by the valuation of the constant.

theorem PowerSeries.newtonPolygon_X_pow_mul {R : Type u_1} [Ring R] (f : PowerSeries R) (v : AddValuation R (WithTop ℝ)) (k : ℕ) : (X ^ k * f).newtonPolygon v = fun (n : ℕ) => if k ≤ n then f.newtonPolygon v (n - k) else ⊤

Multiplying by X ^ k shifts the Newton polygon k places to the right.

theorem PowerSeries.newtonPolygon_rescale {R : Type u_3} [CommRing R] (f : PowerSeries R) (v : AddValuation R (WithTop ℝ)) {c : R} (hc : v c ≠ ⊤) : ((rescale c) f).newtonPolygon v = fun (n : ℕ) => f.newtonPolygon v n + n • v c

Substituting c X for X shears the Newton polygon by the valuation of c, provided that valuation is finite.

theorem PowerSeries.newtonPolygon_map {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : PowerSeries R) (v : AddValuation R (WithTop ℝ)) (φ : R →+* S) {w : AddValuation S (WithTop ℝ)} (hφ : ∀ (x : R), w (φ x) = v x) : ((map φ) f).newtonPolygon w = f.newtonPolygon v

Mapping the coefficients along a ring homomorphism compatible with the valuations preserves the Newton polygon.

theorem PowerSeries.newtonPolygon_map_eq_map_mul {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : PowerSeries R) (v : AddValuation R (WithTop ℝ)) (φ : R →+* S) {w : AddValuation S (WithTop ℝ)} {c : ℝ} (hc : 0 < c) (hφ : ∀ (x : R), w (φ x) = WithTop.map (fun (x : ℝ) => c * x) (v x)) : ((map φ) f).newtonPolygon w = fun (n : ℕ) => WithTop.map (fun (x : ℝ) => c * x) (f.newtonPolygon v n)

Mapping the coefficients along a ring homomorphism that multiplies the valuations by a positive real factor multiplies the Newton polygon by that factor.

noncomputable def Polynomial.newtonPolygon {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : ℕ → WithTop ℝ

The Newton polygon of a polynomial f with respect to a real additive valuation v: the lower convex envelope of the coefficient heights n ↦ v (f.coeff n).

theorem Polynomial.newtonPolygon_def {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : f.newtonPolygon v = TauCeti.lowerConvexEnvelope fun (n : ℕ) => v (f.coeff n)

The Newton polygon is the lower convex envelope of the coefficient heights.

@[simp]

theorem Polynomial.newtonPolygon_coe {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : (↑f).newtonPolygon v = f.newtonPolygon v

The Newton polygon of a polynomial is that of the corresponding power series.

theorem Polynomial.isAdmissible_addValuation_coeff {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : TauCeti.IsAdmissible fun (n : ℕ) => v (f.coeff n)

The coefficient heights of a polynomial are admissible: they are infinite beyond the degree.

theorem Polynomial.finite_setOf_addValuation_coeff_ne_top {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : {n : ℕ | v (f.coeff n) ≠ ⊤}.Finite

A polynomial has only finitely many coefficients of finite height.

theorem Polynomial.isLowerConvexEnvelope_newtonPolygon {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : TauCeti.IsLowerConvexEnvelope (fun (n : ℕ) => v (f.coeff n)) (f.newtonPolygon v)

The Newton polygon of a polynomial is the greatest convex minorant of its coefficient heights.

theorem Polynomial.isConvexSeq_newtonPolygon {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : TauCeti.IsConvexSeq (f.newtonPolygon v)

The Newton polygon is convex.

theorem Polynomial.newtonPolygon_le {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (n : ℕ) : f.newtonPolygon v n ≤ v (f.coeff n)

The Newton polygon lies below every coefficient point.

@[simp]

theorem Polynomial.newtonPolygon_apply_zero {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : f.newtonPolygon v 0 = v (f.coeff 0)

At index zero the Newton polygon is the height of the constant coefficient, which may be infinite.

theorem Polynomial.le_newtonPolygon {R : Type u_1} [Ring R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {H : ℕ → WithTop ℝ} (hH : TauCeti.IsConvexSeq H) (hHf : ∀ (n : ℕ), H n ≤ v (f.coeff n)) : H ≤ f.newtonPolygon v

A convex sequence lying below every coefficient height lies below the Newton polygon.

theorem Polynomial.supportingValue_newtonPolygon {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : TauCeti.supportingValue (f.newtonPolygon v) = TauCeti.supportingValue fun (n : ℕ) => v (f.coeff n)

The Newton polygon has the same supporting values as the coefficient heights.

@[simp]

theorem Polynomial.newtonPolygon_zero {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) : newtonPolygon 0 v = ⊤

The zero polynomial has the empty Newton polygon.

theorem Polynomial.newtonPolygon_eq_top_iff {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : f.newtonPolygon v = ⊤ ↔ ∀ (n : ℕ), v (f.coeff n) = ⊤

The Newton polygon of a polynomial is empty exactly when every coefficient has infinite valuation.

Elementary operations

@[simp]

theorem Polynomial.newtonPolygon_neg {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : (-f).newtonPolygon v = f.newtonPolygon v

Negation does not change the Newton polygon.

theorem Polynomial.newtonPolygon_smul {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (c : R) : (c • f).newtonPolygon v = fun (n : ℕ) => v c + f.newtonPolygon v n

Multiplying by a scalar translates the Newton polygon by the valuation of the scalar.

theorem Polynomial.newtonPolygon_C_mul {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (c : R) : (C c * f).newtonPolygon v = fun (n : ℕ) => v c + f.newtonPolygon v n

Multiplying by a constant translates the Newton polygon by the valuation of the constant.

theorem Polynomial.newtonPolygon_X_pow_mul {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (k : ℕ) : (X ^ k * f).newtonPolygon v = fun (n : ℕ) => if k ≤ n then f.newtonPolygon v (n - k) else ⊤

Multiplying by X ^ k shifts the Newton polygon k places to the right.

theorem Polynomial.newtonPolygon_reflect {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) {N : ℕ} (hN : f.natDegree ≤ N) : (reflect N f).newtonPolygon v = fun (n : ℕ) => if n ≤ N then f.newtonPolygon v (N - n) else ⊤

Reflecting the coefficients in an index N at least the degree reflects the Newton polygon in N: its point at n ≤ N moves to N - n.

theorem Polynomial.newtonPolygon_reverse {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : f.reverse.newtonPolygon v = fun (n : ℕ) => if n ≤ f.natDegree then f.newtonPolygon v (f.natDegree - n) else ⊤

Reversing a polynomial of degree d reflects its Newton polygon by n ↦ d - n.

theorem Polynomial.newtonPolygon_comp_C_mul_X {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (c : R) : (f.comp (C c * X)).newtonPolygon v = fun (n : ℕ) => f.newtonPolygon v n + n • v c

Substituting c X for X shears the Newton polygon by the valuation of c. No finiteness is needed: when that valuation is infinite, the height at index 0 is unchanged and every later point becomes ⊤.

theorem Polynomial.newtonPolygon_map {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (φ : R →+* S) {w : AddValuation S (WithTop ℝ)} (hφ : ∀ (x : R), w (φ x) = v x) : (map φ f).newtonPolygon w = f.newtonPolygon v

Mapping the coefficients along a ring homomorphism compatible with the valuations preserves the Newton polygon.

theorem Polynomial.newtonPolygon_map_eq_map_mul {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (φ : R →+* S) {w : AddValuation S (WithTop ℝ)} {c : ℝ} (hc : 0 < c) (hφ : ∀ (x : R), w (φ x) = WithTop.map (fun (x : ℝ) => c * x) (v x)) : (map φ f).newtonPolygon w = fun (n : ℕ) => WithTop.map (fun (x : ℝ) => c * x) (f.newtonPolygon v n)

Mapping the coefficients along a ring homomorphism that multiplies the valuations by a positive real factor multiplies the Newton polygon by that factor. For instance, the ramification X ↦ X ^ q of Laurent series coefficients multiplies their orders by q.

Endpoints and finite domain

theorem Polynomial.newtonPolygon_eq_top_of_lt_natTrailingDegree {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) {n : ℕ} (hn : n < f.natTrailingDegree) : f.newtonPolygon v n = ⊤

Every point of the Newton polygon before the order of vanishing at zero is infinite.

theorem Polynomial.newtonPolygon_eq_top_of_natDegree_lt {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) {n : ℕ} (hn : f.natDegree < n) : f.newtonPolygon v n = ⊤

Every point of the Newton polygon beyond the degree is infinite.

@[simp]

theorem Polynomial.newtonPolygon_natTrailingDegree {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : f.newtonPolygon v f.natTrailingDegree = v f.trailingCoeff

The Newton polygon begins at the trailing coefficient.

theorem Polynomial.newtonPolygon_eq_of_natDegree_le {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) {n : ℕ} (hn : f.natDegree ≤ n) : f.newtonPolygon v n = v (f.coeff n)

At any index n at least the degree, the Newton polygon is the height of the coefficient of X ^ n: the leading coefficient when n is the degree, and ⊤ beyond it.

@[simp]

theorem Polynomial.newtonPolygon_natDegree {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : f.newtonPolygon v f.natDegree = v f.leadingCoeff

The Newton polygon ends at the leading coefficient.

theorem Polynomial.newtonPolygon_ne_top_iff_of_ne_top {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) {f : Polynomial R} (htr : v f.trailingCoeff ≠ ⊤) (hld : v f.leadingCoeff ≠ ⊤) {n : ℕ} : f.newtonPolygon v n ≠ ⊤ ↔ f.natTrailingDegree ≤ n ∧ n ≤ f.natDegree

If the trailing and leading coefficients of f have finite valuation, the finite domain of the Newton polygon of f runs from its order of vanishing at zero to its degree.

theorem Polynomial.newtonPolygon_ne_top_iff {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) (hv : ∀ (x : R), v x = ⊤ → x = 0) {f : Polynomial R} (hf : f ≠ 0) {n : ℕ} : f.newtonPolygon v n ≠ ⊤ ↔ f.natTrailingDegree ≤ n ∧ n ≤ f.natDegree

If only zero has infinite valuation, the finite domain of the Newton polygon of a nonzero polynomial runs from its order of vanishing at zero to its degree. Over a division ring the hypothesis on v is AddValuation.top_iff.

theorem Polynomial.newtonPolygon_ne_top_of_ne_zero {R : Type u_1} [Ring R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} (hv : ∀ (x : R), v x = ⊤ → x = 0) (hf : f ≠ 0) : f.newtonPolygon v ≠ ⊤

If only zero has infinite valuation, a nonzero polynomial has a nonempty Newton polygon. Over a division ring the hypothesis on v is AddValuation.top_iff.

theorem Polynomial.Monic.newtonPolygon_ne_top {R : Type u_1} [Ring R] {f : Polynomial R} (v : AddValuation R (WithTop ℝ)) (hf : f.Monic) : f.newtonPolygon v ≠ ⊤

A monic polynomial has a nonempty Newton polygon: its leading coefficient has valuation zero.

theorem Polynomial.finiteEdges_newtonPolygon_of_ne_top {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (htr : v f.trailingCoeff ≠ ⊤) (hld : v f.leadingCoeff ≠ ⊤) : TauCeti.finiteEdges (f.newtonPolygon v) = Set.Ico f.natTrailingDegree f.natDegree

If the trailing and leading coefficients of f have finite valuation, the finite unit edges of the Newton polygon of f are those between its order of vanishing at zero and its degree.

theorem Polynomial.finiteEdges_newtonPolygon {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (hv : ∀ (x : R), v x = ⊤ → x = 0) : TauCeti.finiteEdges (f.newtonPolygon v) = Set.Ico f.natTrailingDegree f.natDegree

If only zero has infinite valuation, the finite unit edges of the Newton polygon of a polynomial are those between its order of vanishing at zero and its degree.

theorem Polynomial.ncard_finiteEdges_newtonPolygon {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (hv : ∀ (x : R), v x = ⊤ → x = 0) : (TauCeti.finiteEdges (f.newtonPolygon v)).ncard = f.natDegree - f.natTrailingDegree

If only zero has infinite valuation, a polynomial of degree d and order of vanishing a at zero has exactly d - a finite unit edges.

theorem Polynomial.finiteEdges_newtonPolygon_monomial {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) (k : ℕ) (c : R) : TauCeti.finiteEdges (((monomial k) c).newtonPolygon v) = ∅

A monomial, in particular a constant, has no finite unit edges.