Mahler duality for measures on ℤ_p

Let R be a complete ultrametric normed commutative ring with a contractive ℤ_[p]-algebra structure. A measure μ ∈ D(ℤ_p, R) is a continuous R-linear functional on C(ℤ_[p], R), and its Amice transform A_μ has the moments b_n = μ (x ↦ x choose n) as coefficients. Mahler's theorem identifies C(ℤ_[p], R) isometrically with the null sequences C₀(ℕ, R), the coordinate vectors corresponding to the Mahler basis. Hence, dually, measures correspond to bounded moment sequences:

• every integral is the convergent series μ f = ∑ n, a_n(f) * b_n in the Mahler coefficients a_n(f) = Δ^n f (0) of f (AbstractMeasure.hasSum_mahlerEquiv_mul_coeff_amiceTransform);
• a bound ‖b_n‖ ≤ C on the moments gives ‖μ f‖ ≤ C * ‖f‖, and conversely (AbstractMeasure.norm_apply_le_of_forall_norm_coeff_le, AbstractMeasure.norm_coeff_amiceTransform_le).

When R admits a multiplicative pseudo-uniformiser (TauCeti.NormedRing.IsTate R), every continuous linear functional is bounded, so the moments of every measure are bounded, and the moments give an R-linear equivalence AbstractMeasure.mahlerMomentsEquiv between D(ℤ_p, R) and the bounded sequences ℓ^∞(ℕ, R). The operator norm of a measure is the supremum of the norms of its moments, and a power series is an Amice transform exactly when its coefficients are bounded. Over a nontrivially normed field, for instance a complete extension of ℚ_p, this is the statement for Mathlib's operator norm (AbstractMeasure.norm_toCLMEquiv_eq_iSup_coeff). Over ℚ_p the bounded measures therefore do not exhaust the power series: ∑ p⁻ⁿ Tⁿ is not an Amice transform. The integral case R = ℤ_[p], where every power series is an Amice transform, is Mathlib's AbstractMeasure.amiceTransformEquiv.

No norm is installed on the measure carrier; norms are taken on its image under Mathlib's AbstractMeasure.toCLMEquiv. Over ring scalars this is the operator norm of the scope TauCeti.RingOpNorm.

Main definitions

• AbstractMeasure.mahlerMomentsEquiv: over a ring with a multiplicative pseudo-uniformiser, the linear equivalence between measures on ℤ_p and bounded moment sequences.

Main results

• AbstractMeasure.mahlerMomentsEquiv_apply, AbstractMeasure.mahlerMomentsEquiv_symm_apply: the moments of a measure, and the measure with given bounded moments.
• AbstractMeasure.hasSum_mahlerEquiv_mul_coeff_amiceTransform: the Mahler expansion of an integral.
• AbstractMeasure.bddAbove_norm_coeff_amiceTransform: over Tate scalars, the moments of a measure are bounded.
• AbstractMeasure.ringOpNorm_toCLMEquiv_eq_iSup_coeff: over Tate scalars, the operator norm of a measure is the supremum of the norms of its moments.
• AbstractMeasure.norm_toCLMEquiv_eq_iSup_coeff: the same over a nontrivially normed field, for Mathlib's operator norm.
• AbstractMeasure.norm_toCLMEquiv_le_iff_forall_norm_coeff_le: hence over such a field a measure has norm at most C exactly when its moments do.
• AbstractMeasure.mem_range_amiceTransform_iff: a power series is the Amice transform of a measure exactly when its coefficients are bounded.

References

• K. Mahler, An interpolation series for continuous functions of a p-adic variable, J. reine angew. Math. 199 (1958), 23–34.
• Y. Amice, Interpolation p-adique, Bull. Soc. Math. France 92 (1964), 117–180.
• P. Colmez, Fonctions d'une variable p-adique, Astérisque 330 (2010), §I.3 and §II.2.
• J. Rodrigues Jacinto and C. Williams, An introduction to p-adic L-functions, §3.

