The Mahler basis on the p-adic integers

This file records identities for Mathlib's Mahler basis functions on ℤ_p and for Mathlib's Mahler isometry PadicInt.mahlerEquiv E : C(ℤ_[p], E) ≃ₗᵢ[ℤ_[p]] C₀(ℕ, E), which sends a continuous function to its sequence of Mahler coefficients Δ^n f (0).

Mathlib states Mahler's theorem as a ℤ_[p]-linear isometry. Since the forward differences commute with every scalar action on the coefficient module, the isometry is linear over any additional scalars S acting on E; this scalar-linear refinement is PadicInt.mahlerLinearIsometryEquiv S E. It is what turns Mahler's theorem into a statement about S-linear functionals, for instance measures with values in a ℤ_[p]-algebra S = E.

Main results

• TauCeti.id_mul_mahler: multiplication by the coordinate function satisfies x * mahler n = (n + 1) • mahler (n + 1) + n • mahler n.
• TauCeti.factorial_smul_mahler: n ! • mahler n is the descending Pochhammer polynomial x (x - 1) ⋯ (x - n + 1).
• PadicInt.mahlerEquiv_smul: the Mahler coefficients commute with scalar actions.
• PadicInt.mahlerLinearIsometryEquiv: Mahler's isometry as an S-linear isometric equivalence.
• PadicInt.mahlerEquiv_symm_single: the Mahler series of a coordinate vector single n a is the Mahler term x ↦ (x choose n) • a.
• PadicInt.mahlerTerm_eq_smul: over a normed ring with a ℤ_[p]-action commuting with left multiplication, the Mahler term with coefficient a is a times mahler n • 1.
• PadicInt.mahler_natCast_mul: for m : ℕ, the Mahler function (m x choose n) is the integral combination of the (x choose k), k ≤ n, with coefficients those of ((1 + T) ^ m - 1) ^ k at T ^ n.

theorem TauCeti.id_mul_mahler {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) : ContinuousMap.id ℤ_[p] * mahler n = (n + 1) • mahler (n + 1) + n • mahler n

The Mahler recurrence x * (x choose n) = (n + 1) * (x choose (n + 1)) + n * (x choose n).

theorem TauCeti.factorial_smul_mahler {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) : n.factorial • mahler n = (descPochhammer ℤ_[p] n).toContinuousMap

n ! times the Mahler function x choose n is the descending Pochhammer polynomial x (x - 1) ⋯ (x - n + 1).

theorem PadicInt.mahlerEquiv_smul {p : ℕ} [Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] {S : Type u_2} [Monoid S] [DistribMulAction S E] [ContinuousConstSMul S E] (c : S) (f : C(ℤ_[p], E)) : (mahlerEquiv E) (c • f) = c • (mahlerEquiv E) f

The Mahler coefficients of c • f are c times those of f, for every scalar action on the coefficient module, since the forward differences commute with it.

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

Mahler's theorem, scalar-linear form. Mathlib's Mahler isometry mahlerEquiv E : C(ℤ_[p], E) ≃ₗᵢ[ℤ_[p]] C₀(ℕ, E) is linear over any semiring S acting on the coefficient module E.

@[simp]

theorem PadicInt.coe_mahlerLinearIsometryEquiv {p : ℕ} [Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_2) [Semiring S] [Module S E] [ContinuousConstSMul S E] : ⇑(mahlerLinearIsometryEquiv S E) = ⇑(mahlerEquiv E)

@[simp]

theorem PadicInt.coe_mahlerLinearIsometryEquiv_symm {p : ℕ} [Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_2) [Semiring S] [Module S E] [ContinuousConstSMul S E] : ⇑(mahlerLinearIsometryEquiv S E).symm = ⇑(mahlerEquiv E).symm

@[simp]

theorem PadicInt.mahlerEquiv_symm_single {p : ℕ} [Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (n : ℕ) (a : E) : (mahlerEquiv E).symm (ZeroAtInftyContinuousMap.single n a) = mahlerTerm a n

The Mahler series of the coordinate vector single n a is the single Mahler term x ↦ (x choose n) • a.

@[simp]

theorem PadicInt.mahlerEquiv_mahlerTerm {p : ℕ} [Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (n : ℕ) (a : E) : (mahlerEquiv E) (mahlerTerm a n) = ZeroAtInftyContinuousMap.single n a

The Mahler coordinates of a single Mahler term form the coordinate vector single n a.

theorem PadicInt.mahlerTerm_eq_smul {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedRing R] [Module ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [SMulCommClass ℤ_[p] R R] (a : R) (n : ℕ) : mahlerTerm a n = a • mahler n • 1

For a normed ring R with a ℤ_[p]-action commuting with left multiplication, the Mahler term with coefficient a is a times the Mahler basis function mahler n • 1.

theorem PadicInt.mahler_natCast_mul {p : ℕ} [Fact (Nat.Prime p)] (m n : ℕ) (x : ℤ_[p]) : (mahler n) (↑m * x) = ∑ k ∈ Finset.range (n + 1), ↑((PowerSeries.coeff n) (((1 + PowerSeries.X) ^ m - 1) ^ k)) * (mahler k) x

Mahler functions of a dilation. For m : ℕ, the function x ↦ (m x choose n) is the integral combination ∑_{k ≤ n} c_{n,k} (x choose k), where c_{n,k} is the coefficient of T ^ n in ((1 + T) ^ m - 1) ^ k. This is the coefficientwise form of (1 + T) ^ (m x) = ((1 + T) ^ m) ^ x = ∑_k (x choose k) ((1 + T) ^ m - 1) ^ k.