The Amice transform

We identify the measures on ℤ_[p] with the power series ring ℤ_[p]⟦X⟧, by sending a measure μ to the power series with n-th coefficient μ (mahler n).

More suggestively, this is the series ∫ a : ℤ_[p], (1 + X) ^ a dμ.

Main statements

• AbstractMeasure.amiceTransform: the Amice transform as an R-linear map into R⟦X⟧, allowing R to be any normed ℤ_[p]-algebra
• AbstractMeasure.coeff_amiceTransform: the n-th coefficient of μ.amiceTransform is μ (mahler n)
• AbstractMeasure.amiceTransformEquiv: the Amice transform with ℤ_[p]-coefficients, bundled as a linear equivalence.

TODO

Define the Amice transform as an equivalence over more general base rings; this requires developing some theory of bounded power series over normed rings.

References

• P. Colmez, Fonctions d'une variable p-adique, section II.2

theorem AbstractMeasure.ext_mahler {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedCommRing R] [Algebra ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] [IsBoundedSMul ℤ_[p] R] {μ : AbstractMeasure ℤ_[p] R R} (hμ : ∀ (n : ℕ), μ (mahler n • 1) = 0) : μ = 0

Reformulation of PadicInt.ext_mahler in terms of the type synonym D(ℤ_[p], R).

noncomputable def AbstractMeasure.amiceTransform {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace R] [Algebra ℤ_[p] R] [ContinuousSMul ℤ_[p] R] [IsTopologicalRing R] : AbstractMeasure ℤ_[p] R R →ₗ[R] PowerSeries R

The Amice transform, sending a measure μ on ℤ_[p] to the power series with n-th coefficient μ (mahler n). More suggestively, this is the series ∫ a : ℤ_[p], (1 + X) ^ a dμ.

See also amiceTransformEquiv for the same map bundled as a linear equivalence.

Equations

• AbstractMeasure.amiceTransform = { toFun := fun (μ : AbstractMeasure ℤ_[p] R R) => PowerSeries.mk fun (n : ℕ) => μ (mahler n • 1), map_add' := ⋯, map_smul' := ⋯ }

theorem AbstractMeasure.coeff_amiceTransform {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace R] [Algebra ℤ_[p] R] [ContinuousSMul ℤ_[p] R] [IsTopologicalRing R] (μ : AbstractMeasure ℤ_[p] R R) (n : ℕ) : (PowerSeries.coeff n) (amiceTransform μ) = μ (mahler n • 1)

theorem AbstractMeasure.injective_amiceTransform {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedCommRing R] [Algebra ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] [IsBoundedSMul ℤ_[p] R] : Function.Injective ⇑amiceTransform

noncomputable def AbstractMeasure.invTransform {p : ℕ} [Fact (Nat.Prime p)] (F : PowerSeries ℤ_[p]) : AbstractMeasure ℤ_[p] ℤ_[p] ℤ_[p]

The inverse of the Amice transform, sending a power series F to the unique measure that sends mahler n to the n-th coefficient of F.

Equations

• AbstractMeasure.invTransform F = AbstractMeasure.toCLMEquiv.symm ((AbstractMeasure.invTransformₗ✝ F).mkContinuous 1 ⋯)

theorem AbstractMeasure.invTransform_apply {p : ℕ} [Fact (Nat.Prime p)] (F : PowerSeries ℤ_[p]) (f : C(ℤ_[p], ℤ_[p])) : (invTransform F) f = ∑' (i : ℕ), ((PadicInt.mahlerEquiv ℤ_[p]) f) i * (PowerSeries.coeff i) F

theorem AbstractMeasure.amiceTransform_invTransform {p : ℕ} [Fact (Nat.Prime p)] (F : PowerSeries ℤ_[p]) : amiceTransform (invTransform F) = F

noncomputable def AbstractMeasure.amiceTransformEquiv {p : ℕ} [Fact (Nat.Prime p)] : AbstractMeasure ℤ_[p] ℤ_[p] ℤ_[p] ≃ₗ[ℤ_[p]] PowerSeries ℤ_[p]

The Amice transform bundled as a linear equivalence (with coefficients in ℤ_[p]).

(TODO: Define this more generally -- this will need a definition for bounded power series over a normed ring.)

Equations

• AbstractMeasure.amiceTransformEquiv = { toLinearMap := AbstractMeasure.amiceTransform, invFun := AbstractMeasure.invTransform, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem AbstractMeasure.amiceTransformEquiv_apply {p : ℕ} [Fact (Nat.Prime p)] (μ : AbstractMeasure ℤ_[p] ℤ_[p] ℤ_[p]) : amiceTransformEquiv μ = amiceTransform μ

theorem AbstractMeasure.coeff_amiceTransformEquiv {p : ℕ} [Fact (Nat.Prime p)] (μ : AbstractMeasure ℤ_[p] ℤ_[p] ℤ_[p]) (n : ℕ) : (PowerSeries.coeff n) (amiceTransformEquiv μ) = μ (mahler n)