The Gauss norm on multivariate restricted power series #
For positive polyradii c : σ → ℝ, the restricted-series subring of
MvPowerSeries σ R carries the Gauss norm, the supremum of the weighted coefficient norms
‖aₜ‖ * ∏ i ∈ t.support, c i ^ t i. Over an ultrametric normed ring this makes it a normed
ring, complete when the coefficient ring is complete. A multiplicative coefficient norm gives
a multiplicative Gauss norm. These structures let multivariate Tate algebras serve as coefficient
rings for Weierstrass division in another variable.
No finiteness assumption on the variable type is needed: restrictedness is convergence of the coefficients along the cofinite filter on the exponent set.
The construction follows TauCeti.RingTheory.PowerSeries.TateAlgebra, using Mathlib's
multivariate restricted-series subring and Gauss norm. Multiplicativity selects a largest
Gauss-norm-achieving exponent in a lexicographic order; its product coefficient has a unique
largest summand, so Mathlib's dominant-antidiagonal theorem applies.
Main results #
MvPowerSeries.norm_eq_gaussNorm: the norm is the Gauss norm at the chosen polyradii.MvPowerSeries.norm_le_iff: a norm bound is equivalent to bounds on every weighted coefficient.MvPowerSeries.exists_achievesGaussNormandMvPowerSeries.exists_norm_coeff_mul_prod_gap: a restricted series attains its norm, and its smaller weighted coefficient norms stay below a constant smaller than its norm.- The restricted-series subring inherits
CompleteSpace,IsUltrametricDist, andNormMulClassfrom its coefficient ring. - Over a normed field, the restricted-series subring is a
NormedAlgebraover its coefficients.
References #
- Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.1.1 and §5.2.1.
Restricted series have bounded weighted coefficient norms.
At positive polyradii the restricted-series subring carries its Gauss norm.
Equations
- One or more equations did not get rendered due to their size.
The norm of a restricted series is its Gauss norm at the chosen polyradii.
Every weighted coefficient norm is bounded by the Gauss norm of the restricted series.
A nonnegative bound on the norm is exactly a bound on every weighted coefficient norm.
The norm gap of a restricted series. The weighted coefficient norms of a nonzero restricted series that are smaller than its norm are bounded by a constant smaller than its norm: only finitely many of them exceed half the norm.
A restricted series attains its Gauss norm at some exponent.
The norm of a restricted monomial is its weighted coefficient norm.
Each variable has norm equal to its radius when the coefficient norm of 1 is 1.
The Gauss norm is ultrametric when the coefficient norm is.
The Gauss norm preserves the norm of 1 from the coefficient ring.
The restricted-series Gauss norm is complete over a complete coefficient ring.
The Gauss norm of a product of restricted series is the product of their Gauss norms when the coefficient norm is multiplicative. Positive polyradii are arbitrary.
The Gauss norm inherits multiplicativity from the coefficient norm.
Restricted series form a coefficient algebra via the constant-series embedding.
The coefficient algebra map into restricted series is the constant-series embedding.
Over a commutative coefficient ring, the Gauss norm gives a normed commutative ring.
Equations
- MvPowerSeries.instNormedCommRingIsRestrictedSubring = { toNormedRing := MvPowerSeries.instNormedRingIsRestrictedSubring, mul_comm := ⋯ }
At positive polyradii, restricted series form a normed algebra over their ultrametric coefficient field.
Equations
- MvPowerSeries.instNormedAlgebraIsRestrictedSubring = { toAlgebra := MvPowerSeries.instAlgebraIsRestrictedSubring, norm_smul_le := ⋯ }