The p-adic kit: multivariate evaluation #
Evaluation of a multivariate power series h ∈ O⟦z_s : s ∈ σ⟧ at a family of points of
the maximal ideal (ChabautyColeman.MvPSeries.eval), as a thin layer over Mathlib's
MvPowerSeries.eval₂, in the standing setting of the p-adic kit (Chabauty.Series.PSeries).
For a finite index type, any family in the maximal ideal is a legitimate evaluation
point (ChabautyColeman.MvPSeries.hasEval_of_mem); evaluation is a ring homomorphism
(ChabautyColeman.MvPSeries.evalRingHom) computed by a convergent sum
(ChabautyColeman.MvPSeries.hasSum_eval).
Composition: Mathlib's formal substitution MvPowerSeries.subst is continuous for the
product topologies (MvPowerSeries.continuous_subst' — each coefficient of
subst a f is a fixed finite linear combination of coefficients of f, by
MvPowerSeries.coeff_subst_finite applied to the all-ones series), whence evaluation of
a substitution is evaluation at the evaluated family
(ChabautyColeman.MvPSeries.eval_subst, via uniqueness of continuous algebra
homomorphisms MvPowerSeries.aeval_unique), and the evaluated family is itself a
legitimate evaluation point (ChabautyColeman.MvPSeries.hasEval_eval).
The chain rule mentioned in the blueprint node is deferred to the formal-group-law
items, which set up formal (partial) derivatives; Mathlib currently has none for
MvPowerSeries.
For power series whose coefficients decay (tend to 0 cofinitely), evaluation
converges at any family of points of O — not only those in the maximal ideal —
because the terms tend to 0 for a bounded point family; this is
ChabautyColeman.MvPSeries.evalT, agreeing with eval where the latter converges
(ChabautyColeman.MvPSeries.evalT_eq_eval).
Blueprint nodes: def:mv-eval, def:mv-evalT.
On ι →₀ ℕ with ι finite, the total degree tends to ∞ along the cofinite
filter: only finitely many multi-indices have degree below any bound.
Evaluation of a multivariate power series at a family of points of the maximal
ideal: the convergent sum ∑ a_d z₀^d (junk if the series does not converge).
Equations
- ChabautyColeman.MvPSeries.eval z₀ h = MvPowerSeries.eval₂ (RingHom.id O) z₀ h
Instances For
Evaluation of a multivariate power series with decaying coefficients at an arbitrary
family of points of O (junk if the defining series does not converge). Unlike
MvPSeries.eval, the evaluation points need not lie in the maximal ideal; convergence is
supplied instead by the decay of the coefficients.
Equations
Instances For
The constant power series 1 has decaying coefficients.
Coefficient decay is preserved by renaming the variables along an injection.
Families of points of the maximal ideal, indexed by a finite type, are legitimate evaluation points for multivariate power series.
A sufficient condition for the coefficients of a multivariate power series to decay
(hence for evalT to converge): each coefficient lies in a power of the maximal ideal
whose exponent tends to ∞ cofinitely.
The defining series of evalT is summable when the coefficients of h decay.
evalT is additive on power series with decaying coefficients.
The product of two coefficient-decaying power series again has decaying coefficients (the coefficients are the Cauchy convolution of two null sequences).
evalT is multiplicative on power series with decaying coefficients: the Cauchy product
of the two convergent value series.
A product ∏ᵢ (b i)^{mᵢ} of coefficient-decaying series has decaying coefficients.
evalT is multiplicative on products of powers of decaying series: it evaluates
∏ᵢ (b i)^{mᵢ} at the family of values evalT z (b i).
evalT composes with substitution: evaluating a formal substitution at z is
evaluating the outer series at the family of values of the inner series. Both g and each
a s must have decaying coefficients.
The defining series of MvPSeries.eval converges.
On a legitimate (point-nilpotent) evaluation point, evalT agrees with eval.
Evaluation at a legitimate point, as a ring homomorphism.
Equations
Instances For
The value of a multivariate power series at a point of the maximal ideal is congruent to its constant coefficient modulo the maximal ideal.
Values of a power series with constant coefficient in the maximal ideal lie in the maximal ideal.
The values of a continuous algebra homomorphism of power series rings at the variables form a legitimate evaluation point.
Evaluation along a continuous algebra homomorphism of power series rings is evaluation at the images of the variables (by uniqueness of continuous algebra homomorphisms).
The family of values of a substitutable family is a legitimate evaluation point.
Evaluation of a (formal) substitution is evaluation at the evaluated family.