The Gauss norm of restricted power series #
A restricted power series has finite Gauss norm. At a positive radius, a nonzero restricted
series has a last coefficient attaining that norm; the degree of that coefficient is the
distinguished degree of the series, and IsDistinguished names the property. Over a
nonarchimedean normed ring with multiplicative norm, a pair of distinguished degrees produces a
dominant coefficient in a product, and the Gauss norm is therefore multiplicative on restricted
series.
The distinguished degree is the datum Weierstrass division and preparation for Tate algebras are organised around. No completeness hypothesis is needed for the norm identities here. The radius is any positive real number, including the unit radius of the usual Tate algebra.
Completeness enters only in the summation section, where a family of restricted series with summable Gauss norms is summed coefficientwise. This is the convergence statement that successive-approximation arguments over a complete nonarchimedean ring run on, and it takes the place of completeness of the Tate algebra for the Gauss norm.
Multiplicativity and the ultrametric inequality together make the Gauss norm a valuation with
values in ℝ≥0 on the ring of restricted series, gaussValuation, whose support is trivial.
Pulled back to the Tate algebra at radii at most one, these valuations give the Gauss points of the
closed unit disc.
Main definitions #
TauCeti.PowerSeries.gaussValuation: at a positive radius, the Gauss norm as a valuation with values inℝ≥0on the ring of restricted series.TauCeti.PowerSeries.IsDistinguished: the Gauss norm is attained in degreesand every later coefficient is strictly smaller.
Main results #
TauCeti.PowerSeries.gaussNorm_eq_of_forall_le: the Gauss norm is attained at a degree whose weighted coefficient dominates.TauCeti.PowerSeries.exists_isDistinguished: at a positive radius, every nonzero restricted series is distinguished of some degree.TauCeti.PowerSeries.IsDistinguished.unique: of no more than one degree.TauCeti.PowerSeries.isDistinguished_of_norm_coeff_sub_lt: over an ultrametric ring, a series is distinguished once its coefficient in degreesis close to an element of maximal norm.TauCeti.PowerSeries.IsDistinguished.trunc,TauCeti.PowerSeries.IsDistinguished.gaussNorm_truncandTauCeti.PowerSeries.IsDistinguished.gaussNorm_sub_trunc_lt: the polynomial part of a distinguished series is distinguished of the same degree and the same Gauss norm, and the tail it leaves is strictly smaller.TauCeti.PowerSeries.IsDistinguished.norm_coeff_mul_mul_pow_eq_gaussNorm_mul: the dominant coefficient of a product of distinguished series.TauCeti.PowerSeries.gaussNorm_mul_of_isRestricted: multiplicativity of the Gauss norm.TauCeti.PowerSeries.gaussValuation_eq_zero_iff: the Gauss valuation vanishes only at zero.TauCeti.PowerSeries.summable_coeff_of_summable_gaussNormandTauCeti.PowerSeries.isRestricted_mk_tsum_coeff: over a complete ring, a family of restricted series with summable Gauss norms has summable coefficients, and its coefficientwise sum is again restricted.
References #
- Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.
The dominant-coefficient argument follows Mathlib's proof of Polynomial.gaussNorm_mul;
restrictedness replaces the finite-support argument for attaining the maximum. We use Mathlib's
PowerSeries.IsRestricted and PowerSeries.gaussNorm throughout.
A restricted power series has bounded weighted coefficient norms.
If the weighted coefficient in degree s dominates every other one, the Gauss norm is the
value it takes there.
f is distinguished of degree s at the radius c when its Gauss norm at c is attained
in degree s and every later coefficient is strictly smaller.
At the unit radius this is a norm-theoretic analogue of the classical condition that the leading
coefficient of f dominates, in the sense of Bosch–Güntzer–Remmert §5.2. At a positive radius, a
nonzero restricted series is distinguished of exactly one degree
(TauCeti.PowerSeries.exists_isDistinguished and
TauCeti.PowerSeries.IsDistinguished.unique), so this is a genuine invariant of f and c rather
than extra data.
The first field is the univariate reading of Mathlib's MvPowerSeries.AchievesGaussNorm; the
second is what makes the degree unique and pins down the dominant coefficient of a product.
This is unrelated to Polynomial.IsDistinguishedAt, which asks a polynomial to be monic with its
remaining coefficients in an ideal.
The Gauss norm is attained in degree
s.- norm_coeff_mul_pow_lt (m : ℕ) : s < m → ‖(PowerSeries.coeff m) f‖ * c ^ m < PowerSeries.gaussNorm norm c f
Every coefficient in a degree past
sis strictly smaller.
Instances For
A distinguished series has positive Gauss norm, without any sign assumption on the radius.
A distinguished series is nonzero.
The coefficient of a distinguished series in its distinguished degree is nonzero.
The weighted coefficient norms of a distinguished series are bounded above.
The distinguished degree is unique: a series cannot be distinguished of two degrees at the same radius.
Every nonzero restricted series is distinguished of some degree: its last coefficient attaining the Gauss norm supplies that degree.
Truncating a series just past a degree in which its Gauss norm is attained leaves that norm unchanged.
The truncation of a distinguished series just past its distinguished degree is again
distinguished of that degree. It is the polynomial part f⁻ a Weierstrass division divides by.
The tail f⁺ left by truncating a restricted distinguished series just past its
distinguished degree has strictly smaller Gauss norm than the series itself. This is the
contraction factor of the Weierstrass division algorithm.
Recognising a distinguished series. At a positive radius, f is distinguished of degree
s once its weighted coefficient in degree s is closer than the Gauss norm to an element a
of weighted norm equal to the Gauss norm, and every later weighted coefficient norm is smaller
than the Gauss norm.
The sum of two power series with bounded weighted coefficient norms again has bounded weighted coefficient norms at a nonnegative radius.
The product of two power series with bounded weighted coefficient norms again has bounded weighted coefficient norms at a nonnegative radius.
Over a complete ring, a family of power series with summable Gauss norms has summable coefficients in every degree.
Coefficientwise summation of restricted power series. Over a complete nonarchimedean ring, the degreewise sums of a family of restricted power series with summable Gauss norms assemble into a restricted power series.
This is the convergence statement behind successive-approximation arguments such as Weierstrass division: it plays the role of completeness of the Tate algebra for the Gauss norm.
The dominant coefficient of a product of distinguished series. If f is distinguished of
degree i and g of degree j, then the coefficient of f * g in degree i + j realises the
product of the two Gauss norms.
The Gauss norm is multiplicative on restricted power series at every positive radius.
The product of series distinguished in degrees i and j is distinguished in degree
i + j at a positive radius.
The Gauss valuation #
The Gauss valuation at a positive radius c: the Gauss norm f ↦ sup ‖aₙ‖ cⁿ, as a
valuation with values in ℝ≥0 on the ring of power series restricted at c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Gauss valuation is the Gauss norm, read in ℝ.
The Gauss valuation of a constant series is the norm of its coefficient.
The Gauss valuation of the variable is the radius.
The Gauss valuation vanishes only at zero: its support is trivial.