The Weierstrass quotient and remainder as linear maps #
Let R be a complete ultrametric normed commutative ring, c > 0 a radius, and g a series
restricted at c which is multiplicatively distinguished of degree s
(TauCeti.PowerSeries.IsMulDistinguished). Weierstrass division by g
(TauCeti.PowerSeries.IsMulDistinguished.existsUnique_mul_add_eq) writes every series f
restricted at c uniquely as
f = g * q + r, q restricted at c, r a polynomial of degree less than s.
This file names the quotient q and the remainder r as functions of f, for fixed g. By
uniqueness they are R-linear, so they are recorded as linear maps
weierstrassDiv : R⟨c⁻¹X⟩ →ₗ[R] R⟨c⁻¹X⟩, weierstrassMod : R⟨c⁻¹X⟩ →ₗ[R] R[X]
on the ring PowerSeries.IsRestricted.subring c of series restricted at c. They are
characterised by the division identity and the degree bound on the remainder, they send g * q
to (q, 0) and a polynomial of degree less than s to (0, p), and the remainder vanishes
exactly on the multiples of g. The Gauss norm at c satisfies
‖f‖ = max (‖g‖ * ‖weierstrassDiv f‖) ‖weierstrassMod f‖,
so for the Gauss norm the quotient map is bounded by ‖g‖⁻¹ and the remainder map by 1; in
particular the
quotient map is continuous for the Gauss-norm topology. The norm of R need not be
multiplicative, and R may have nilpotents.
Main definitions #
TauCeti.PowerSeries.IsMulDistinguished.weierstrassDiv: the Weierstrass quotient byg.TauCeti.PowerSeries.IsMulDistinguished.weierstrassMod: the Weierstrass remainder byg, a polynomial of degree less thans.
Main results #
TauCeti.PowerSeries.IsMulDistinguished.mul_weierstrassDiv_add_weierstrassModandTauCeti.PowerSeries.IsMulDistinguished.degree_weierstrassMod_lt: the division identity.TauCeti.PowerSeries.IsMulDistinguished.weierstrassDiv_eq_and_weierstrassMod_eq_iff: any decompositiong * q + rwithdeg r < sis the Weierstrass division.TauCeti.PowerSeries.IsMulDistinguished.weierstrassMod_eq_zero_iff_dvd: the remainder vanishes exactly on multiples ofg.TauCeti.PowerSeries.IsMulDistinguished.gaussNorm_eq_max,TauCeti.PowerSeries.IsMulDistinguished.gaussNorm_weierstrassDiv_leandTauCeti.PowerSeries.IsMulDistinguished.gaussNorm_weierstrassMod_le: the norm identity and the bounds‖q‖ ≤ ‖f‖ / ‖g‖and‖r‖ ≤ ‖f‖.TauCeti.PowerSeries.IsMulDistinguished.continuous_weierstrassDiv: the quotient map is continuous.
References #
- F. Martin, Overconvergent subanalytic subsets in the framework of Berkovich spaces, J. Eur. Math. Soc. 18 (2016), Proposition 1.27, for division by a multiplicatively distinguished series over a Banach ring and its norm estimates.
- Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.1, Theorem 2, for the field case.
The names and the shape of the characterising lemmas follow Mathlib's PowerSeries.weierstrassDiv
and PowerSeries.weierstrassMod, the quotient and remainder of the ideal-adic Weierstrass division
over a complete local ring; that is a different division theorem, for a different notion of
divisor.
The Weierstrass quotient by a restricted series g multiplicatively distinguished of
degree s at a radius c > 0, over a complete ultrametric normed commutative ring: the
restricted series q in the unique decomposition f = g * q + r with r a polynomial of degree
less than s. It is R-linear in f.
Instances For
The Weierstrass remainder by a restricted series g multiplicatively distinguished of
degree s at a radius c > 0, over a complete ultrametric normed commutative ring: the
polynomial r of degree less than s in the unique decomposition f = g * q + r with q
restricted. It is R-linear in f.
Instances For
The Weierstrass remainder has degree less than the distinguished degree.
The Weierstrass division identity: f = g * q + r for the Weierstrass quotient q and
remainder r of f.
Uniqueness of the Weierstrass quotient and remainder. A decomposition g * q + r of f
with r a polynomial of degree less than s is the Weierstrass division of f.
The Weierstrass quotient of g * q + r, with r a polynomial of degree less than s,
is q.
The Weierstrass remainder of g * q + r, with r a polynomial of degree less than s,
is r.
Dividing a multiple g * q by g returns q.
A multiple g * q has Weierstrass remainder zero.
A polynomial of degree less than s has Weierstrass quotient zero.
A polynomial of degree less than s is its own Weierstrass remainder.
For a monic polynomial divisor, the Weierstrass remainder of a polynomial agrees with ordinary polynomial remainder.
The Weierstrass remainder of f vanishes exactly when g divides f in the ring of
restricted series.
In distinguished degree zero every Weierstrass remainder is zero.
The Weierstrass norm identity. The Gauss norm of f at c is the larger of
‖g‖ * ‖q‖ and ‖r‖, for its Weierstrass quotient q and remainder r.
The Weierstrass quotient bound ‖q‖ ≤ ‖f‖ / ‖g‖, for the Gauss norm at c.
The Weierstrass remainder bound ‖r‖ ≤ ‖f‖, for the Gauss norm at c.
The Weierstrass quotient map is continuous for the Gauss-norm topology at c: it is bounded
by ‖g‖⁻¹.