3.6. Pseudo-measures🔗

The Mahler transform matches measures with bounded analytic functions on the open unit disc. The Riemann zeta function has a simple pole at s = 1, so we must allow simple poles on the p-adic side; this is the role of pseudo-measures.

Definition3.6.1

Statement uses 2

Statement dependency previews

Preview

Definition 3.3.3

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

Used by 11

Reverse dependency previews

Preview

Theorem 2.5.1

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

Let G be profinite abelian and Q(G) the ring of fractions of the Iwasawa algebra Definition 3.3.3. A pseudo-measure on G is an element \lambda \in Q(G) such that ([g] - [1])\lambda \in \Lam(G) for every g \in G (product = convolution Definition 3.3.4).

Lean code for Definition3.6.1●1 definition

defdefined in PadicLFunctions/Measure/PseudoMeasure.lean

complete

def PadicMeasure.IsPseudoMeasure (p : ℕ) [hp : Fact (Nat.Prime p)]
  (q : PadicMeasure.QuotientField p) : Prop

def PadicMeasure.IsPseudoMeasure (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (q : PadicMeasure.QuotientField p) :
  Prop

A *pseudo-measure* on `ℤ_p^×`: an element `λ` of `Q(ℤ_p^×)` with
`([g]−[1])·λ ∈ Λ(ℤ_p^×)` for all `g`.

Source: RJW Def. 3.34 (TeX lines 1185–1191).

Definition3.6.2

uses 1used by 1XL∃∀N

For a non-trivial character \chi : G \to \Cp^\times and a pseudo-measure \lambda, define \int_G \chi \cdot \lambda := (\chi(g) - 1)^{-1} \int_G \chi \cdot ([g] - [1])\lambda, for any g with \chi(g) \neq 1. Uses Definition 3.6.1.

Proposition3.6.3

uses 1used by 0XL∃∀N

The value \int_G \chi \cdot \lambda of Definition 3.6.2 is independent of the chosen g.

Proof for Proposition 3.6.3

uses 0

Because \mu \mapsto \int_G \chi \cdot \mu is a ring homomorphism \Lam(G) \to \Cp (convolution becomes multiplication, \chi being a character), for g, h with \chi(g), \chi(h) \neq 1 one computes (\chi(h)-1)\int_G \chi\cdot([g]-[1])\lambda = \int_G \chi\cdot([g]-[1])([h]-[1])\lambda = (\chi(g)-1)\int_G \chi\cdot([h]-[1])\lambda, using commutativity. Dividing through shows the two definitions agree. Equivalently, the homomorphism \Lam(G) \to \Cp extends uniquely to Q(G) \to \Cp, and its value on \lambda is the expression above.

Proposition3.6.4

uses 0used by 0✓L∃∀N

Let \mu \in \Lam(\Zpx). (i) If \int_{\Zpx} x^k \cdot \mu = 0 for all k > 0, then \mu = 0. (ii) If \int_{\Zpx} x^k \cdot \mu \neq 0 for all k > 0, then \mu is not a zero divisor in \Lam(\Zpx). (iii) Part (i) holds more generally for a pseudo-measure \mu. In particular a pseudo-measure on \Zpx is determined by the values \int_{\Zpx} x^k \cdot \mu, k > 0.

Lean code for Proposition3.6.4●3 theorems

theoremdefined in PadicLFunctions/Measure/PseudoMeasure.lean

complete

theorem PadicMeasure.eq_zero_of_forall_unitsPowCM_eq_zero (p : ℕ)
  [hp : Fact (Nat.Prime p)] (μ : PadicMeasure p ℤ_[p]ˣ)
  (h : ∀ (k : ℕ), 0 < k → μ (PadicMeasure.unitsPowCM p k) = 0) : μ = 0

theorem PadicMeasure.eq_zero_of_forall_unitsPowCM_eq_zero
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]ˣ)
  (h :
    ∀ (k : ℕ),
      0 < k →
        μ (PadicMeasure.unitsPowCM p k) =
          0) :
  μ = 0

**RJW Lem. 3.36(i) (`lem:zero divisor`)**: a measure on `ℤ_p^×` with
`∫ x^k dμ = 0` for all `k > 0` is zero. Source proof (TeX lines 1228–1229): the Mahler
transform of `ιμ` is constant (binomial polynomials with `n ≥ 1` have no constant
term), and `ψ` fixes constants while killing `ιμ`; hence `𝓐_{ιμ} = 0`.

theoremdefined in PadicLFunctions/Measure/PseudoMeasure.lean

complete

