The van der Put basis of continuous functions on ℤ_p #
For n : ℕ let ℓ(n) = (p.digits n).length be the number of base-p digits of n, so that
ℓ(0) = 0 and p ^ (ℓ(n) - 1) ≤ n < p ^ ℓ(n) for n > 0. The n-th van der Put function is
the indicator of the ball n + p ^ ℓ(n) ℤ_p, that is of the x whose truncation modulo
p ^ ℓ(n) is n; for n = 0 this is the constant function 1. Deleting the leading digit of
n > 0 gives n⁻ = n % p ^ (ℓ(n) - 1), and the n-th van der Put coefficient of a function
f on ℤ_p is f 0 for n = 0 and f n - f n⁻ for n > 0.
Van der Put's theorem says that for an ultrametric normed group E, a continuous
f : ℤ_[p] → E is the uniformly convergent sum of its van der Put terms, its coefficients tend to
zero, and its sup norm is the sup norm of its coefficients. If E is also complete, conversely
every null sequence of coefficients defines a continuous function. Together, the coefficients then
give an isometric isomorphism C(ℤ_[p], E) ≃ₗᵢ C₀(ℕ, E), linear over any scalars acting
continuously on E.
Unlike Mahler's theorem (PadicInt.mahlerEquiv), this needs no ℤ_[p]-module structure on E,
and its basis functions are locally constant. The proof rests on the telescoping identity
∑_{n < p ^ k} e_n(x) a_n(f) = f (x mod p ^ k) (PadicInt.sum_vanDerPutTerm_vanDerPutCoeff_apply)
and on the biorthogonality of terms and coefficients (PadicInt.vanDerPutCoeff_vanDerPutTerm).
Main definitions #
PadicInt.vanDerPutTerm a n: the function equal toaonn + p ^ ℓ(n) ℤ_pand to0off it.PadicInt.vanDerPutCoeff f n: then-th van der Put coefficient off : ℤ_[p] → E.PadicInt.vanDerPutSeries a: the sum of the van der Put terms with coefficientsa.PadicInt.vanDerPutEquiv S E: the isometric isomorphismC(ℤ_[p], E) ≃ₗᵢ[S] C₀(ℕ, E).
Main results #
PadicInt.sum_vanDerPutTerm_vanDerPutCoeff_apply: the partial sums overn < p ^ kof the van der Put expansion of any function evaluate it at the truncations modulop ^ k.PadicInt.vanDerPutCoeff_vanDerPutTerm: the coefficients of a single term.PadicInt.tendsto_vanDerPutCoeff,PadicInt.norm_vanDerPutCoeff_le: the coefficients of a continuous function tend to zero and are bounded by its sup norm.PadicInt.hasSum_vanDerPut: van der Put's theorem, the expansion of a continuous function.PadicInt.vanDerPutCoeff_id: the coefficients of the identity ofℤ_[p]are the leading digit partsn - n⁻.
References #
- P. Colmez, Fonctions d'une variable p-adique, Astérisque 330 (2010), 13–59.
- W. H. Schikhof, Ultrametric Calculus, Cambridge University Press, 1984, §62.
The definitions and the proof of the isometry are modelled on Mathlib's treatment of the Mahler
basis in Mathlib.NumberTheory.Padics.MahlerBasis (PadicInt.mahlerTerm, PadicInt.mahlerSeries
and PadicInt.mahlerEquiv).
The n-th van der Put term with value a: the locally constant function on ℤ_[p] equal to
a at the x whose truncation modulo p ^ ℓ is n, and to 0 elsewhere, where
ℓ = (p.digits n).length is the number of base-p digits of n. These x form the ball
n + p ^ ℓ ℤ_[p] (PadicInt.vanDerPutTerm_apply_eq_ite_norm_sub_le); for n = 0 it is all of
ℤ_[p].
Instances For
The n-th van der Put term is supported on the closed ball of radius p ^ (-ℓ) around n,
ℓ the number of base-p digits of n.
The 0-th van der Put term is constant.
The van der Put term with value 0 vanishes.
The n-th van der Put term takes the value a at n.
The van der Put term is additive in its value.
The van der Put term commutes with negation of its value.
The van der Put term commutes with scalar multiplication of its value.
The n-th van der Put coefficient of a function f on ℤ_[p]: f 0 for n = 0, and
f n - f n⁻ for n > 0, where n⁻ = n % p ^ Nat.log p n is n with its leading base-p digit
deleted.
Instances For
The van der Put coefficients are additive in the function.
The van der Put coefficients commute with negation of the function.
The van der Put coefficients commute with subtraction of functions.
The telescoping identity. For any function f on ℤ_[p], the partial sum over n < p ^ k
of its van der Put expansion at x is the value of f at the truncation of x modulo p ^ k.
Biorthogonality: the van der Put coefficients of the m-th van der Put term with value a
are a at m and 0 elsewhere.
The sup norm of a van der Put term is the norm of its value.
The van der Put coefficients of a continuous function tend to zero: n and n⁻ are
congruent modulo p ^ Nat.log p n, and f is uniformly continuous.
Over an ultrametric group, the van der Put coefficients of a continuous function are bounded by its sup norm.
Van der Put's theorem: a continuous function on ℤ_[p] with values in an ultrametric
normed group is the uniformly convergent sum of its van der Put terms, without assuming
completeness.
A continuous function is the van der Put series of its van der Put coefficients.
A van der Put series whose coefficients tend to zero converges uniformly.
A convergent van der Put series is evaluated pointwise.
The van der Put coefficients of a convergent van der Put series are its coefficients.
Van der Put's theorem, as an isometric isomorphism between the continuous functions on
ℤ_[p] with values in a complete ultrametric normed group E and the null sequences in E,
sending a function to its van der Put coefficients. It is linear over any scalars S acting
continuously on E.
Instances For
The coordinates of vanDerPutEquiv S E f are the van der Put coefficients of f.
The inverse of vanDerPutEquiv S E sums the van der Put series.
The van der Put series of the coordinate vector single n a is the van der Put term
vanDerPutTerm a n.