An introduction to p-adic L-functions — Lean blueprint

3.2. p-adic measures🔗

We now fix the setting. Let G be a profinite abelian group; the cases G = \Zp and G = \Zpx are of most interest.

Definition3.2.1
uses 1used by 1✓L∃∀N

Let \cC(G, L) be the L-vector space of continuous functions \phi : G \to L, equipped with the valuation \vC(\phi) = \inf_{x \in G} \vp(\phi(x)). As G is compact this is well-defined, induces the sup norm, and makes \cC(G, L) an L-Banach space in the sense of Definition 3.1.2.

Lean code for Definition3.2.1●1 definition
  • structure(2 fields)defined in Mathlib/Topology/ContinuousMap/Defs.lean
    complete
    structure ContinuousMap.{u_1, u_2} (X : Type u_1) (Y : Type u_2)
  [TopologicalSpace X] [TopologicalSpace Y] : Type (max u_1 u_2)
    structure ContinuousMap.{u_1, u_2} (X : Type u_1)
  (Y : Type u_2) [TopologicalSpace X]
  [TopologicalSpace Y] :
  Type (max u_1 u_2)
    The type of continuous maps from `X` to `Y`.

When possible, instead of parametrizing results over `(f : C(X, Y))`,
you should parametrize over `{F : Type*} [ContinuousMapClass F X Y] (f : F)`.

When you extend this structure, make sure to extend `ContinuousMapClass`.

    Fields

    toFun : X → Y
    The function `X → Y` 
    continuous_toFun : Continuous self.toFun
    Proposition that `toFun` is continuous
Definition3.2.2
uses 1
Used by 5
Reverse dependency previews
Preview
Theorem 2.5.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

The space \sM(G, L) of L-valued measures on G is the continuous dual \cC(G, L)^* = \mathrm{Hom}_{\mathrm{cts}}(\cC(G,L), L), using Definition 3.2.1. The pairing of \mu \in \sM(G,L) with \phi \in \cC(G,L) is written \int_G \phi(x) \cdot \mu(x) (or \int_G \phi \cdot \mu). We call \mu an \OL-valued measure, \mu \in \sM(G, \OL), if \int_G \phi \cdot \mu \in \OL for every \OL-valued \phi; boundedness gives \sM(G, L) = \sM(G, \OL) \otimes_{\OL} L. A p-adic measure on \Zp is such a functional with G = \Zp. (All of this applies verbatim to any subset X \subseteq G with the subspace topology, X no longer needing to be a group.)

Lean code for Definition3.2.2●1 definition
  • abbrevdefined in PadicLFunctions/Measure/Basic.lean
    complete
    abbrev PadicMeasure.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (X : Type u_1)
  [TopologicalSpace X] : Type u_1
    abbrev PadicMeasure.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (X : Type u_1)
  [TopologicalSpace X] : Type u_1
    The space of `ℤ_[p]`-valued *p-adic measures* on a topological space `X`: `ℤ_[p]`-linear
functionals on the continuous functions `C(X, ℤ_[p])`. Over `ℤ_[p]` every linear functional
is automatically bounded (norm ≤ 1) and continuous, so this agrees with the continuous
dual used in the source.

Source: RJW Def. 3.6 (`def:measures`, TeX line 760) together with the `𝒪_L`-valued
convention of line 765.
Definition3.2.3
uses 1
Used by 3
Reverse dependency previews
Preview
Proposition 3.2.5
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

For g \in G, the Dirac measure \delta_g \in \sM(G, \OL) is evaluation at g, i.e. \delta_g(\phi) = \phi(g). It depends on Definition 3.2.2.

Lean code for Definition3.2.3●1 definition
  • defdefined in PadicLFunctions/Measure/Basic.lean
    complete
    def PadicMeasure.dirac.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)]
  {X : Type u_1} [TopologicalSpace X] (x : X) : PadicMeasure p X
    def PadicMeasure.dirac.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] {X : Type u_1}
  [TopologicalSpace X] (x : X) :
  PadicMeasure p X
    The *Dirac measure* at `x : X`: the functional `φ ↦ φ x`.

Source: RJW Ex. 3.7 (`ex:dirac`, TeX lines 774–779).
Proposition3.2.4
uses 1
Used by 2
Reverse dependency previews
Preview
Proposition 3.2.5
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Let \cClc(G, \OL) be the locally constant functions G \to \OL, a dense subspace of \cC(G, \OL), and \sMlc(G, \OL) = \cClc(G, \OL)^* its dual. Restriction induces a canonical isomorphism \sM(G, \OL) \xrightarrow{\ \sim\ } \sMlc(G, \OL). This rests on Definition 3.2.2.