theorem AbstractMeasure.norm_coeff_amiceTransform_le {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedCommRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [NormOneClass R] (μ : AbstractMeasure ℤ_[p] R R) {C : ℝ} (hμ : ∀ (f : C(ℤ_[p], R)), ‖μ f‖ ≤ C * ‖f‖) (n : ℕ) : ‖(PowerSeries.coeff n) (amiceTransform μ)‖ ≤ C

A bound ‖μ f‖ ≤ C * ‖f‖ on a measure bounds its moments by C, since the Mahler basis functions have norm one.

theorem AbstractMeasure.hasSum_mahlerEquiv_mul_coeff_amiceTransform {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedCommRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] (μ : AbstractMeasure ℤ_[p] R R) (f : C(ℤ_[p], R)) : HasSum (fun (n : ℕ) => ((PadicInt.mahlerEquiv R) f) n * (PowerSeries.coeff n) (amiceTransform μ)) (μ f)

Mahler expansion of an integral. The integral of f against μ is the sum over n of the Mahler coefficients Δ^n f (0) of f times the moments μ (x ↦ x choose n), the coefficients of the Amice transform of μ.

theorem AbstractMeasure.norm_apply_le_of_forall_norm_coeff_le {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedCommRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] (μ : AbstractMeasure ℤ_[p] R R) {C : ℝ} (hC : ∀ (n : ℕ), ‖(PowerSeries.coeff n) (amiceTransform μ)‖ ≤ C) (f : C(ℤ_[p], R)) : ‖μ f‖ ≤ C * ‖f‖

A bound C on the norms of the moments of a measure is a bound for the measure: ‖μ f‖ ≤ C * ‖f‖.

theorem AbstractMeasure.bddAbove_norm_coeff_amiceTransform {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] (μ : AbstractMeasure ℤ_[p] R R) : BddAbove (Set.range fun (n : ℕ) => ‖(PowerSeries.coeff n) (amiceTransform μ)‖)

Over a ring with a multiplicative pseudo-uniformiser, the moments of every measure on ℤ_p are bounded.

noncomputable def AbstractMeasure.mahlerMomentsEquiv (p : ℕ) [Fact (Nat.Prime p)] (R : Type u_1) [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] : AbstractMeasure ℤ_[p] R R ≃ₗ[R] ↥(lp (fun (x : ℕ) => R) ⊤)

Mahler duality. Over a ring with a multiplicative pseudo-uniformiser, a measure on ℤ_p is determined by its moments μ (x ↦ x choose n), the coefficients of its Amice transform, and every bounded sequence is the moment sequence of a measure. The inverse sends a bounded sequence b to the measure f ↦ ∑ n, Δ^n f (0) * b n.

@[simp]

theorem AbstractMeasure.mahlerMomentsEquiv_apply {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] (μ : AbstractMeasure ℤ_[p] R R) (n : ℕ) : ↑((mahlerMomentsEquiv p R) μ) n = (PowerSeries.coeff n) (amiceTransform μ)

The moment sequence of a measure is the coefficient sequence of its Amice transform.

@[simp]

theorem AbstractMeasure.amiceTransform_mahlerMomentsEquiv_symm {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] (b : ↥(lp (fun (x : ℕ) => R) ⊤)) : amiceTransform ((mahlerMomentsEquiv p R).symm b) = PowerSeries.mk ↑b

The measure with a given bounded moment sequence has that sequence as the coefficients of its Amice transform.

theorem AbstractMeasure.mahlerMomentsEquiv_symm_apply {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] (b : ↥(lp (fun (x : ℕ) => R) ⊤)) (f : C(ℤ_[p], R)) : ((mahlerMomentsEquiv p R).symm b) f = ∑' (n : ℕ), ((PadicInt.mahlerEquiv R) f) n * ↑b n

The measure with a bounded moment sequence b integrates f to ∑ n, Δ^n f (0) * b n.

theorem AbstractMeasure.ringOpNorm_toCLMEquiv_eq_iSup_coeff {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] (μ : AbstractMeasure ℤ_[p] R R) : ‖toCLMEquiv μ‖ = ⨆ (n : ℕ), ‖(PowerSeries.coeff n) (amiceTransform μ)‖

Over a ring with a multiplicative pseudo-uniformiser, the operator norm of a measure on ℤ_p is the supremum of the norms of its moments.

theorem AbstractMeasure.ringOpNorm_toCLMEquiv_eq_norm_mahlerMomentsEquiv {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] (μ : AbstractMeasure ℤ_[p] R R) : ‖toCLMEquiv μ‖ = ‖(mahlerMomentsEquiv p R) μ‖

Mahler duality is isometric: the operator norm of a measure is the supremum norm of its moment sequence.

theorem AbstractMeasure.mem_range_amiceTransform_iff {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] (F : PowerSeries R) : F ∈ amiceTransform.range ↔ BddAbove (Set.range fun (n : ℕ) => ‖(PowerSeries.coeff n) F‖)

The range of the Amice transform. Over a ring with a multiplicative pseudo-uniformiser, a power series is the Amice transform of a measure on ℤ_p exactly when its coefficients are bounded.

theorem AbstractMeasure.norm_toCLMEquiv_eq_iSup_coeff {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [NontriviallyNormedField K] [Algebra ℤ_[p] K] [IsBoundedSMul ℤ_[p] K] [IsUltrametricDist K] [CompleteSpace K] (μ : AbstractMeasure ℤ_[p] K K) : ‖toCLMEquiv μ‖ = ⨆ (n : ℕ), ‖(PowerSeries.coeff n) (amiceTransform μ)‖

Mahler duality for field coefficients. Over a complete ultrametric nontrivially normed field with a contractive ℤ_[p]-algebra structure, such as a complete extension of ℚ_p, the operator norm of a measure on ℤ_p is the supremum of the norms of the coefficients of its Amice transform.

theorem AbstractMeasure.norm_toCLMEquiv_le_iff_forall_norm_coeff_le {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [NontriviallyNormedField K] [Algebra ℤ_[p] K] [IsBoundedSMul ℤ_[p] K] [IsUltrametricDist K] [CompleteSpace K] (μ : AbstractMeasure ℤ_[p] K K) {C : ℝ} : ‖toCLMEquiv μ‖ ≤ C ↔ ∀ (n : ℕ), ‖(PowerSeries.coeff n) (amiceTransform μ)‖ ≤ C

Over a complete ultrametric nontrivially normed field with a contractive ℤ_[p]-algebra structure, a measure on ℤ_p has operator norm at most C exactly when every coefficient of its Amice transform has norm at most C.