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

4.2. Restriction to the units🔗

We now restrict \mua from \Zp to \Zpx, so as to obtain a measure on the units. The restriction operator is \Res_{\Zpx} = 1 - \varphi\circ\psi, where \varphi and \psi are the operators on measures (and on power series, via the Mahler transform) introduced in the toolbox; on power series \varphi acts by F \mapsto F((1+T)^p - 1). We first record a key invariance of \mua.

Lemma4.2.1
uses 0used by 1✓L∃∀N

The measure \mua satisfies \psi(\mua) = \mua; equivalently \psi(\Fa) = \Fa.

Lean code for Lemma4.2.1●1 theorem
  • theoremdefined in PadicLFunctions/KubotaLeopoldt/MuA.lean
    complete
    theorem PadicMeasure.psi_muA (p : ℕ) [hp : Fact (Nat.Prime p)] {a : ℕ}
  (hpa : ¬p ∣ a) :
  PadicMeasure.psi p (PadicMeasure.muA p a) = PadicMeasure.muA p a
    theorem PadicMeasure.psi_muA (p : ℕ)
  [hp : Fact (Nat.Prime p)] {a : ℕ}
  (hpa : ¬p ∣ a) :
  PadicMeasure.psi p
      (PadicMeasure.muA p a) =
    PadicMeasure.muA p a
    **RJW Lem. 4.7 (`LemmaPsiInvariant`)**: `ψ(μ_a) = μ_a`.

The source's proof runs through the roots-of-unity formula for `φ∘ψ` (TeX
1517–1524); here the same content is the elementary computation
`([a]−1)·ψμ_a = ψ(([ap]−1)·μ_a) = ψ((Σ_{j<p}[aj])·([a]−1)·μ_a) = ([a]−1)·μ_a`,
using the projection formula and the finite Dirac identities.
Proof for Lemma 4.2.1
uses 0

Work on Mahler transforms, where it suffices to show \psi(\Fa) = \Fa. Writing \sigmaa for the toolbox operator F(T)\mapsto F((1+T)^a - 1), one has \Fa(T) = \tfrac{1}{T} - a\cdot\sigmaa(\tfrac{1}{T}). Since \psi commutes with \sigmaa, it is enough to prove \psi(\tfrac1T) = \tfrac1T. The defining relation reads (\varphi\circ\psi)(F)(T) = \tfrac1p\sum_{\xi\in\mu_p} F((1+T)\xi - 1). Applying it to F = \tfrac1T and using the factorisation \prod_{\xi\in\mu_p}\bigl((1+T)\xi - 1\bigr) = (1+T)^p - 1, a partial-fraction expansion of \tfrac1p\sum_\xi \tfrac{1}{(1+T)\xi-1} collapses to a single term: (\varphi\circ\psi)\!\left(\tfrac1T\right) = \frac1p\sum_{\xi\in\mu_p}\frac{1}{(1+T)\xi - 1} = \frac{1}{(1+T)^p - 1} = \varphi\!\left(\tfrac1T\right).$$ As \varphi is injective, this forces \psi(\tfrac1T) = \tfrac1T, and hence \psi(\Fa) = \Fa, i.e. \psi(\mua) = \mua.

Proposition4.2.2
uses 0
Used by 2
Reverse dependency previews
Preview
Definition 4.3.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

For all k \ge 0, \int_{\Zpx} x^k \cdot \mua = (-1)^k\,(1 - p^k)\,(1 - a^{k+1})\,\zeta(-k).$$ In other words, restricting from \Zp to \Zpx removes the Euler factor at p.

Lean code for Proposition4.2.2●1 theorem
  • theoremdefined in PadicLFunctions/KubotaLeopoldt/MuA.lean
    complete
    theorem PadicMeasure.res_units_muA_apply_powCM (p : ℕ) [hp : Fact (Nat.Prime p)]
  {a : ℕ} (hpa : ¬p ∣ a) (k : ℕ) :
  ↑((PadicMeasure.res p ⋯ (PadicMeasure.muA p a))
        (PadicMeasure.powCM p k)) =
    (-1) ^ k * (1 - ↑p ^ k) * (1 - ↑a ^ (k + 1)) * ↑(zetaNeg k)
    theorem PadicMeasure.res_units_muA_apply_powCM
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {a : ℕ} (hpa : ¬p ∣ a) (k : ℕ) :
  ↑((PadicMeasure.res p ⋯
          (PadicMeasure.muA p a))
        (PadicMeasure.powCM p k)) =
    (-1) ^ k * (1 - ↑p ^ k) *
        (1 - ↑a ^ (k + 1)) *
      ↑(zetaNeg k)
    **RJW Prop. 4.8 (`PropInterpolation1`)**: restricting to `ℤ_p^×` removes the
Euler factor at `p`:
`∫_{ℤ_p^×} x^k dμ_a = (−1)^k (1−p^k)(1−a^{k+1}) ζ(−k)`.
Proof for Proposition 4.2.2
Proof uses 2
Proof dependency previews
Preview
Proposition 4.1.5
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

Since \Res_{\Zpx} = 1 - \varphi\circ\psi, we have \int_{\Zpx} x^k\cdot\mua = \int_{\Zp} x^k\cdot(1-\varphi\circ\psi)\mua = \int_{\Zp} x^k\cdot(1-\varphi)\mua,$$ where the second equality uses \psi(\mua) = \mua from Lemma 4.2.1. The operator \varphi corresponds to \sigma_p, i.e. push-forward along multiplication by p, so \int_{\Zp} x^k\cdot\varphi\mua = p^k\int_{\Zp} x^k\cdot\mua; hence the right-hand side equals (1-p^k)\int_{\Zp} x^k\cdot\mua. Substituting the value of \int_{\Zp} x^k\cdot\mua from Proposition 4.1.5 gives the stated formula.