Lean code for Proposition3.2.4●2 theorems
  • theoremdefined in PadicLFunctions/Measure/Basic.lean
    complete
    theorem PadicMeasure.exists_locallyConstant_norm_sub_le.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] {X : Type u_1} [TopologicalSpace X]
  [CompactSpace X] (f : C(X, ℤ_[p])) {ε : ℝ} (hε : 0 < ε) :
  ∃ g, ‖f - ↑g‖ ≤ ε
    theorem PadicMeasure.exists_locallyConstant_norm_sub_le.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {X : Type u_1} [TopologicalSpace X]
  [CompactSpace X] (f : C(X, ℤ_[p]))
  {ε : ℝ} (hε : 0 < ε) : ∃ g, ‖f - ↑g‖ ≤ ε
    **Density of locally constant functions**: any continuous `f : X → ℤ_[p]` on a
compact space is uniformly approximated by locally constant functions. The preimages of
the (clopen) balls of radius `ε` form a clopen cover; pass to a finite subcover,
disjointify, and pick values.

Source: RJW Rem. 3.8 (`rem:locally constant`, TeX lines 782–791): "any continuous
function `φ ∈ 𝒞(G, 𝒪_L)` can be p-adically approximated by its locally constant
truncations". Not in mathlib (verified absent); PR candidate.
  • theoremdefined in PadicLFunctions/Measure/Basic.lean
    complete
    theorem PadicMeasure.ext_locallyConstant.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)]
  {X : Type u_1} [TopologicalSpace X] [CompactSpace X]
  {μ ν : PadicMeasure p X}
  (h : ∀ (g : LocallyConstant X ℤ_[p]), μ ↑g = ν ↑g) : μ = ν
    theorem PadicMeasure.ext_locallyConstant.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {X : Type u_1} [TopologicalSpace X]
  [CompactSpace X]
  {μ ν : PadicMeasure p X}
  (h :
    ∀ (g : LocallyConstant X ℤ_[p]),
      μ ↑g = ν ↑g) :
  μ = ν
    A measure is determined by its values on locally constant functions.

Source: RJW Eq. (3.1) (`eq:restrict measures`, TeX lines 787–799): restriction defines
an isomorphism `ℳ(G, 𝒪_L) ≅ ℳ^lc(G, 𝒪_L)`; injectivity is this statement.
Proof for Proposition 3.2.4
uses 0

Any continuous \phi \in \cC(G, \OL) is the p-adic limit of its locally constant truncations \phi_n(x) = \sum_{a \in \Z/p^n\Z} \phi(a)\, \one_{a + p^n\Zp}(x), so \cClc is dense and restriction \sM \to \sMlc is injective. For surjectivity one writes down an inverse: given \mu^{\mathrm{lc}} \in \sMlc(G,\OL) and \phi \in \cC(G,\OL), pick locally constant \phi_n \to \phi and set \int_G \phi \cdot \mu := \lim_n \int_G \phi_n \cdot \mu^{\mathrm{lc}}. By continuity the limit exists and is independent of the chosen sequence, giving a well-defined measure inverse to restriction.

Proposition3.2.5
uses 1used by 0XL∃∀N

Locally constant measures \sMlc(G, \OL) are identified with the additive functions \mu : \set{\text{open compact subsets of } G} \to \OL. Combined with Proposition 3.2.4, this identifies \sM(G, \OL) with the additive functions on the open compact subsets of G.

Proof for Proposition 3.2.5
uses 1

Given \mu \in \sMlc(G, \OL), set \mu(U) := \int_G \one_U \cdot \mu for an open compact U; additivity of U \mapsto \mu(U) is clear from linearity. Conversely an additive set-function integrates a locally constant \phi, factoring through G/H for some open subgroup H, by the finite sum \int_G \phi \cdot \mu := \sum_{[a] \in G/H} \phi(a)\,\mu(aH); the two constructions are mutually inverse. (On \Zp the real-valued Haar measure, with a + p^n\Zp \mapsto p^{-n}, is not a p-adic measure, being p-adically unbounded.) Under this dictionary the Dirac measure \delta_g from Definition 3.2.3 is the set-function X \mapsto 1 if g \in X and 0 otherwise.