theorem PadicMeasure.mem_nonZeroDivisors_of_forall_unitsPowCM_ne_zero (p : ℕ)
  [hp : Fact (Nat.Prime p)] (μ : PadicMeasure p ℤ_[p]ˣ)
  (h : ∀ (k : ℕ), 0 < k → μ (PadicMeasure.unitsPowCM p k) ≠ 0) :
  μ ∈ nonZeroDivisors (PadicMeasure p ℤ_[p]ˣ)

theorem PadicMeasure.mem_nonZeroDivisors_of_forall_unitsPowCM_ne_zero
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]ˣ)
  (h :
    ∀ (k : ℕ),
      0 < k →
        μ (PadicMeasure.unitsPowCM p k) ≠
          0) :
  μ ∈
    nonZeroDivisors
      (PadicMeasure p ℤ_[p]ˣ)

**RJW Lem. 3.36(ii)**: a measure on `ℤ_p^×` with `∫ x^k dμ ≠ 0` for all `k > 0`
is not a zero divisor. Source proof (TeX lines 1232–1234): `∫ (xy)^k d(μ⋆λ) =
(∫ x^k dμ)(∫ y^k dλ)`, then apply (i).

theoremdefined in PadicLFunctions/Measure/PseudoMeasure.lean

complete

theorem PadicMeasure.pseudoMeasure_eq_zero_of_moments (p : ℕ)
  [hp : Fact (Nat.Prime p)] {a : ℤ_[p]ˣ}
  (ha : ∀ (k : ℕ), 0 < k → ↑a ^ k ≠ 1)
  (q : PadicMeasure.QuotientField p)
  (hq : PadicMeasure.IsPseudoMeasure p q)
  (h :
    ∀ (k : ℕ),
      0 < k →
        ∀ (ν : PadicMeasure p ℤ_[p]ˣ),
          (algebraMap (PadicMeasure p ℤ_[p]ˣ)
                    (PadicMeasure.QuotientField p))
                  (PadicMeasure.dirac p a - 1) *
                q =
              (algebraMap (PadicMeasure p ℤ_[p]ˣ)
                  (PadicMeasure.QuotientField p))
                ν →
            ν (PadicMeasure.unitsPowCM p k) = 0) :
  q = 0

theorem PadicMeasure.pseudoMeasure_eq_zero_of_moments
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {a : ℤ_[p]ˣ}
  (ha : ∀ (k : ℕ), 0 < k → ↑a ^ k ≠ 1)
  (q : PadicMeasure.QuotientField p)
  (hq : PadicMeasure.IsPseudoMeasure p q)
  (h :
    ∀ (k : ℕ),
      0 < k →
        ∀ (ν : PadicMeasure p ℤ_[p]ˣ),
          (algebraMap
                    (PadicMeasure p
                      ℤ_[p]ˣ)
                    (PadicMeasure.QuotientField
                      p))
                  (PadicMeasure.dirac p
                      a -
                    1) *
                q =
              (algebraMap
                  (PadicMeasure p ℤ_[p]ˣ)
                  (PadicMeasure.QuotientField
                    p))
                ν →
            ν
                (PadicMeasure.unitsPowCM p
                  k) =
              0) :
  q = 0

**RJW Lem. 3.36(iii)**: a pseudo-measure all of whose moments `∫ x^k` (`k > 0`)
vanish is zero. The moments of a pseudo-measure `q` are encoded via any `g` with
`g^k ≠ 1`: `∫x^k q := (g^k − 1)^{-1} ∫x^k (([g]−[1])q)`. Here we state it via the
witnessing measures directly. Source: TeX lines 1236–1240.

Proof for Proposition 3.6.4

Proof uses 3

Proof dependency previews

Preview

Proposition 3.5.6

Loading preview

Proof dependency preview content is loaded from the Blueprint HTML cache.

(i) Each \binomc{x}{k} with k \geq 1 is a combination of positive powers of x, so the vanishing forces \Am_\mu(T) to be constant. As \mu is supported on \Zpx, Corollary 3.5.7 gives \psi(\Am_\mu) = 0; but \psi fixes constants (by the formula in Proposition 3.5.6), so the constant is 0, i.e. \Am_\mu = 0 and \mu = 0. (ii) If \mu *_{\Zpx} \lambda = 0, then for each k, 0 = \int_{\Zpx} x^k(\mu *_{\Zpx}\lambda) = (\int_{\Zpx} x^k\mu)(\int_{\Zpx} x^k\lambda) by multiplicativity of x^k over the convolution Proposition 3.5.8; the hypothesis forces \int_{\Zpx} x^k \lambda = 0 for all k, so \lambda = 0 by (i). (iii) For a pseudo-measure \mu and an integer a \neq 1 prime to p, \lambda = ([a]-[1])\mu is a measure with \int_{\Zpx} x^k \lambda = (a^k - 1)\int_{\Zpx} x^k \mu = 0, so \lambda = 0 by (i); since [a]-[1] satisfies (ii) it is not a zero divisor, forcing \mu = 0.

