Integral measures on ℤ_p and the dual unit ball

A ℚ_p-valued measure ν on ℤ_p is integral when it is the extension of coefficients of a ℤ_p-valued measure μ, that is, when ν (f) = μ (f) for every ℤ_p-valued test function f. This file identifies the integral measures with the closed unit ball for the operator norm, and describes that ball on the side of the Amice transform:

• extension of coefficients along a continuous ℤ_[p]-algebra map j applies j to the coefficients of the Amice transform (AbstractMeasure.amiceTransform_extendCoefficients). For ℤ_p ⊆ ℚ_p this is the compatibility of Mathlib's integral Amice equivalence AbstractMeasure.amiceTransformEquiv with extension to ℚ_p (AbstractMeasure.amiceTransform_extendCoefficients_coe_ringHom);
• a ℚ_p-valued measure has operator norm at most 1 exactly when it is the unique extension of a ℤ_p-valued measure (AbstractMeasure.existsUnique_integral_iff_norm_le_one), and exactly when its Amice transform has coefficients in ℤ_p (AbstractMeasure.norm_toCLMEquiv_le_one_iff_exists_amiceTransform_eq_map).

The first characterisation is the case j : ℤ_[p] → ℚ_[p] of AbstractMeasure.existsUnique_apply_comp_eq_iff_norm_le_one: a measure of norm at most 1 sends ℤ_p-valued test functions, of norm at most 1, into ℤ_p. The second combines it with Mahler duality, which computes the operator norm as the supremum of the norms of the moments.

References

• J. Rodrigues Jacinto and C. Williams, An introduction to p-adic L-functions, Essential Number Theory 4 (2025), no. 1, 101–216, §3, Remark 3.28.
• P. Colmez, Fonctions d'une variable p-adique, Astérisque 330 (2010), §I.3 and §II.2.

@[simp]

theorem AbstractMeasure.amiceTransform_extendCoefficients {p : ℕ} [Fact (Nat.Prime p)] {O : Type u_1} {K : Type u_2} [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] [Algebra ℤ_[p] O] [ContinuousSMul ℤ_[p] O] [NormedField K] [IsUltrametricDist K] [CompleteSpace K] [Algebra ℤ_[p] K] [ContinuousSMul ℤ_[p] K] (j : O →ₐ[ℤ_[p]] K) (hjc : Continuous ⇑j) (hj : ∀ (a : O), ‖j a‖ ≤ 1) (μ : AbstractMeasure ℤ_[p] O O) : amiceTransform ((extendCoefficients (↑j) hj) μ) = (PowerSeries.map ↑j) (amiceTransform μ)

Extension of coefficients along a continuous ℤ_[p]-algebra map j into the closed unit ball applies j to the coefficients of the Amice transform.

@[simp]

theorem AbstractMeasure.amiceTransform_extendCoefficients_coe_ringHom {p : ℕ} [Fact (Nat.Prime p)] (μ : AbstractMeasure ℤ_[p] ℤ_[p] ℤ_[p]) : amiceTransform ((extendCoefficients PadicInt.Coe.ringHom ⋯) μ) = (PowerSeries.map PadicInt.Coe.ringHom) (amiceTransform μ)

Extension of coefficients from ℤ_p to ℚ_p applies the inclusion to the coefficients of the Amice transform.

theorem AbstractMeasure.existsUnique_integral_iff_norm_le_one {p : ℕ} [Fact (Nat.Prime p)] (ν : AbstractMeasure ℤ_[p] ℚ_[p] ℚ_[p]) : (∃! μ : AbstractMeasure ℤ_[p] ℤ_[p] ℤ_[p], ∀ (f : C(ℤ_[p], ℤ_[p])), ν ({ toFun := fun (x : ℤ_[p]) => ↑x, continuous_toFun := ⋯ }.comp f) = ↑(μ f)) ↔ ‖toCLMEquiv ν‖ ≤ 1

The integral dual unit ball. A ℚ_p-valued measure on ℤ_p has operator norm at most 1 exactly when there is a unique ℤ_p-valued measure μ with ν (f) = μ (f) for every ℤ_p-valued test function f.

theorem AbstractMeasure.norm_toCLMEquiv_le_one_iff_exists_amiceTransform_eq_map {p : ℕ} [Fact (Nat.Prime p)] (ν : AbstractMeasure ℤ_[p] ℚ_[p] ℚ_[p]) : ‖toCLMEquiv ν‖ ≤ 1 ↔ ∃ (F : PowerSeries ℤ_[p]), amiceTransform ν = (PowerSeries.map PadicInt.Coe.ringHom) F

A ℚ_p-valued measure on ℤ_p has operator norm at most 1 exactly when its Amice transform has coefficients in ℤ_p.

The checks of the integral dual unit ball: the zero measure and the Dirac measures are integral, while p⁻¹ δ₀ is not.