Gauss norms and Newton supporting values

Fix a real additive valuation v on a normed division ring and a base b > 1 with ‖x‖ = b ^ (-(v x).untop₀) for nonzero x. At the radius b ^ σ the weighted coefficient norm ‖aₙ‖ (b ^ σ) ^ n is b ^ (-(v aₙ - σ n)), the exponential of the negated tilted coefficient height. Consequently an upper bound b ^ (-c) on all weighted coefficient norms is exactly an affine line of slope σ and intercept c supporting the coefficient heights, and a weighted coefficient norm equals b ^ (-c) exactly when the coefficient lies on that line.

This identifies the analytic Gauss norm with the convex supporting-line description:

• the weighted coefficient norms are bounded exactly when the supporting value at σ is above negative infinity, and coefficient heights are admissible exactly when the series is restricted at some positive radius;
• for a nonzero series with bounded weighted coefficient norms, the supporting value of its coefficient heights, and of its Newton polygon, is -Real.logb b of its Gauss norm;
• the coefficients attaining the Gauss norm are exactly the contact points of the supporting line of slope σ, so the last and the first of them, TauCeti.PowerSeries.IsDistinguished and TauCeti.PowerSeries.IsLowestDominant, are the greatest and least contact indices.

Neither attainment nor restrictedness at the given radius is assumed: at the boundary of convergence the Gauss norm is still the supporting value, while it need not be attained. For polynomials the identities hold at every radius, and the purity criterion Polynomial.forall_mem_newtonSlopes_eq_iff becomes a statement about weighted norms: every finite slope equals m exactly when, at the radius b ^ m, the weighted leading and trailing terms have equal norms and bound all other weighted terms. The norm and valuation are compared by an explicit hypothesis, so no normalisation is hidden in a typeclass instance.

Main results

• PowerSeries.isSupportingLine_addValuation_coeff_iff: affine minorants of the coefficient heights are exponential bounds on the weighted coefficient norms.
• PowerSeries.hasGaussNorm_iff_supportingValue_ne_bot: bounded weighted coefficient norms correspond to a supporting value above negative infinity.
• PowerSeries.isAdmissible_addValuation_coeff_iff_exists_isRestricted: coefficient heights are admissible exactly when the series is restricted at some positive radius.
• PowerSeries.supportingValue_newtonPolygon_eq_neg_logb_gaussNorm: the supporting value of the Newton polygon is the negative logarithm of the Gauss norm, with the polynomial case Polynomial.supportingValue_newtonPolygon_eq_neg_logb_gaussNorm at every radius.
• Polynomial.forall_mem_newtonSlopes_eq_iff_norm_coeff_mul_rpow_pow_le: the purity criterion in terms of weighted coefficient norms at the radius b ^ m.
• PowerSeries.mem_supportingFace_addValuation_coeff_iff: the contact indices of the supporting line are the indices attaining the Gauss norm.
• PowerSeries.isDistinguished_iff_isGreatest_supportingFace and PowerSeries.isLowestDominant_iff_isLeast_supportingFace: the last and the first coefficient attaining the Gauss norm are the greatest and least contact indices.
• PowerSeries.exists_isSupportingLine_mem_supportingFace_of_isRestricted: the coefficient heights of a nonzero series restricted at b ^ σ touch a supporting line of slope σ.

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.
• 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. Lazard's variable is a valuation threshold, corresponding to -σ here.

