Restricted series with coefficients in a normed module #
Let E be a seminormed additive group and c : σ → ℝ a polyradius. A family of coefficients
a : (σ →₀ ℕ) → E is restricted at c when its weighted norms tend to zero,
‖a t‖ * ∏ i ∈ t.support, c i ^ t i → 0 along the cofinite filter on σ →₀ ℕ.
This is Mathlib's condition MvPowerSeries.IsRestricted with coefficients in a group rather than
a ring, and for E = R the two agree (MvPowerSeries.isRestrictedFamily_coeff_iff).
Restricted families are the coefficients of the module-valued restricted series ∑ₜ a t Xᵗ,
such as analytic functions on a closed polydisc with values in a Banach module.
The restricted families form an additive subgroup of the coefficient families, and an
R-submodule when E is a module over a seminormed ring R with ‖r • e‖ ≤ ‖r‖ * ‖e‖. This file
gives their coefficient maps and extensionality, the inclusion of finitely supported families,
the slices obtained by fixing exponents in one variable or a set of variables
(TauCeti.MvPowerSeries.IsRestrictedFamily.comp_optionElim and
TauCeti.MvPowerSeries.IsRestrictedFamily.comp_sumElim), and the maps induced
coefficientwise by bounded linear maps ‖φ e‖ ≤ C * ‖e‖. When E is
ultrametric, restricted series over R act on restricted families by convolution,
(f • a) t = ∑_{p + q = t} f_p • a_q,
making the restricted families a module over the ring of restricted series. The convolution
MvPowerSeries.convSMul and its module laws, which need no norm, are in
TauCeti.RingTheory.MvPowerSeries.Convolution.
The variables may be arbitrary, the coefficient ring need not be commutative, and no
completeness is assumed. Without variables, the restricted families are the module E itself
(TauCeti.MvPowerSeries.IsRestrictedFamily.isEmptyLinearEquiv); with E = R, they are the ring
of restricted series as a module over itself
(TauCeti.MvPowerSeries.IsRestrictedFamily.subringLinearEquiv).
Implementation notes #
The predicate and its closure properties adapt Mathlib's ring-valued
MvPowerSeries.IsRestricted to group-valued coefficients: the proofs of
TauCeti.MvPowerSeries.IsRestrictedFamily.of_norm_le and
TauCeti.MvPowerSeries.IsRestrictedFamily.add follow those of Mathlib's
MvPowerSeries.isRestricted_map and MvPowerSeries.IsRestricted.add. The proof that convolution
preserves restrictedness, TauCeti.MvPowerSeries.IsRestrictedFamily.convSMul, adapts Mathlib's
MvPowerSeries.tendsto_antidiagonal.
A family of coefficients a : (σ →₀ ℕ) → E in a seminormed group is restricted at the
polyradius c if ‖a t‖ * ∏ i ∈ t.support, c i ^ t i → 0 along the cofinite filter. These are
the coefficient families of restricted power series with coefficients in E.
Instances For
Restrictedness is decay of the weighted coefficient norms along the cofinite filter.
At unit polyradius, restricted families are exactly the null coefficient families.
For coefficients in a normed ring, a family is restricted exactly when the power series with these coefficients is restricted in Mathlib's sense.
Restrictedness only depends on the absolute values of the radii.
A family whose coefficient norms are bounded by a constant multiple of those of a restricted family is restricted.
Mapping the coefficients of a restricted family by a function bounded by a constant multiple of the norm gives a restricted family.
A family with finitely many nonzero coefficients is restricted at every polyradius.
A family with a single nonzero coefficient is restricted at every polyradius.
Scalar multiples of restricted families are restricted.
Fixing the exponent k of the variable none, the slice t ↦ a (t.optionElim k) of a
restricted family is restricted in the remaining variables. Only the radius of none needs to be
positive.
Fixing the exponents in one set of variables preserves restrictedness in the others. Only the radii of the fixed variables need to be positive.
At any polyradius, a family with coefficients in a finite product is restricted exactly when each coordinate family is restricted. The product has its maximum seminorm.
The restricted families at the polyradius c, as an additive subgroup of all coefficient
families.
Instances For
Two restricted families with the same coefficients are equal.
The restricted families at the polyradius c, as an R-submodule of all coefficient
families. Its underlying additive subgroup is
TauCeti.MvPowerSeries.IsRestrictedFamily.addSubgroup, which carries the resulting module
structure.
Instances For
The coefficient of a restricted family at the exponent t, as an R-linear map.
Instances For
The inclusion of the finitely supported coefficient families into the restricted families.
Instances For
The family with the single coefficient e at t is the image of Finsupp.single t e.
A bounded R-linear map φ : E → F, ‖φ e‖ ≤ C * ‖e‖, maps restricted families to
restricted families coefficientwise.
Instances For
A restricted family is killed by the induced map exactly when each coefficient is killed.
Uniformly bounded coefficient lifts give restricted lifts with the same coefficient bound. The polyradius can be arbitrary and the lift need not be linear.
Bounded lifts, rather than algebraic surjectivity alone, guarantee surjectivity on restricted families.
Without variables, a restricted family is determined by its constant coefficient, which can be arbitrary: the restricted families are the coefficient module itself.
Instances For
Over an ultrametric coefficient module, the convolution of a restricted series with a restricted family is restricted.
Restricted series act on restricted families by convolution.
The restricted families form a module over the ring of restricted series.
For coefficients in the ring itself, the restricted families are the ring of restricted series, regarded as a module over itself.
Instances For
The maps induced by bounded linear maps commute with the action of restricted series.
Over a commutative coefficient ring, the action of a constant series is scalar multiplication by its constant.