Evaluation of power series as infinite sums #
For a power series f = ∑ aₙ Xⁿ over a commutative ring R and an element b of an R-algebra
A with a topology, PowerSeries.evalAt f b is the infinite sum ∑ₙ aₙ • bⁿ, with the junk
value 0 when the sum does not converge. The algebra A need not be commutative: the scalars
aₙ act centrally, so the values of f at b commute with b.
Unlike Mathlib's PowerSeries.aeval, which evaluates every power series at a topologically
nilpotent point of a complete linearly topologized algebra, evalAt makes sense at every point;
it is meaningful for series whose coefficients decay fast enough, such as entire series over a
normed ring (TauCeti.RingTheory.PowerSeries.Entire.Eval). This file first records the values of
evalAt that need no convergence hypothesis. In an ultrametric normed algebra, ‖f(b)‖ is
bounded by the Gauss norm of f at every radius r ≥ ‖b‖ at which that Gauss norm is defined.
In any normed algebra, it is bounded by (‖1‖ + 1) * (1 - q)⁻¹ times that Gauss norm once
‖b‖ ≤ q * r with 0 ≤ q < 1. In a complete normed algebra, evaluation is additive and
multiplicative on series whose terms at the point are absolutely summable, such as entire series
or series on an open disc containing the point.
In a complete ultrametric normed algebra, a series restricted at a radius c can be evaluated at
every b with ‖b‖ ≤ c: the terms aₙ • bⁿ tend to zero, so they are summable, and the Cauchy
product formula makes evaluation at b a ring homomorphism on the restricted series. The algebra
need not be commutative, so this evaluates restricted series at bounded operators as well as at
points of complete normed field extensions.
A power series F = ∑ Fₙ Xⁿ whose coefficients lie in a ring A acted on by R, such as a series
of operators, is instead evaluated at a scalar a : R: PowerSeries.evalScalar F a is the
infinite sum ∑ₙ aⁿ • Fₙ.
Over a field 𝕜, the same sum is Mathlib's FormalMultilinearSeries.ofScalarsSum
(PowerSeries.evalAt_eq_ofScalarsSum); that construction needs a field of scalars, while the
coefficient rings here may have nilpotents.
Main definitions #
PowerSeries.evalAt: the value∑ₙ aₙ • bⁿof a power series atb.PowerSeries.evalScalar: the value∑ₙ aⁿ • Fₙof a power series at a scalara.
Main results #
PowerSeries.evalAt_coe: on polynomials,evalAtisPolynomial.aeval; in particularPowerSeries.evalAt_X_sub_C: the value ofX - aatbisb - a.PowerSeries.evalAt_hasseDeriv_coe: the value ataof a Hasse derivative of a polynomial is a coefficient of its Taylor expansion ata.PowerSeries.evalAt_hasseDeriv_X_sub_C_pow: the Hasse derivatives of(X - a) ^ mata.PowerSeries.evalAt_map_algebraMap: evaluation is compatible with extension of scalars.PowerSeries.evalAt_rescale: rescaling the variable rescales the point of evaluation.PowerSeries.commute_evalAt: the values of a series atbcommute withb.PowerSeries.norm_evalAt_le_gaussNorm: the Gauss-norm bound in an ultrametric algebra.PowerSeries.norm_evalAt_le_mul_gaussNorm_of_norm_algebraMap_le: a coefficient map bounded byCgives an evaluation bound byC, even without norm-one identity in the target;PowerSeries.norm_evalAt_le_gaussNorm_of_norm_algebraMap_leis the contractive case.PowerSeries.norm_evalAt_le_mul_gaussNorm: a Gauss-norm bound in any normed algebra.PowerSeries.evalAt_add_of_summable_norm,PowerSeries.evalAt_sum_of_summable_normandPowerSeries.evalAt_mul_of_summable_norm: in a complete normed algebra, evaluation preserves addition, finite sums and multiplication on series whose terms at the point are absolutely summable.PowerSeries.IsRestricted.hasSum_evalAt,PowerSeries.IsRestricted.evalAt_addandPowerSeries.IsRestricted.evalAt_mul: a series restricted atcconverges at everybwith‖b‖ ≤ cin a complete ultrametric algebra, additively and multiplicatively in the series;PowerSeries.IsRestricted.evalAt_smulandPowerSeries.IsRestricted.evalAt_sumrecord the compatibility with scalars and finite sums.PowerSeries.IsRestricted.evalAtHom: evaluation at suchbas a ring homomorphism on the restricted series.PowerSeries.evalAt_eq_zero_iff_of_isUnit_X_pow_mul_finprod_eq: zeros in the closed disc of a series factored asu * (X ^ a * ∏ᶠ m, g m)withua restricted unit.PowerSeries.evalScalar_monomial,PowerSeries.evalScalar_at_zero,PowerSeries.evalScalar_add: evaluation at a scalar of monomials, at the scalar0, and of sums.PowerSeries.commute_evalScalar: an element commuting with the coefficients of a series commutes with its value at a scalar.PowerSeries.norm_evalScalar_le: in an ultrametric ring, a uniform boundcon‖a‖ ^ n * ‖Fₙ‖bounds‖F(a)‖.
The value f(b) = ∑ₙ aₙ • bⁿ of the power series f = ∑ aₙ Xⁿ at an element b of a
topological R-algebra, defined as an infinite sum. It takes the junk value 0 when the sum does
not converge; for entire f over a normed ring it converges in every complete normed algebra
(PowerSeries.IsEntire.hasSum_evalAt).
Instances For
The value f(b) is the infinite sum ∑ₙ aₙ • bⁿ.
On polynomials, evaluation is Polynomial.aeval.
The value at a of a Hasse derivative of a polynomial is a coefficient of its Taylor
expansion at a.
The zero series evaluates to zero.
A constant series evaluates to its constant, mapped into the algebra.
The series 1 evaluates to 1.
The variable X evaluates to the point of evaluation.
The monomial a Xⁿ evaluates to a • bⁿ.
At the point 0, a power series evaluates to its constant coefficient.
Evaluation is compatible with extension of scalars: mapping the coefficients along
R → S does not change the value at a point of an S-algebra.
Rescaling the variable by a evaluates at the rescaled point: f(a X) at b is
f(a • b).
Over a field, evalAt is the sum FormalMultilinearSeries.ofScalarsSum of the scalar
series with the same coefficients.
The values of a series at b commute with b.
Evaluation commutes with negation.
The value of X - a at b is b - a.
The value F(a) = ∑ₙ aⁿ • Fₙ at a scalar a : R of a power series F = ∑ Fₙ Xⁿ whose
coefficients lie in a topological semiring A acted on by R, defined as an infinite sum. Unlike
PowerSeries.evalAt, the coefficients need not be scalars, so this evaluates series of operators
at scalars. It takes the junk value 0 when the sum does not converge; for entire F over a
complete normed ring it converges at every a (PowerSeries.IsEntire.hasSum_evalScalar).
Instances For
The value F(a) at a scalar is the infinite sum ∑ₙ aⁿ • Fₙ.
An element commuting with every coefficient of a series commutes with its value at a scalar.
The zero series evaluates to zero at every scalar.
The monomial c Xⁿ evaluates to aⁿ • c at the scalar a.
A constant series evaluates to its constant at every scalar.
The variable X evaluates to a • 1 at the scalar a.
The series 1 evaluates to 1 at every scalar.
Evaluation at a scalar is additive on series whose defining sums converge there.
At the scalar 0, a power series evaluates to its constant coefficient.
Evaluation at a scalar commutes with negation.
A coefficient map bounded by C gives the same bound for evaluation in an
ultrametric algebra, at every radius where the Gauss norm is defined and bounds the argument.
Neither a norm-one identity nor completeness nor a bounded scalar action is required.
For negative C the coefficient bound forces the series to be zero.
Contractive coefficient maps give a contractive evaluation estimate without requiring that the target algebra have norm-one identity. The target may be noncommutative.
In an ultrametric normed algebra with ‖1‖ = 1, the value of a series at a point b with
‖b‖ ≤ r is bounded by the Gauss norm of the series at the radius r, whenever the latter is
defined. This needs no convergence: the junk value 0 satisfies the bound too.
In any normed algebra, the value of a series at a point b with ‖b‖ ≤ q * r, where
0 ≤ q < 1, is bounded by (‖1‖ + 1) * (1 - q)⁻¹ times the Gauss norm of the series at the radius
r, whenever the latter is defined: the terms of the sum are dominated by a geometric series of
ratio q. This needs neither an ultrametric norm nor convergence: the junk value 0 satisfies the
bound too.
In an ultrametric normed ring, if c bounds ‖a‖ ^ n * ‖Fₙ‖ for every n, then it
bounds the value at the scalar a of the series F = ∑ Fₙ Xⁿ. This needs no convergence: the
junk value 0 satisfies the bound too.
If the weighted coefficient norms ‖aₙ‖ ‖b‖ⁿ of a series f = ∑ aₙ Xⁿ are summable, then so
are the norms of its terms aₙ • bⁿ at b, in any seminormed ring with a bounded scalar action.
In a complete seminormed algebra, if the terms aₙ • bⁿ of a series f = ∑ aₙ Xⁿ are
absolutely summable, then they sum to f(b).
Evaluation at b is additive on series whose terms at b are absolutely summable.
Evaluation commutes with finite sums of series whose terms at b are absolutely summable.
Evaluation at b is multiplicative on series whose terms at b are absolutely summable: this
is the Cauchy product formula for absolutely convergent series.
At a point b with ‖b‖ ≤ c, the terms aₙ • bⁿ of a series restricted at the radius c
tend to zero.
Evaluation of restricted series. In a complete ultrametric normed algebra, for a series
f = ∑ aₙ Xⁿ restricted at the radius c and a point b with ‖b‖ ≤ c, the series
∑ aₙ • bⁿ converges to f(b).
Evaluation at a point of norm at most c is additive on series restricted at c.
Evaluation at a point of norm at most c commutes with scalar multiplication of a series
restricted at c.
Evaluation at a point of norm at most c commutes with finite sums of series restricted
at c.
Evaluation at a point of norm at most c is multiplicative on series restricted at c: this
is the Cauchy product formula, which holds in a complete ultrametric ring as soon as the terms of
both series tend to zero.
Evaluation of restricted series at b as a ring homomorphism from the series restricted at
c to a complete ultrametric normed algebra, for a point b with ‖b‖ ≤ c.
Instances For
The evaluation homomorphism at b sends a restricted series f to f(b).
Suppose f = u * (X ^ a * ∏ᶠ m, g m) on the closed disc of radius r, where u is a unit of
the ring of series restricted at r and g is a finitely supported family of polynomials. Then in
any complete ultrametric normed domain A over R, for every x : A with ‖x‖ ≤ r,
f.evalAt x = 0 iff (x = 0 ∧ 0 < a) or x is a root of some factor g m
(m ∈ Function.mulSupport g).