The Mahler basis of continuous functions #
In this file we introduce the Mahler basis function mahler k, for k : ℕ, which is the unique
continuous map ℤ_[p] → ℚ_[p] agreeing with n ↦ n.choose k for n ∈ ℕ.
Using this, we prove Mahler's theorem, showing that for any any continuous function f on ℤ_[p]
(valued in a p-adic normed space E), the Mahler series x ↦ ∑' k, mahler k x • Δ^[n] f 0
converges (uniformly) to f, and this construction defines a Banach-space isomorphism between
C(ℤ_[p], E) and the space of sequences ℕ → E tending to 0.
For this, we follow the argument of Bojanić [Boj74].
The formalisation of Mahler's theorem presented here is based on code written by Giulio Caflisch for his bachelor's thesis at ETH Zürich.
References #
- R. Bojanić, A simple proof of Mahler's theorem on approximation of continuous functions of a p-adic variable by polynomials
- P. Colmez, Fonctions d'une variable p-adique
Tags #
Bojanic
The p-adic integers are a binomial ring, i.e. a ring where binomial coefficients make sense.
Equations
- One or more equations did not get rendered due to their size.
Bound for iterated forward differences of a continuous function from a compact space to a nonarchimedean seminormed group.
Explicit bound for the decay rate of the Mahler coefficients of a continuous function on ℤ_[p].
This will be used to prove Mahler's theorem.
Key lemma for Mahler's theorem: for f a continuous function on ℤ_[p], the sequence
n ↦ Δ^[n] f 0 tends to 0. See PadicInt.fwdDiff_iter_le_of_forall_le for an explicit
estimate of the decay rate.
A single term of a Mahler series, given by the product of the scalar-valued continuous map
mahler n : ℤ_[p] → ℚ_[p] with a constant vector in some normed ℚ_[p]-vector space.
Equations
- PadicInt.mahlerTerm a n = mahler n • ContinuousMap.const ℤ_[p] a
Instances For
A series of the form considered in Mahler's theorem.
Equations
- PadicInt.mahlerSeries a = ∑' (n : ℕ), PadicInt.mahlerTerm (a n) n
Instances For
A Mahler series whose coefficients tend to 0 is convergent.
Evaluation of a Mahler series is just the pointwise sum.
The value of a Mahler series at a natural number n is given by the finite sum of the first m
terms, for any n ≤ m.
The coefficients of a Mahler series can be recovered from the sum by taking forward differences at
0.
Mahler's theorem: for any continuous function f from ℤ_[p] to a p-adic Banach space, the
Mahler series with coeffients n ↦ Δ_[1]^[n] f 0 converges to the original function f.
The isometric equivalence from C(ℤ_[p], E) to the space of sequences in E tending to 0 given
by Mahler's theorem, for E a nonarchimedean ℚ_[p]-Banach space.
Equations
- One or more equations did not get rendered due to their size.