Analytic stages on ℤ_p and their evaluation #
For h : ℕ, the residue classes a ∈ ZMod (p ^ h) cut ℤ_p into the discs a + pʰℤ_p, where
a is represented by its natural representative a.val < pʰ. On the disc of a the coordinate
w = (x - a) / pʰ runs through ℤ_p, and a function analytic on each of these discs is a family
of power series ∑ₙ c(a, n) wⁿ whose coefficients tend to zero. With coefficients in a complete
ultrametric normed ℤ_p-module E, these coefficient families make up the analytic stage
LA_h(E) = C₀(ZMod (pʰ) × ℕ, E),
normed by the largest coefficient (the maximum of the Gauss norms on the discs). Its elements are
coefficient vectors, kept distinct from the functions they define: evaluation need not be
injective when E has p-torsion. If multiplication by p on E is injective, evaluation
is injective: values at powers of p in each normalized disc coordinate determine all
coefficients by cancellation and a vanishing tail estimate.
Evaluation TauCeti.AnalyticStage.eval sends a coefficient vector to the continuous function
x ↦ ∑ₙ wⁿ • c(a, n). It is linear over every scalar ring acting on E compatibly with ℤ_p,
and does not increase norms.
Passing from level h to level h + 1 subdivides each disc a + pʰℤ_p into the p discs of the
classes a' = a + pʰ b, 0 ≤ b < p, in ZMod (p ^ (h + 1)). On the smaller disc
w = b + p v, so re-expanding in v gives the coefficients
d(a', j) = ∑_{k ≥ j} (k choose j) b^(k - j) pʲ • c(a, k).
The transition TauCeti.AnalyticStage.transition is this re-expansion. It does not increase norms
and it is compatible with evaluation. Composing these adjacent transitions gives
transitionLE S hhk : LA_h(E) →L[S] LA_k(E) for every h ≤ k. These maps form a directed
system, do not increase norms, and preserve evaluation. No injectivity assumption is needed.
When multiplication by p on E is injective, every transition is injective: reading the
coefficients on the subdisc with the same centre recovers p^j times the original coefficient.
The disc decomposition itself is the homeomorphism PadicInt.discHomeomorph of
TauCeti.NumberTheory.Padics.Disc, which sends (a, w) to a.val + pʰ w.
Main definitions #
TauCeti.AnalyticStage p h E: the analytic stageC₀(ZMod (pʰ) × ℕ, E).TauCeti.AnalyticStage.eval S: evaluationLA_h(E) →L[S] C(ℤ_p, E).TauCeti.AnalyticStage.transition S: the re-expansionLA_h(E) →L[S] LA_{h+1}(E).TauCeti.AnalyticStage.transitionLE S hhk: re-expansion from levelhto levelkforh ≤ k.
Main results #
TauCeti.AnalyticStage.eval_natCast_val_add_mul: on the disc ofa, the evaluation ofcis∑ₙ wⁿ • c(a, n).TauCeti.AnalyticStage.norm_eval_le,TauCeti.AnalyticStage.opNorm_eval_le_one: evaluation does not increase norms.TauCeti.AnalyticStage.eval_injective: evaluation is injective when multiplication bypon the coefficient module is injective.TauCeti.AnalyticStage.transition_apply: the re-expansion formula for the transition.TauCeti.AnalyticStage.norm_transition_apply_le: the coefficient ofvʲafter the transition has norm at most‖p‖ʲ ‖c‖.TauCeti.AnalyticStage.transition_apply_cast: the same-centre coefficients recoverp^jtimes the original coefficients.TauCeti.AnalyticStage.transition_injective: the transition is injective when multiplication bypon the coefficients is injective.TauCeti.AnalyticStage.norm_transition_le: the transition does not increase norms.TauCeti.AnalyticStage.eval_transition,TauCeti.AnalyticStage.eval_comp_transition: the transition is compatible with evaluation.TauCeti.AnalyticStage.transitionLE_comp: re-expansion through an intermediate level is re-expansion to the final level.TauCeti.AnalyticStage.norm_transitionLE_le,TauCeti.AnalyticStage.opNorm_transitionLE_le_one: every multi-level transition decreases norms.TauCeti.AnalyticStage.eval_transitionLE,TauCeti.AnalyticStage.eval_comp_transitionLE: every multi-level transition preserves evaluation.TauCeti.AnalyticStage.transitionLE_injective: multi-level transitions are injective under the same scalar-regularity hypothesis.
References #
- Y. Amice, Interpolation p-adique, Bull. Soc. Math. France 92 (1964), 117–180.
- P. Colmez, Fonctions d'une variable p-adique, Astérisque 330 (2010), §I.4.
Analytic stages #
The analytic stage LA_h(E) = C₀(ZMod (pʰ) × ℕ, E) of level h: the coefficient vectors
c(a, n) of families of power series ∑ₙ c(a, n) wⁿ, one on each disc a + pʰℤ_p, in the
coordinate w = (x - a.val) / pʰ. Its norm is the largest coefficient norm.
Instances For
Evaluation of the analytic stage LA_h(E): the coefficient vector c defines the continuous
function equal to ∑ₙ wⁿ • c(a, n) on the disc a + pʰℤ_p, where w = (x - a.val) / pʰ. It is
linear over every scalar ring S acting on E compatibly with ℤ_p.
Instances For
The value of the evaluation at x is the power series of the disc of x at the disc
coordinate of x.
The evaluation of c at x is the sum of the power series of the disc of x at the disc
coordinate of x.
On the disc a + pʰℤ_p, the evaluation of c is the power series ∑ₙ wⁿ • c(a, n) in the
disc coordinate w.
On the disc of a, the evaluation of c at a.val + pʰ w is ∑' n, wⁿ • c(a, n).
Evaluation does not increase norms.
Evaluation has operator norm at most 1.
Analytic-stage evaluation is injective if multiplication by p on the coefficient module
is injective. The coefficient module need not carry a field structure or an isometric scalar
action.
Raising the level #
The transition LA_h(E) → LA_{h+1}(E). The disc of a ∈ ZMod (pʰ) is the union of the discs
of the classes a' = a + pʰ b, 0 ≤ b < p, in ZMod (p ^ (h + 1)), where b = ⌊a'.val / pʰ⌋.
On the disc of a' the coordinates are related by w = b + p v, and the transition re-expands
∑ₖ c(a, k) wᵏ in powers of v:
d(a', j) = ∑ₖ (k choose j) b^(k - j) pʲ • c(a, k).
Instances For
The re-expansion formula for the transition.
On the subdisc with the same natural centre, re-expansion multiplies the degree-j
coefficient by p^j.
Raising the level is injective if multiplication by p on the coefficient module is
injective.
The coefficient of vʲ after the transition has norm at most ‖p‖ʲ ‖c‖.
The transition does not increase norms.
The transition is compatible with evaluation: a coefficient vector and its re-expansion on the smaller discs define the same function.
Evaluation after the transition is evaluation, as an identity of continuous linear maps.
Re-expansion from level h to level k, obtained by composing adjacent transitions.
Instances For
Re-expansion from a level to itself is the identity.
Re-expansion to the next target level appends one adjacent transition.
Re-expansion to the adjacent level is the original transition.
Appending an adjacent transition is re-expansion to the next target level.
Applying an adjacent transition after re-expansion raises the target level by one.
Re-expansion through an intermediate level equals the transition to the final level.
Applying two successive transitions is the transition across the combined levels.
Re-expansion after an adjacent transition starts one level earlier.
Applying re-expansion after an adjacent transition starts one level earlier.
Two adjacent transitions compose to re-expansion across two levels.
Two adjacent transitions re-expand a coefficient vector across two levels.
Analytic-stage transitions form a directed system of coefficient vectors.
Re-expansion between any two analytic levels does not increase the Gauss norm.
Re-expansion between any two analytic levels has operator norm at most 1.
Re-expansion between any two analytic levels preserves the evaluated function.
Evaluation after re-expansion between two levels is evaluation, as an identity of continuous linear maps.
Re-expansion between any two levels is injective if multiplication by p on the
coefficient module is injective.