Definition3.6.5

uses 0used by 1✓L∃∀N

The augmentation ideal I((\Z/p^n\Z)^\times) \subset \OL[(\Z/p^n\Z)^\times] is the kernel of the degree map \sum_a c_a [a] \mapsto \sum_a c_a. These assemble into a degree map \Lam(\Zpx) \to \OL, whose kernel is the augmentation ideal I(\Zpx) \subset \Lam(\Zpx), and I(\Zpx) \cong \varprojlim_n I((\Z/p^n\Z)^\times).

Lean code for Definition3.6.5●2 definitions

defdefined in PadicLFunctions/Measure/PseudoMeasure.lean

complete

def PadicMeasure.deg.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1}
  [TopologicalSpace G] [CommMonoid G] [ContinuousMul G]
  [CompactSpace G] : PadicMeasure p G →+* ℤ_[p]

def PadicMeasure.deg.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] {G : Type u_1}
  [TopologicalSpace G] [CommMonoid G]
  [ContinuousMul G] [CompactSpace G] :
  PadicMeasure p G →+* ℤ_[p]

The degree (augmentation) map `Λ(G) → ℤ_p`, `μ ↦ ∫_G 1 dμ`.

Source: RJW Def. 3.37 (`DefAugmentationIdealFiniteLevel`, TeX lines 1245–1253); the
inverse-limit degree map is evaluation at the constant function `1`.

defdefined in PadicLFunctions/Measure/PseudoMeasure.lean

complete

def PadicMeasure.augmentationIdeal.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)]
  {G : Type u_1} [TopologicalSpace G] [CommMonoid G] [ContinuousMul G]
  [CompactSpace G] : Ideal (PadicMeasure p G)

def PadicMeasure.augmentationIdeal.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {G : Type u_1} [TopologicalSpace G]
  [CommMonoid G] [ContinuousMul G]
  [CompactSpace G] :
  Ideal (PadicMeasure p G)

The augmentation ideal `I(G) = ker(deg)`. Source: RJW Def. 3.37.

Proposition3.6.6

Statement uses 2

Statement dependency previews

Preview

Definition 3.6.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Let a be a topological generator of \Zpx and \mu \in \Lam(\Zpx) a measure. Then \mu' := \mu / ([a] - [1]) \in Q(\Zpx) is a pseudo-measure. Conversely every pseudo-measure has this shape. This uses Definition 3.6.1 and Definition 3.6.5.

Lean code for Proposition3.6.6●4 theorems

theoremdefined in PadicLFunctions/Measure/PseudoMeasure.lean

complete

theorem PadicMeasure.exists_topological_generator (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) :
  ∃ a,
    ∀ (n : ℕ),
      Subgroup.zpowers ((PadicMeasure.unitsToZModPow p n) a) = ⊤

theorem PadicMeasure.exists_topological_generator
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) :
  ∃ a,
    ∀ (n : ℕ),
      Subgroup.zpowers
          ((PadicMeasure.unitsToZModPow p
              n)
            a) =
        ⊤

For odd `p` there is a *topological generator* of `ℤ_p^×`: an `a` whose image
generates `(ℤ/p^n)^×` for every `n`. The hypothesis `p ≠ 2` is essential:
`(ZMod 8)ˣ` is not cyclic. Proof: the per-level generator sets are nonempty nested
clopen subsets of the compact `ℤ_[p]ˣ`; pick a point of the intersection.
Source: RJW Lem. 3.38 (the proof opens "As p is odd").

theoremdefined in PadicLFunctions/Measure/PseudoMeasure.lean

complete

theorem PadicMeasure.augmentationIdeal_eq_span (p : ℕ) [hp : Fact (Nat.Prime p)]
  {a : ℤ_[p]ˣ}
  (ha :
    ∀ (n : ℕ),
      Subgroup.zpowers ((PadicMeasure.unitsToZModPow p n) a) = ⊤) :
  PadicMeasure.augmentationIdeal p =
    Ideal.span {PadicMeasure.dirac p a - 1}

theorem PadicMeasure.augmentationIdeal_eq_span
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {a : ℤ_[p]ˣ}
  (ha :
    ∀ (n : ℕ),
      Subgroup.zpowers
          ((PadicMeasure.unitsToZModPow p
              n)
            a) =
        ⊤) :
  PadicMeasure.augmentationIdeal p =
    Ideal.span
      {PadicMeasure.dirac p a - 1}