theorem PowerSeries.norm_coeff_mul_rpow_pow_eq {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {n : ℕ} (hn : (coeff n) f ≠ 0) (σ : ℝ) : ‖(coeff n) f‖ * (b ^ σ) ^ n = b ^ (-((v ((coeff n) f)).untop₀ - σ * ↑n))

At a nonzero coefficient, the weighted norm is the exponential of the negated tilted coefficient height.

theorem PowerSeries.norm_coeff_mul_rpow_pow_le_iff {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) (n : ℕ) (σ c : ℝ) : ‖(coeff n) f‖ * (b ^ σ) ^ n ≤ b ^ (-c) ↔ ↑(c + σ * ↑n) ≤ v ((coeff n) f)

An exponential upper bound on one weighted coefficient norm is an affine lower bound on the height of that coefficient. A zero coefficient satisfies both bounds.

theorem PowerSeries.norm_coeff_mul_rpow_pow_eq_iff {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) (n : ℕ) (σ c : ℝ) : ‖(coeff n) f‖ * (b ^ σ) ^ n = b ^ (-c) ↔ v ((coeff n) f) = ↑(c + σ * ↑n)

A weighted coefficient norm equals b ^ (-c) exactly when the coefficient lies on the line of slope σ and intercept c. A zero coefficient satisfies neither condition.

theorem PowerSeries.isSupportingLine_addValuation_coeff_iff {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) (σ c : ℝ) : TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) f)) σ c ↔ ∀ (n : ℕ), ‖(coeff n) f‖ * (b ^ σ) ^ n ≤ b ^ (-c)

A line of slope σ and intercept c supports the coefficient heights exactly when b ^ (-c) bounds every weighted coefficient norm at the radius b ^ σ. No boundedness assumption is needed.

theorem PowerSeries.hasGaussNorm_iff_supportingValue_ne_bot {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) (σ : ℝ) : HasGaussNorm norm (b ^ σ) f ↔ TauCeti.supportingValue (fun (n : ℕ) => v ((coeff n) f)) σ ≠ ⊥

Bounded weighted coefficient norms are equivalent to a supporting value above negative infinity, including for the zero series. This is weaker than restrictedness.

theorem PowerSeries.isSupportingLine_addValuation_coeff_iff_gaussNorm_le {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {σ : ℝ} (hf : HasGaussNorm norm (b ^ σ) f) (c : ℝ) : TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) f)) σ c ↔ gaussNorm norm (b ^ σ) f ≤ b ^ (-c)

For bounded weighted coefficient norms, a line of slope σ and intercept c supports the coefficient heights exactly when b ^ (-c) bounds the Gauss norm at the radius b ^ σ.

theorem PowerSeries.isAdmissible_addValuation_coeff_iff_exists_isRestricted {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) : (TauCeti.IsAdmissible fun (n : ℕ) => v ((coeff n) f)) ↔ ∃ (r : ℝ), 0 < r ∧ IsRestricted r f

Coefficient heights are admissible exactly when the series is restricted at some positive radius. This includes the zero series, whose heights are all infinite.

theorem PowerSeries.supportingValue_addValuation_coeff_eq_neg_logb_gaussNorm {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {σ : ℝ} (hf : HasGaussNorm norm (b ^ σ) f) (hf0 : f ≠ 0) : TauCeti.supportingValue (fun (n : ℕ) => v ((coeff n) f)) σ = ↑(-Real.logb b (gaussNorm norm (b ^ σ) f))

For a nonzero series with bounded weighted coefficient norms, the supporting value of its coefficient heights is the negative base-b logarithm of its Gauss norm. The Gauss norm need not be attained.

theorem PowerSeries.supportingValue_newtonPolygon_eq_neg_logb_gaussNorm {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {σ : ℝ} (hf : HasGaussNorm norm (b ^ σ) f) (hf0 : f ≠ 0) : TauCeti.supportingValue (f.newtonPolygon v) σ = ↑(-Real.logb b (gaussNorm norm (b ^ σ) f))

The Newton polygon of a nonzero series with bounded weighted coefficient norms has supporting value equal to the negative base-b logarithm of the Gauss norm. Boundedness at this radius already makes the coefficient heights admissible.

theorem PowerSeries.mem_supportingFace_addValuation_coeff_iff {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {σ : ℝ} (hf : HasGaussNorm norm (b ^ σ) f) (hf0 : f ≠ 0) (n : ℕ) : n ∈ TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) f)) σ (-Real.logb b (gaussNorm norm (b ^ σ) f)) ↔ ‖(coeff n) f‖ * (b ^ σ) ^ n = gaussNorm norm (b ^ σ) f

