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

8.3. The Lambda-adic family🔗

We can now assemble the family. The constant term is interpolated by \zeta_p (after a shift in the variable), and each non-constant coefficient by a finite sum of Dirac measures.

Theorem8.3.1
Statement uses 5
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 exists a power series \mathbf{E}(z) = \sum_{n \geq 0} A_n\, q^n \in Q(\Zpx)[\![q]\!] with coefficients in the fraction ring Q(\Zpx) of the Iwasawa algebra, such that:

  • the constant term A_0 is a pseudo-measure and A_n \in \Lam(\Zpx) is a genuine measure for all n \geq 1;

  • for every even k \geq 4, integrating coefficient-by-coefficient against x^{k-1} recovers the p-stabilised Eisenstein series: \int_{\Zpx} x^{k-1} \cdot \mathbf{E}(z) := \sum_{n \geq 0} \Big( \int_{\Zpx} x^{k-1} \cdot A_n \Big) q^n = E_k^{(p)}(z).

This rests on Definition 8.2.1, Proposition 8.1.2, Definition 4.3.2, Theorem 5.1.1 and Definition 3.6.1.

Erratum (errata.md #11). As stated in the notes, "(a) A_0 is a pseudo-measure" fails for the notes' own Definition 3.34: the x-twist moves the pole of \zeta_p from the trivial character to the character x^{-1}, so ([g]-[1])\,x\zeta_p \notin \Lam for g \neq 1. The formalisation realises the x-twist as a ring automorphism unitsTwist of \Lam(\Zpx) (extended to Q(\Zpx)), defines A_0 = x\zeta_p/2 as twistedZetaHalf, and proves the corrected claim (g[g]-[1])A_0 \in \Lam(\Zpx) for all g (twistedZetaHalf_isTwistedPseudoMeasure), together with the moment interpolation in the same witness encoding as \zeta_p's (twistedZetaHalf_moments). The full coefficientwise display is eisensteinFamily_interpolation, whose target coefficients tie to the complex E_k^{(p)} through stabilisedCoeff and hasSum_stabilisedEisenstein; evenness of k enters only on that complex side.

Lean code for Theorem8.3.1●6 declarations
  • defdefined in PadicLFunctions/EisensteinFamily.lean
    complete
    def PadicLFunctions.eisensteinFamily (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) : PowerSeries (PadicMeasure.QuotientField p)
    def PadicLFunctions.eisensteinFamily (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) :
  PowerSeries
    (PadicMeasure.QuotientField p)
    R8 (RJW TeX 2399–2400): the Λ-adic Eisenstein family
`𝐄 = Σ_{n≥0} A_n qⁿ ∈ Q(ℤ_p^×)⟦q⟧`: constant coefficient `A₀ = x·ζ_p/2`,
higher coefficients the divisor-sum measures `A_n`.
  • theoremdefined in PadicLFunctions/EisensteinFamily.lean
    complete
    theorem PadicLFunctions.eisensteinFamily_interpolation (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {k : ℕ} (hk : 4 ≤ k) :
  (∀ (b : ℤ_[p]ˣ) (ν : PadicMeasure p ℤ_[p]ˣ),
      (algebraMap (PadicMeasure p ℤ_[p]ˣ)
                (PadicMeasure.QuotientField p))
              (↑b • PadicMeasure.dirac p b - 1) *
            PowerSeries.constantCoeff
              (PadicLFunctions.eisensteinFamily p hp2) =
          (algebraMap (PadicMeasure p ℤ_[p]ˣ)
              (PadicMeasure.QuotientField p))
            ν →
        ↑(ν (PadicMeasure.unitsPowCM p (k - 1))) =
          (↑↑b ^ k - 1) * ↑(PadicLFunctions.stabilisedCoeff p k 0)) ∧
    ∀ (n : ℕ),
      n ≠ 0 →
        (PowerSeries.coeff n) (PadicLFunctions.eisensteinFamily p hp2) =
            (algebraMap (PadicMeasure p ℤ_[p]ˣ)
                (PadicMeasure.QuotientField p))
              (PadicLFunctions.divisorMeasure p n) ∧
          ↑((PadicLFunctions.divisorMeasure p n)
                (PadicMeasure.unitsPowCM p (k - 1))) =
            ↑(PadicLFunctions.stabilisedCoeff p k n)
    theorem PadicLFunctions.eisensteinFamily_interpolation
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) {k : ℕ} (hk : 4 ≤ k) :
  (∀ (b : ℤ_[p]ˣ)
      (ν : PadicMeasure p ℤ_[p]ˣ),
      (algebraMap (PadicMeasure p ℤ_[p]ˣ)
                (PadicMeasure.QuotientField
                  p))
              (↑b •
                  PadicMeasure.dirac p b -
                1) *
            PowerSeries.constantCoeff
              (PadicLFunctions.eisensteinFamily
                p hp2) =
          (algebraMap
              (PadicMeasure p ℤ_[p]ˣ)
              (PadicMeasure.QuotientField
                p))
            ν →
        ↑(ν
              (PadicMeasure.unitsPowCM p
                (k - 1))) =
          (↑↑b ^ k - 1) *
            ↑(PadicLFunctions.stabilisedCoeff
                p k 0)) ∧
    ∀ (n : ℕ),
      n ≠ 0 →
        (PowerSeries.coeff n)
              (PadicLFunctions.eisensteinFamily
                p hp2) =
            (algebraMap
                (PadicMeasure p ℤ_[p]ˣ)
                (PadicMeasure.QuotientField
                  p))
              (PadicLFunctions.divisorMeasure
                p n) ∧
          ↑((PadicLFunctions.divisorMeasure
                  p n)
                (PadicMeasure.unitsPowCM p
                  (k - 1))) =
            ↑(PadicLFunctions.stabilisedCoeff
                p k n)
    **RJW §8 Theorem (TeX 2399–2407), p-adic half**: the coefficientwise
interpolation `∫_{ℤ_p^×} x^{k−1}·𝐄 = E_k^{(p)}` for `k ≥ 4` — the `n`-th
moment of the family equals the `n`-th coefficient `stabilisedCoeff p k n`
of the p-stabilised Eisenstein series, with the constant coefficient in the
pseudo-measure witness encoding. (Evenness of `k` is not needed on the
p-adic side; it enters only in the complex identification of
`stabilisedCoeff` with the q-expansion of `E_k^{(p)}`, which is
`hasSum_stabilisedEisenstein` in `EisensteinComplex.lean`.)
  • defdefined in PadicLFunctions/EisensteinFamily.lean
    complete
    def PadicLFunctions.unitsTwist (p : ℕ) [hp : Fact (Nat.Prime p)] :
  PadicMeasure p ℤ_[p]ˣ ≃+* PadicMeasure p ℤ_[p]ˣ
    def PadicLFunctions.unitsTwist (p : ℕ)
  [hp : Fact (Nat.Prime p)] :
  PadicMeasure p ℤ_[p]ˣ ≃+*
    PadicMeasure p ℤ_[p]ˣ
    R8 (replan R8.2): the x-twist `τ : Λ(ℤ_p^×) → Λ(ℤ_p^×)`,
`(τμ)(f) = μ(x·f)` — on Diracs `[g] ↦ g·[g]` — as a ring automorphism of
the convolution algebra. Multiplicativity is a moments check
(`units_mul_apply_unitsPowCM` + the zero-divisor lemma); the inverse is the
twist by `x⁻¹`.
  • defdefined in PadicLFunctions/EisensteinFamily.lean
    complete
    def PadicLFunctions.twistedZetaHalf (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) : PadicMeasure.QuotientField p
    def PadicLFunctions.twistedZetaHalf (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) :
  PadicMeasure.QuotientField p
    R8 (RJW TeX 2410): the constant coefficient `A₀ = x·ζ_p/2` of the
Eisenstein family — the x-twist of the Kubota–Leopoldt pseudo-measure,
halved (`2` is a unit of `ℤ_p` for odd `p`).
  • theoremdefined in PadicLFunctions/EisensteinFamily.lean
    complete
    theorem PadicLFunctions.twistedZetaHalf_isTwistedPseudoMeasure (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) (g : ℤ_[p]ˣ) :
  ∃ ν,
    (algebraMap (PadicMeasure p ℤ_[p]ˣ) (PadicMeasure.QuotientField p))
          (↑g • PadicMeasure.dirac p g - 1) *
        PadicLFunctions.twistedZetaHalf p hp2 =
      (algebraMap (PadicMeasure p ℤ_[p]ˣ)
          (PadicMeasure.QuotientField p))
        ν
    theorem PadicLFunctions.twistedZetaHalf_isTwistedPseudoMeasure
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) (g : ℤ_[p]ˣ) :
  ∃ ν,
    (algebraMap (PadicMeasure p ℤ_[p]ˣ)
            (PadicMeasure.QuotientField
              p))
          (↑g • PadicMeasure.dirac p g -
            1) *
        PadicLFunctions.twistedZetaHalf p
          hp2 =
      (algebraMap (PadicMeasure p ℤ_[p]ˣ)
          (PadicMeasure.QuotientField p))
        ν
    R8 (replan R8.1, **erratum #11**): the corrected form of RJW TeX 2403(a).
The notes claim `A₀ = x·ζ_p/2` is a pseudo-measure; with Def 3.34 this is
false (the pole of `x·ζ_p` sits at the character `x⁻¹`, not at the trivial
character — see `.mathlib-quality/errata.md` #11). What holds, and what the
family needs, is the x-twisted analogue: `(g·[g] − [1])·A₀ ∈ Λ(ℤ_p^×)` for
every `g`.
  • theoremdefined in PadicLFunctions/EisensteinFamily.lean
    complete
    theorem PadicLFunctions.twistedZetaHalf_moments (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) (b : ℤ_[p]ˣ) {k : ℕ}
  (hk : 4 ≤ k) (ν : PadicMeasure p ℤ_[p]ˣ)
  (hν :
    (algebraMap (PadicMeasure p ℤ_[p]ˣ) (PadicMeasure.QuotientField p))
          (↑b • PadicMeasure.dirac p b - 1) *
        PadicLFunctions.twistedZetaHalf p hp2 =
      (algebraMap (PadicMeasure p ℤ_[p]ˣ)
          (PadicMeasure.QuotientField p))
        ν) :
  ↑(ν (PadicMeasure.unitsPowCM p (k - 1))) =
    (↑↑b ^ k - 1) * (1 - ↑p ^ (k - 1)) * ↑(zetaNeg (k - 1)) / 2
    theorem PadicLFunctions.twistedZetaHalf_moments
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) (b : ℤ_[p]ˣ) {k : ℕ}
  (hk : 4 ≤ k) (ν : PadicMeasure p ℤ_[p]ˣ)
  (hν :
    (algebraMap (PadicMeasure p ℤ_[p]ˣ)
            (PadicMeasure.QuotientField
              p))
          (↑b • PadicMeasure.dirac p b -
            1) *
        PadicLFunctions.twistedZetaHalf p
          hp2 =
      (algebraMap (PadicMeasure p ℤ_[p]ˣ)
          (PadicMeasure.QuotientField p))
        ν) :
  ↑(ν
        (PadicMeasure.unitsPowCM p
          (k - 1))) =
    (↑↑b ^ k - 1) * (1 - ↑p ^ (k - 1)) *
        ↑(zetaNeg (k - 1)) /
      2
    R8 (RJW TeX 2412 "A₀ interpolates the constant term"): the moments of
`A₀ = x·ζ_p/2` in the witness encoding — any witness `ν` of
`(b·[b]−[1])·A₀ ∈ Λ` has
`∫x^{k−1}·ν = (b^k−1)·(1−p^{k−1})·ζ(1−k)/2`, the constant coefficient of
`E_k^{(p)}` scaled by the twisted-denominator factor `b^k−1`.
Proof for Theorem 8.3.1
uses 0

Define the coefficient measures explicitly. For the non-constant terms set A_n = \sum_{\substack{0 < d \mid n \\ p \nmid d}} \delta_d \in \Lam(\Zpx) \qquad (n \geq 1), a finite sum of Dirac measures at units, hence a genuine measure. For the constant term take the pseudo-measure A_0 = x\,\zeta_p / 2, i.e. \zeta_p shifted by one in the variable (in the opposite direction to the shift used when constructing \zeta_p), so that integrating x^{k-1} against A_0 is integrating x^{k} against \zeta_p/2.

For the interpolation, the non-constant coefficients follow from Proposition 8.1.2: \int_{\Zpx} x^{k-1} \cdot A_n = \sum_{\substack{0 < d \mid n \\ p \nmid d}} \int_{\Zpx} x^{k-1} \cdot \delta_d = \sum_{\substack{0 < d \mid n \\ p \nmid d}} d^{k-1} = \sigma_{k-1}^{p}(n), which is exactly the q^n-coefficient of E_k^{(p)}. For the constant term, the interpolation property of \zeta_p gives \int_{\Zpx} x^{k-1} \cdot A_0 = \tfrac{1}{2}\int_{\Zpx} x^{k} \cdot \zeta_p = \tfrac{1}{2}(1 - p^{k-1})\zeta(1-k), matching the constant term of E_k^{(p)} computed in Definition 8.2.1. Coefficient-by-coefficient the two power series agree, proving the claim.