Evaluation of power series and division by X - C c #
Mathlib evaluates a power series over R at a topologically nilpotent point a of a complete,
separated, linearly topologized R-algebra S through PowerSeries.aeval. This file records the
values of that evaluation on the generators, X ↦ a and C r ↦ algebraMap R S r, expands it as
the series ∑ c n • aⁿ when the coefficients come from a scalar ring acting on R and S, shows
that a series without constant term evaluates to a multiple of a, and performs division by a
linear factor over a ring A in which power series can be evaluated at c:
f = (X - C c) * divXSubC hc f + C (f(c)),
where the quotient PowerSeries.divXSubC hc f is the explicit series whose n-th coefficient is
the value at c of the tail ∑ₖ f_{n+1+k} X^k of f, that is ∑ₖ f_{n+1+k} c^k. The identity
is checked coefficientwise from the recursion tailₙ(c) = fₙ + c * tailₙ₊₁(c), which is
PowerSeries.aeval applied to tailₙ = X * tailₙ₊₁ + C fₙ. The divisibility criterion
(X - C c) ∣ f ↔ f(c) = 0
follows: one direction is that X - C c evaluates to zero, and the other reads off the
factorization once the remainder f(c) vanishes. This is the special case of Weierstrass division
by X - C c that a complete local ring such as ℤ_[p] uses at a point c of its maximal ideal;
the explicit quotient makes the general division theorem unnecessary here.
The evaluability hypothesis HasEval c is where the topology enters: it is what makes the tails
of f evaluable at c, and it already excludes the units. For a unit c the series X - C c
is a unit of A⟦X⟧, so it divides everything, while f(c) need not vanish; and a unit is
topologically nilpotent only in the zero ring.
A fixed series is also continuous in a continuously varying admissible argument under a linear
topology; PowerSeries.continuous_eval₂_of_continuous specializes the multivariate result.
Main results #
PowerSeries.continuous_eval₂_of_continuous: continuity in the admissible evaluation point.PowerSeries.algHom_coe_eq_aeval: any algebra map out ofA⟦X⟧, continuous or not, restricts on polynomials to the polynomial evaluation at the image ofX.PowerSeries.constantCoeff_polynomial_aeval: the constant coefficient of a polynomial evaluated at a power seriesfis the polynomial evaluated at the constant coefficient off.PowerSeries.aeval_X,PowerSeries.aeval_C: the values of evaluation on the generators.PowerSeries.hasSum_smul_pow_aeval: the series expansion of the evaluation of a power series whose coefficients come from a scalar ring.PowerSeries.exists_aeval_eq_mul_of_constantCoeff_eq_zero,PowerSeries.isTopologicallyNilpotent_aeval_of_constantCoeff_eq_zero: a series without constant term evaluates atato a multiple ofa, hence to a topologically nilpotent element.PowerSeries.aeval_mem_of_constantCoeff_eq_zero: a series without constant term evaluates at a point of an ideal to an element of that ideal.PowerSeries.aeval_rescale: the rescaled seriesf(r X)evaluates atatof(r • a).PowerSeries.divXSubC: the quotient of a power series on division byX - C c, with its coefficientsPowerSeries.coeff_divXSubCand their series expansionPowerSeries.hasSum_coeff_divXSubC.PowerSeries.X_sub_C_mul_divXSubC_add_C_aeval: the divisionf = (X - C c) * q + C (f(c)).PowerSeries.X_sub_C_mul_divXSubC: the factorizationf = (X - C c) * qwhenf(c) = 0.PowerSeries.X_sub_C_dvd_iff_aeval_eq_zero: divisibility byX - C cis vanishing atc.
References #
- L. C. Washington, Introduction to Cyclotomic Fields, Proposition 7.2 (Weierstrass division).
A fixed power series is continuous in a continuously varying admissible argument. No common ideal of definition for the arguments is required.
An A-algebra map out of A⟦X⟧ restricts on polynomials to evaluation at the image of X.
No continuity is assumed.
Evaluating a polynomial at a power series f and taking the constant coefficient is
evaluating it at the constant coefficient of f.
Evaluation at a sends X to a.
Evaluation at a sends a constant to its image in S.
A power series whose coefficients are the images algebraMap A R (c n) of scalars from a ring
A acting compatibly on R and S evaluates at a to the sum of the series ∑ c n • aⁿ.
A power series without constant term evaluates at a to a multiple of a.
A power series without constant term evaluates at a point a of an ideal I to an element
of I.
A power series without constant term evaluates at a topologically nilpotent a to a
topologically nilpotent element.
Evaluating the rescaled series f(r X) at a is evaluating f at r • a.
The quotient of a power series f on division by X - C c, at a point c where power series
can be evaluated: its n-th coefficient is the value at c of the tail ∑ₖ f_{n+1+k} X^k of f.
The remainder is the constant f(c); see PowerSeries.X_sub_C_mul_divXSubC_add_C_aeval.
Instances For
The n-th coefficient of the quotient is the value at c of the shifted tail
∑ₖ f_{n+1+k} X^k of f.
The coefficients of the quotient by X - C c are the explicit series
∑ₖ f_{n+1+k} c^k.
The value at c of the tail ∑ₖ f_{n+k} X^k of f is fₙ + c * (∑ₖ f_{n+1+k} X^k)(c).
Division by X - C c. At a point c where power series can be evaluated,
f = (X - C c) * q + C (f(c)) with q = divXSubC hc f.
A power series vanishing at c factors as f = (X - C c) * divXSubC hc f.
Divisibility by a linear factor is vanishing at its root. At a point c where power
series can be evaluated, a power series is divisible by X - C c exactly when its value at c is
zero; the quotient is PowerSeries.divXSubC hc f.