Amice's polynomials on the discs of level h #
For h, n : ℕ put m_h(n) = ⌊n / pʰ⌋!. Amice's basis of the analytic stage LA_h consists of
the polynomials
e_{h,n}(x) = m_h(n) (x choose n).
On the disc a + pʰℤ_p, in the coordinate w = (x - a) / pʰ, the polynomial e_{h,n} is a
polynomial in w. Its coefficients lie in ℤ_p
(TauCeti.exists_natDegree_le_and_eval_eq_factorial_mul_choose). This is stronger than
e_{h,n} taking integral values, which already holds for x choose n, and it needs the factor
m_h(n): the coefficient of w in (pʰ w choose n) is (-1) ^ (n - 1) pʰ / n, which is
± p⁻¹ for n = p ^ (h + 1). The proof factors
n! (a + pʰ w choose n) = ∏_{i < n} (a - i + pʰ w). The factor of index i is divisible by
p ^ min(v_p(a - i), h), and among n consecutive elements of ℤ_p at least ⌊n / pᵏ⌋ are
divisible by pᵏ, so the product is divisible by p ^ (∑_{k = 1}^{h} ⌊n / pᵏ⌋). By Legendre's
formula this exponent is v_p(n!) - v_p(m_h(n)).
Hence e_{h,n} has an expansion in LA_h(ℤ_p), and more generally e_{h,n} • e has one in
LA_h(E) for every normed ℤ_p-module E, of norm at most ‖e‖ when the action is
contractive. For complete ultrametric E, summing these vectors gives a continuous linear map
TauCeti.AnalyticStage.amiceMap : C₀(ℕ, E) → LA_h(E), (cₙ) ↦ ∑ₙ e_{h,n} • cₙ,
which does not increase norms. Followed by evaluation, it is the Mahler series with
coefficients m_h(n) • cₙ (TauCeti.AnalyticStage.eval_amiceMap). Amice's theorem, that
amiceMap is an isometric isomorphism, is TauCeti.AnalyticStage.amiceEquiv in
TauCeti.NumberTheory.Padics.Distribution.Amice.Isometry.
Its arithmetic input is the reduction of Amice's polynomials modulo p. Write n = pʰ q + r
with r < pʰ, and let a be a natural number. In ∏_{i < n} (a - i + pʰ w), the factors with
i ≡ a mod pʰ are pʰ times a monic linear polynomial, and each other factor is a - i times a
polynomial congruent to 1 modulo p. Hence Amice's polynomial on the disc of a is c F, where
F is congruent modulo p to a monic polynomial of degree #{i < n | i ≡ a mod pʰ}, which is
q or q + 1, and, by Legendre's formula, v_p(c) is the number of k ∈ [1, h] with
a mod pᵏ < n mod pᵏ. Consequently, modulo p, the expansion of e_{h,n} has degree at most
q on every disc, vanishes on the discs with a mod pʰ < r, and has a unit coefficient of w^q
on the disc of r. Ordering the coordinates (a, j) of LA_h by j and then by decreasing a,
and matching n with the coordinate (r, q), the matrix of amiceMap is thus congruent modulo
p to an upper triangular matrix with unit diagonal.
Main definitions #
TauCeti.amicePolynomial p h n a: the polynomialw ↦ m_h(n) (a + pʰ w choose n)overℤ_p.TauCeti.AnalyticStage.amiceTerm p h n e: the expansion ofe_{h,n} • einLA_h(E).TauCeti.AnalyticStage.amiceMap p h S: the mapC₀(ℕ, E) →L[S] LA_h(E),c ↦ ∑ₙ e_{h,n} • cₙ.
Main results #
TauCeti.exists_natDegree_le_and_eval_eq_factorial_mul_choose: Amice's polynomials have integral coefficients on every disc.TauCeti.eval_amicePolynomial,TauCeti.eq_amicePolynomial_of_eval:amicePolynomialis the unique polynomial with these values.TauCeti.AnalyticStage.eval_amiceTerm:amiceTermevaluates to the Mahler term ofm_h(n) • e.TauCeti.norm_coeff_amicePolynomial_lt_one_of_div_lt: modulop, Amice's polynomial on every disc has degree at most⌊n / pʰ⌋.TauCeti.norm_coeff_amicePolynomial_lt_one_of_mod_lt: modulop, it vanishes on the disc ofawhena mod pʰ < n mod pʰ.TauCeti.norm_coeff_amicePolynomial_div_of_mod_le: the norm of its coefficient ofw ^ ⌊n / pʰ⌋on the other discs.TauCeti.norm_coeff_amicePolynomial_mod_div: that coefficient is a unit on the disc ofn mod pʰ.TauCeti.AnalyticStage.norm_amiceMap_le,TauCeti.AnalyticStage.eval_amiceMap.
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.
Integrality of the disc coefficients #
Integrality of Amice's polynomials on discs. For every centre a ∈ ℤ_p, the polynomial
w ↦ ⌊n / pʰ⌋! (a + pʰ w choose n) has coefficients in ℤ_p: it is the evaluation of a
polynomial over ℤ_p of degree at most n.
Amice's polynomial on the disc of centre a. The polynomial over ℤ_p whose value at
w is ⌊n / pʰ⌋! (a + pʰ w choose n): the expansion of Amice's basis polynomial
e_{h,n}(x) = ⌊n / pʰ⌋! (x choose n) in the coordinate w = (x - a) / pʰ of the disc
a + pʰℤ_p.
Instances For
The value of Amice's polynomial on the disc of centre a at w is
⌊n / pʰ⌋! (a + pʰ w choose n).
amicePolynomial p h n a is the only polynomial with values ⌊n / pʰ⌋! (a + pʰ w choose n).
The disc expansion of Amice's polynomial: ∑_{k ≤ n} cₖ wᵏ = ⌊n / pʰ⌋! (a + pʰ w choose n),
where cₖ are the coefficients of amicePolynomial p h n a.
Reduction modulo p #
Amice's polynomials modulo p: vanishing on earlier discs. If a mod pʰ < n mod pʰ,
every coefficient of ⌊n / pʰ⌋! (a + pʰ w choose n) as a polynomial in w lies in pℤ_p.
Amice's polynomials modulo p: degree bound. On every disc a + pʰℤ_p, the coefficients
of wʲ in ⌊n / pʰ⌋! (a + pʰ w choose n) with j > ⌊n / pʰ⌋ lie in pℤ_p: modulo p, Amice's
polynomial has degree at most ⌊n / pʰ⌋.
Amice's polynomials modulo p: the coefficient of w ^ ⌊n / pʰ⌋. If
n mod pʰ ≤ a mod pʰ, the coefficient of w ^ ⌊n / pʰ⌋ in ⌊n / pʰ⌋! (a + pʰ w choose n) has
norm ‖p‖ ^ e, where e is the number of k ∈ [1, h] with a mod pᵏ < n mod pᵏ.
Amice's polynomials modulo p: the diagonal coefficient. On the disc of n mod pʰ, the
coefficient of w ^ ⌊n / pʰ⌋ in ⌊n / pʰ⌋! (n mod pʰ + pʰ w choose n) is a unit of ℤ_p.
Amice's vectors in the analytic stages #
Amice's vector e_{h,n} • e in LA_h(E): on the disc of a ∈ ZMod (pʰ) its coefficient
of wᵏ is the k-th coefficient of amicePolynomial p h n a.val, times e.
Instances For
Amice's vector e_{h,n} • e commutes with scalars acting on E compatibly with ℤ_p.
Amice's vectors have norm at most ‖e‖: their coefficients are integral multiples of e.
Amice's vector e_{h,n} • e evaluates to the Mahler term x ↦ (x choose n) • ⌊n / pʰ⌋! • e.
Amice's map C₀(ℕ, E) → LA_h(E), (cₙ) ↦ ∑ₙ e_{h,n} • cₙ, sending a null sequence to
the expansion on the discs of level h of the series of Amice's polynomials
e_{h,n}(x) = ⌊n / pʰ⌋! (x choose n) with coefficients cₙ.
Instances For
Amice's map is the sum of Amice's vectors e_{h,n} • cₙ.
The coordinates of Amice's map: on the disc of a, the coefficient of wᵏ in amiceMap c is
the sum over n of the k-th coefficient of amicePolynomial p h n a.val, times cₙ.
The coefficient of wᵏ on the disc of a in amiceMap c.
Amice's map sends the coordinate vector single n e to Amice's vector e_{h,n} • e.
Amice's map does not increase norms.
Amice's map followed by evaluation is the Mahler series x ↦ ∑ₙ (x choose n) • ⌊n / pʰ⌋! • cₙ.