For a nonzero series with bounded weighted coefficient norms, the coefficients touching the supporting line of slope σ are exactly those attaining the Gauss norm at the radius b ^ σ. The intercept of that line is the supporting value -Real.logb b (f.gaussNorm norm (b ^ σ)).

theorem PowerSeries.isDistinguished_iff_isGreatest_supportingFace {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {σ : ℝ} (hf : HasGaussNorm norm (b ^ σ) f) (s : ℕ) : TauCeti.PowerSeries.IsDistinguished (b ^ σ) s f ↔ IsGreatest (TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) f)) σ (-Real.logb b (gaussNorm norm (b ^ σ) f))) s

The distinguished degree at the radius b ^ σ, the last index attaining the Gauss norm, is the greatest contact index of the supporting line of slope σ with the coefficient heights.

theorem PowerSeries.isLowestDominant_iff_isLeast_supportingFace {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {σ : ℝ} (hf : HasGaussNorm norm (b ^ σ) f) (s : ℕ) : TauCeti.PowerSeries.IsLowestDominant (b ^ σ) s f ↔ IsLeast (TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) f)) σ (-Real.logb b (gaussNorm norm (b ^ σ) f))) s

The lowest dominant degree at the radius b ^ σ, the first index attaining the Gauss norm, is the least contact index of the supporting line of slope σ with the coefficient heights.

theorem PowerSeries.exists_isSupportingLine_mem_supportingFace_of_isRestricted {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {σ : ℝ} (hf : IsRestricted (b ^ σ) f) (hf0 : f ≠ 0) : ∃ (c : ℝ) (i : ℕ), TauCeti.IsSupportingLine (fun (n : ℕ) => v ((coeff n) f)) σ c ∧ i ∈ TauCeti.supportingFace (fun (n : ℕ) => v ((coeff n) f)) σ c

The coefficient heights of a nonzero series restricted at the radius b ^ σ touch a supporting line of slope σ.

theorem PowerSeries.supportingValue_newtonPolygon_ne_bot_of_isRestricted {K : Type u_1} [NormedDivisionRing K] (f : PowerSeries K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {σ : ℝ} (hf : IsRestricted (b ^ σ) f) : TauCeti.supportingValue (f.newtonPolygon v) σ ≠ ⊥

A series restricted at the radius b ^ σ has a Newton polygon whose supporting value at σ is above ⊥.

theorem Polynomial.supportingValue_newtonPolygon_eq_neg_logb_gaussNorm {K : Type u_1} [NormedDivisionRing K] (p : Polynomial K) (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) (hp : p ≠ 0) (σ : ℝ) : TauCeti.supportingValue (p.newtonPolygon v) σ = ↑(-Real.logb b (PowerSeries.gaussNorm norm (b ^ σ) ↑p))

At every slope σ, the Newton polygon of a nonzero polynomial has supporting value equal to the negative base-b logarithm of its Gauss norm at the radius b ^ σ.

theorem Polynomial.forall_mem_newtonSlopes_eq_iff_norm_coeff_mul_rpow_pow_le {K : Type u_1} [NormedDivisionRing K] {v : AddValuation K (WithTop ℝ)} {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f : Polynomial K} {m : ℝ} : (∀ s ∈ f.newtonSlopes v, s = m) ↔ ‖f.leadingCoeff‖ * (b ^ m) ^ f.natDegree = ‖f.trailingCoeff‖ * (b ^ m) ^ f.natTrailingDegree ∧ ∀ (n : ℕ), ‖f.coeff n‖ * (b ^ m) ^ n ≤ ‖f.trailingCoeff‖ * (b ^ m) ^ f.natTrailingDegree

Purity criterion, Gauss form. Let the norm be ‖x‖ = b ^ (-v x) for x ≠ 0, with 1 < b. Every finite slope of f equals m exactly when, at the radius b ^ m, the weighted leading and trailing terms have the same norm and every weighted term has norm at most that of the trailing term.