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 ∈ ℕ.

In future PR's, we will show that these functions give a Banach basis for the space of continuous maps ℤ_[p] → ℚ_[p].

References

• [P. Colmez, Fonctions d'une variable p-adique][colmez2010]

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 ℕ.

@[simp]

theorem 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.