Documentation

TauCeti.RingTheory.PowerSeries.Restricted

Restricted power series and their coefficient algebra #

Mathlib's PowerSeries.IsRestricted asks the weighted coefficient norms of a power series to tend to zero. A series whose coefficients vanish in every degree past some bound — a polynomial — satisfies that condition at every radius, and a series restricted at one radius is restricted at every smaller one. Over an ultrametric normed commutative ring, constant series give the restricted subring its coefficient algebra structure. The polynomial inclusion is an algebra homomorphism; it induces the polynomial-to-series comparisons used in Weierstrass division and its quotients.

Main results #

source
theorem TauCeti.PowerSeries.isRestricted_of_forall_coeff_eq_zero {R : Type u_1} [NormedRing R] {c : ℝ} {f : PowerSeries R} {n : ℕ} (hf : ∀ (m : ℕ), n ≤ m → (PowerSeries.coeff m) f = 0) :
PowerSeries.IsRestricted c f

A power series whose coefficients vanish in every degree ≥ n is restricted at every radius: its weighted coefficient norms are eventually zero. Such a series is a polynomial of degree less than n.

source
theorem TauCeti.PowerSeries.isRestricted_of_abs_le {R : Type u_1} [NormedRing R] {c : ℝ} {f : PowerSeries R} {c' : ℝ} (hf : PowerSeries.IsRestricted c' f) (h : |c| ≤ |c'|) :
PowerSeries.IsRestricted c f

Restrictedness passes to smaller radii. If the weighted coefficient norms of f tend to zero at the radius c', they do so at every radius c with |c| ≤ |c'|, being dominated by the former.

source
theorem TauCeti.PowerSeries.isRestrictedSubring_le_of_abs_le {R : Type u_1} [NormedRing R] {c : ℝ} [IsUltrametricDist R] {c' : ℝ} (h : |c| ≤ |c'|) :
PowerSeries.IsRestricted.subring c' ≤ PowerSeries.IsRestricted.subring c

Over an ultrametric ring, the subring of series restricted at c' lies in the subring of series restricted at any c with |c| ≤ |c'|.

source
theorem TauCeti.PowerSeries.isRestricted_polynomial {R : Type u_1} [NormedRing R] {c : ℝ} (p : Polynomial R) :
PowerSeries.IsRestricted c ↑p

Every polynomial is restricted at every radius.

source
@[instance_reducible]
noncomputable instance TauCeti.PowerSeries.instAlgebraIsRestrictedSubring {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} :
Algebra R ↥(PowerSeries.IsRestricted.subring c)

The coefficient algebra structure on restricted power series, given by constant series.

Equations
source
@[simp]
theorem TauCeti.PowerSeries.coe_algebraMap_isRestrictedSubring {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} (a : R) :
↑((algebraMap R ↥(PowerSeries.IsRestricted.subring c)) a) = PowerSeries.C a

The coefficient map of the restricted-series algebra is the constant series map.

source
noncomputable def TauCeti.PowerSeries.polynomialToRestricted {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (c : ℝ) :
Polynomial R →ₐ[R] ↥(PowerSeries.IsRestricted.subring c)

The inclusion of polynomials into the algebra of restricted power series.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.PowerSeries.coe_polynomialToRestricted {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} (p : Polynomial R) :
    ↑((polynomialToRestricted c) p) = ↑p

    The polynomial inclusion has the usual underlying power series.

    source
    theorem TauCeti.PowerSeries.polynomialToRestricted_trunc_eq_of_coeff_eq_zero {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {s : ℕ} (r : ↥(PowerSeries.IsRestricted.subring c)) (hr : ∀ (n : ℕ), s ≤ n → (PowerSeries.coeff n) ↑r = 0) :
    (polynomialToRestricted c) ((PowerSeries.trunc s) ↑r) = r

    A restricted series whose coefficients vanish from degree s onward is the polynomial inclusion of its s-truncation.