For a topological generator `a`, the augmentation ideal is principal, generated by
`[a] − [1]`: at each finite level the augmentation ideal of the (cyclic) group ring
`ℤ_p[(ℤ/p^n)^×]` is generated by `[ā]−[1]`; compatibility and a compactness argument
pass this to the limit. Source: RJW Lem. 3.38, proof (TeX lines 1264–1282).

theoremdefined in PadicLFunctions/Measure/PseudoMeasure.lean

complete

theorem PadicMeasure.isPseudoMeasure_mk' (p : ℕ) [hp : Fact (Nat.Prime p)]
  {a : ℤ_[p]ˣ}
  (ha :
    ∀ (n : ℕ),
      Subgroup.zpowers ((PadicMeasure.unitsToZModPow p n) a) = ⊤)
  (hreg :
    PadicMeasure.dirac p a - 1 ∈
      nonZeroDivisors (PadicMeasure p ℤ_[p]ˣ))
  (μ : PadicMeasure p ℤ_[p]ˣ) :
  PadicMeasure.IsPseudoMeasure p
    (IsLocalization.mk' (PadicMeasure.QuotientField p) μ
      ⟨PadicMeasure.dirac p a - 1, hreg⟩)

theorem PadicMeasure.isPseudoMeasure_mk' (p : ℕ)
  [hp : Fact (Nat.Prime p)] {a : ℤ_[p]ˣ}
  (ha :
    ∀ (n : ℕ),
      Subgroup.zpowers
          ((PadicMeasure.unitsToZModPow p
              n)
            a) =
        ⊤)
  (hreg :
    PadicMeasure.dirac p a - 1 ∈
      nonZeroDivisors
        (PadicMeasure p ℤ_[p]ˣ))
  (μ : PadicMeasure p ℤ_[p]ˣ) :
  PadicMeasure.IsPseudoMeasure p
    (IsLocalization.mk'
      (PadicMeasure.QuotientField p) μ
      ⟨PadicMeasure.dirac p a - 1, hreg⟩)

**RJW Lem. 3.38 (`lem:pseudo-measure existence`)**: for a topological generator `a`
and any measure `μ`, the quotient `μ/([a]−[1])` is a pseudo-measure.

theoremdefined in PadicLFunctions/Measure/PseudoMeasure.lean

complete

theorem PadicMeasure.isPseudoMeasure_iff_exists (p : ℕ)
  [hp : Fact (Nat.Prime p)] {a : ℤ_[p]ˣ}
  (ha :
    ∀ (n : ℕ),
      Subgroup.zpowers ((PadicMeasure.unitsToZModPow p n) a) = ⊤)
  (hreg :
    PadicMeasure.dirac p a - 1 ∈
      nonZeroDivisors (PadicMeasure p ℤ_[p]ˣ))
  (q : PadicMeasure.QuotientField p) :
  PadicMeasure.IsPseudoMeasure p q ↔
    ∃ μ,
      q =
        IsLocalization.mk' (PadicMeasure.QuotientField p) μ
          ⟨PadicMeasure.dirac p a - 1, hreg⟩

theorem PadicMeasure.isPseudoMeasure_iff_exists
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {a : ℤ_[p]ˣ}
  (ha :
    ∀ (n : ℕ),
      Subgroup.zpowers
          ((PadicMeasure.unitsToZModPow p
              n)
            a) =
        ⊤)
  (hreg :
    PadicMeasure.dirac p a - 1 ∈
      nonZeroDivisors
        (PadicMeasure p ℤ_[p]ˣ))
  (q : PadicMeasure.QuotientField p) :
  PadicMeasure.IsPseudoMeasure p q ↔
    ∃ μ,
      q =
        IsLocalization.mk'
          (PadicMeasure.QuotientField p) μ
          ⟨PadicMeasure.dirac p a - 1,
            hreg⟩

Every pseudo-measure has the shape `μ/([a]−[1])`. Source: RJW TeX lines 1284–1285
("Note moreover that *all* pseudo-measures have this shape").

Proof for Proposition 3.6.6

uses 0

As p is odd, (\Z/p^n\Z)^\times is cyclic generated by \bar a = a \bmod p^n, so I((\Z/p^n\Z)^\times) = ([\bar a]-[\bar 1])\,\OL[(\Z/p^n\Z)^\times]. Passing to the limit, I(\Zpx) = ([a]-[1])\Lam(\Zpx). Hence for any g \in \Zpx we may write [g]-[1] = \nu([a]-[1]) with \nu \in \Lam(\Zpx), and then ([g]-[1])\mu' = \nu([a]-[1])\mu' = \nu \cdot \mu \in \Lam(\Zpx), so \mu' is a pseudo-measure. Conversely, if \mu' is a pseudo-measure then by definition \mu := ([a]-[1])\mu' is a measure, and \mu' = \mu/([a]-[1]).