4. The Kubota-Leopoldt p-adic L-function🔗

Throughout, p is a fixed odd prime. The goal of this chapter is to construct the Kubota–Leopoldt p-adic L-function as a pseudo-measure on \Zpx interpolating the values (1-p^{k-1})\zeta(1-k) of the Riemann zeta function. The strategy is to start from an explicit \cC^\infty function, transport it to a power series via the substitution e^t = T+1, recognise that power series as the Mahler transform of a measure \mua on \Zp, restrict \mua to \Zpx to strip off the Euler factor at p, and finally rescale by an augmentation element to remove the auxiliary parameter a and produce a pseudo-measure.

The headline result of the chapter is the following.

Theorem4.1

Statement uses 3

Statement dependency previews

Preview

Definition 3.6.1

Loading preview

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

used by 0✓L∃∀N

There is a unique pseudo-measure \zetap on \Zpx such that, for all integers k > 0, \int_{\Zpx} x^k \cdot \zetap = (1-p^{k-1})\,\zeta(1-k).$$ This pseudo-measure is the Kubota–Leopoldt p-adic L-function. Existence is supplied by the explicit construction Definition 4.3.2 together with Proposition 4.3.3, and uniqueness rests on the Definition 3.6.1 rigidity of Proposition 4.3.3.

Lean code for Theorem4.1●1 theorem

theoremdefined in PadicLFunctions/KubotaLeopoldt/ZetaP.lean

complete

theorem PadicMeasure.kubotaLeopoldt (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) :
  ∃! q,
    PadicMeasure.IsPseudoMeasure p q ∧
      ∀ (b : ℤ_[p]ˣ) (k : ℕ),
        0 < k →
          ∀ (ν : PadicMeasure p ℤ_[p]ˣ),
            (algebraMap (PadicMeasure p ℤ_[p]ˣ)
                      (PadicMeasure.QuotientField p))
                    (PadicMeasure.dirac p b - 1) *
                  q =
                (algebraMap (PadicMeasure p ℤ_[p]ˣ)
                    (PadicMeasure.QuotientField p))
                  ν →
              ↑(ν (PadicMeasure.unitsPowCM p k)) =
                (↑↑b ^ k - 1) * (1 - ↑p ^ (k - 1)) * ↑(zetaNeg (k - 1))

theorem PadicMeasure.kubotaLeopoldt (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) :
  ∃! q,
    PadicMeasure.IsPseudoMeasure p q ∧
      ∀ (b : ℤ_[p]ˣ) (k : ℕ),
        0 < k →
          ∀ (ν : PadicMeasure p ℤ_[p]ˣ),
            (algebraMap
                      (PadicMeasure p
                        ℤ_[p]ˣ)
                      (PadicMeasure.QuotientField
                        p))
                    (PadicMeasure.dirac p
                        b -
                      1) *
                  q =
                (algebraMap
                    (PadicMeasure p
                      ℤ_[p]ˣ)
                    (PadicMeasure.QuotientField
                      p))
                  ν →
              ↑(ν
                    (PadicMeasure.unitsPowCM
                      p k)) =
                (↑↑b ^ k - 1) *
                    (1 - ↑p ^ (k - 1)) *
                  ↑(zetaNeg (k - 1))

**RJW Thm. 4.1 (`thm:kubota leopoldt theorem`)**: there is a unique pseudo-measure
`ζ_p` on `ℤ_p^×` with `∫_{ℤ_p^×} x^k ζ_p = (1−p^{k−1}) ζ(1−k)` for all `k > 0`
(moments encoded via the witnesses of `([b]−[1])·ζ_p`).

Proof for Theorem 4.1

Proof uses 3

Proof dependency previews

Preview

Definition 3.6.1

Loading preview

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

Existence is Proposition 4.3.3, which exhibits the pseudo-measure \zetap of Definition Definition 4.3.2 and verifies the interpolation formula. For uniqueness, suppose \zetap and \zetap' are two pseudo-measures satisfying the displayed formula, and set \lambda = \zetap - \zetap', a pseudo-measure with \int_{\Zpx} x^k \cdot \lambda = 0 for all k > 0. Fix a topological generator a of \Zpx and let \thetaa = [a]-[1]. By definition of a Definition 3.6.1 pseudo-measure, \thetaa\lambda is a genuine measure on \Zpx, and for k>0 its monomial integrals are \int_{\Zpx} x^k\cdot\thetaa\lambda = (a^k-1)\int_{\Zpx} x^k\cdot\lambda = 0. A measure on \Zpx is determined by the values \int_{\Zpx} x^k\cdot(-) for k > 0 (these recover all Mahler coefficients on the units), so \thetaa\lambda = 0. Since \thetaa is not a zero divisor in \Lam(\Zpx), we conclude \lambda = 0, i.e. \zetap = \zetap'.