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 normed ℤ_[p]-module 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ć [bojanic74].

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][bojanic74]
• [P. Colmez, Fonctions d'une variable p-adique][colmez2010]

Tags

Bojanic

theorem PadicInt.norm_ascPochhammer_le {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ) (x : ℤ_[p]) : ‖Polynomial.eval x (ascPochhammer ℤ_[p] k)‖ ≤ ‖↑k.factorial‖

Bound for norms of ascending Pochhammer symbols.

noncomputable instance PadicInt.instBinomialRing {p : ℕ} [hp : Fact (Nat.Prime p)] : BinomialRing ℤ_[p]

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.

theorem PadicInt.continuous_multichoose {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ) : Continuous fun (x : ℤ_[p]) => Ring.multichoose x k

theorem PadicInt.continuous_choose {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ) : Continuous fun (x : ℤ_[p]) => Ring.choose x k

noncomputable def mahler {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ) : C(ℤ_[p], ℤ_[p])

The k-th Mahler basis function, i.e. the unique continuous function ℤ_[p] → ℤ_[p] agreeing with n ↦ n.choose k for n ∈ ℕ. See [colmez2010], §1.2.1.

Equations

• mahler k = { toFun := fun (x : ℤ_[p]) => Ring.choose x k, continuous_toFun := ⋯ }

theorem mahler_apply {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ) (x : ℤ_[p]) : (mahler k) x = Ring.choose x k

theorem mahler_natCast_eq {p : ℕ} [hp : Fact (Nat.Prime p)] (k n : ℕ) : (mahler k) ↑n = ↑(n.choose k)

The function mahler k extends n ↦ n.choose k on ℕ.

theorem IsUltrametricDist.norm_fwdDiff_iter_apply_le {M : Type u_1} {G : Type u_2} [TopologicalSpace M] [CompactSpace M] [AddCommMonoid M] [SeminormedAddCommGroup G] [IsUltrametricDist G] (h : M) (f : C(M, G)) (m : M) (n : ℕ) : ‖(fwdDiff h)^[n] (⇑f) m‖ ≤ ‖f‖

Bound for iterated forward differences of a continuous function from a compact space to a nonarchimedean seminormed group.

theorem PadicInt.fwdDiff_iter_le_of_forall_le {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] {f : C(ℤ_[p], E)} {s t : ℕ} (hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s) (n : ℕ) : ‖(fwdDiff 1)^[n + s * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s

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.

theorem PadicInt.fwdDiff_tendsto_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] (f : C(ℤ_[p], E)) : Filter.Tendsto (fun (x : ℕ) => (fwdDiff 1)^[x] (⇑f) 0) Filter.atTop (nhds 0)

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.

noncomputable def PadicInt.mahlerTerm {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] (a : E) (n : ℕ) : C(ℤ_[p], E)

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]-module.

Equations

• PadicInt.mahlerTerm a n = mahler n • ContinuousMap.const ℤ_[p] a

theorem PadicInt.mahlerTerm_apply {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] (a : E) (n : ℕ) (x : ℤ_[p]) : (mahlerTerm a n) x = (mahler n) x • a

@[simp]

theorem PadicInt.norm_mahlerTerm {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] (a : E) (n : ℕ) : ‖mahlerTerm a n‖ = ‖a‖

@[simp]

theorem PadicInt.mahlerTerm_one {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : mahlerTerm 1 n = mahler n

@[simp]

theorem PadicInt.norm_mahler_eq {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ) : ‖mahler k‖ = 1

The uniform norm of the k-th Mahler basis function is 1, for every k.

noncomputable def PadicInt.mahlerSeries {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] (a : ℕ → E) : C(ℤ_[p], E)

A series of the form considered in Mahler's theorem.

Equations

• PadicInt.mahlerSeries a = ∑' (n : ℕ), PadicInt.mahlerTerm (a n) n

theorem PadicInt.hasSum_mahlerSeries {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] {a : ℕ → E} (ha : Filter.Tendsto a Filter.atTop (nhds 0)) : HasSum (fun (n : ℕ) => mahlerTerm (a n) n) (mahlerSeries a)

A Mahler series whose coefficients tend to 0 is convergent.

theorem PadicInt.mahlerSeries_apply {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] {a : ℕ → E} (ha : Filter.Tendsto a Filter.atTop (nhds 0)) (x : ℤ_[p]) : (mahlerSeries a) x = ∑' (n : ℕ), (mahler n) x • a n

Evaluation of a Mahler series is just the pointwise sum.

theorem PadicInt.mahlerSeries_apply_nat {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] {a : ℕ → E} (ha : Filter.Tendsto a Filter.atTop (nhds 0)) {m n : ℕ} (hmn : m ≤ n) : (mahlerSeries a) ↑m = ∑ i ∈ Finset.range (n + 1), m.choose i • a i

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.

theorem PadicInt.fwdDiff_mahlerSeries {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] {a : ℕ → E} (ha : Filter.Tendsto a Filter.atTop (nhds 0)) (n : ℕ) : (fwdDiff 1)^[n] (⇑(mahlerSeries a)) 0 = a n

The coefficients of a Mahler series can be recovered from the sum by taking forward differences at 0.

theorem PadicInt.hasSum_mahler {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (f : C(ℤ_[p], E)) : HasSum (fun (n : ℕ) => mahlerTerm ((fwdDiff 1)^[n] (⇑f) 0) n) f

Mahler's theorem: for any continuous function f from ℤ_[p] to a p-adic Banach space, the Mahler series with coefficients n ↦ Δ_[1]^[n] f 0 converges to the original function f.

noncomputable def PadicInt.mahlerEquiv {p : ℕ} [hp : Fact (Nat.Prime p)] (E : Type u_1) [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] : C(ℤ_[p], E) ≃ₗᵢ[ℤ_[p]] ZeroAtInftyContinuousMap ℕ E

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.

theorem PadicInt.mahlerEquiv_apply {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (f : C(ℤ_[p], E)) : ⇑((mahlerEquiv E) f) = fun (n : ℕ) => (fwdDiff 1)^[n] (⇑f) 0

theorem PadicInt.mahlerEquiv_symm_apply {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (a : ZeroAtInftyContinuousMap ℕ E) : (mahlerEquiv E).symm a = mahlerSeries ⇑a