Polynomials with coefficients in the closed unit ball

Over an ultrametric normed commutative ring with ‖1‖ = 1, the multivariate polynomials whose coefficients all have norm at most 1 are closed under products and powers: each coefficient of a product is a finite sum of products of coefficients, so the ultrametric inequality bounds it by 1.

This is the estimate that makes substituting such polynomials into restricted power series preserve unit-radius restrictedness and not increase the Gauss norm.

Main results

• TauCeti.MvPolynomial.norm_coeff_prod_pow_le_one: a product of powers of polynomials with coefficients of norm at most 1 again has coefficients of norm at most 1.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.1.3.

theorem TauCeti.MvPolynomial.norm_coeff_prod_pow_le_one {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] {a : σ → MvPolynomial τ R} (ha : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) (d : σ →₀ ℕ) (t : τ →₀ ℕ) : ‖(d.prod fun (s : σ) (n : ℕ) => a s ^ n).coeff t‖ ≤ 1

Products of powers of polynomials whose coefficients have norm at most 1 again have coefficients of norm at most 1.