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

8.1. Eisenstein series and their q-expansions🔗

Definition8.1.1
uses 1used by 1✓L∃∀N

For an even integer k \geq 4, the Eisenstein series of weight k is the holomorphic function on \uhp given by G_k(z) := \sum_{\substack{c,d \in \Z \\ (c,d) \neq (0,0)}} \frac{1}{(cz+d)^k}. It is a modular form of weight k for \mathrm{SL}_2(\Z), and may be viewed as a two-dimensional analogue of the zeta value \zeta(k). Its normalisation E_k(z) := \frac{(k-1)!}{2\,(2\pi i)^k}\, G_k(z) has the rational q-expansion E_k(z) = \frac{\zeta(1-k)}{2} + \sum_{n \geq 1} \sigma_{k-1}(n)\, q^n, \qquad \sigma_{k-1}(n) = \sum_{0 < d \mid n} d^{k-1}. The constant term is the special value Corollary 2.3.4 \zeta(1-k) = -B_k/k.

Mathlib already provides the level-1 Eisenstein series and its q-expansion (ModularForm.E, normalised with constant term 1, and EisensteinSeries.q_expansion_bernoulli giving E = 1 - (2k/B_k)\sum \sigma_{k-1}(n)q^n); the notes' normalisation is the rescale rjwEisenstein = (\zeta(1-k)/2)\cdot E, under which the n-th coefficient becomes exactly \sigma_{k-1}(n).

Lean code for Definition8.1.1●3 declarations
  • defdefined in Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean
    complete
    def ModularForm.E {k : ℕ} (hk : 3 ≤ k) :
  ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
    def ModularForm.E {k : ℕ} (hk : 3 ≤ k) :
  ModularForm
    (Matrix.SpecialLinearGroup.mapGL
        ℝ).range
    ↑k
    Normalised Eisenstein series of level 1 and weight `k`,
here they have been scaled by `1/2` since we sum over coprime pairs.
  • theoremdefined in Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean
    complete
    theorem EisensteinSeries.q_expansion_bernoulli {k : ℕ} (hk : 3 ≤ k)
  (hk2 : Even k) (z : UpperHalfPlane) :
  (ModularForm.E hk) z =
    1 -
      2 * ↑k / ↑(bernoulli k) *
        ∑' (n : ℕ+),
          ↑((ArithmeticFunction.sigma (k - 1)) ↑n) *
            Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑↑n
    theorem EisensteinSeries.q_expansion_bernoulli
  {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k)
  (z : UpperHalfPlane) :
  (ModularForm.E hk) z =
    1 -
      2 * ↑k / ↑(bernoulli k) *
        ∑' (n : ℕ+),
          ↑((ArithmeticFunction.sigma
                  (k - 1))
                ↑n) *
            Complex.exp
                (2 * ↑Real.pi *
                    Complex.I *
                  ↑z) ^
              ↑↑n
    The q-Expansion of normalised Eisenstein series of level one with `bernoulli` term.
  • defdefined in PadicLFunctions/EisensteinComplex.lean
    complete
    def PadicLFunctions.rjwEisenstein {k : ℕ} (hk : 3 ≤ k) : UpperHalfPlane → ℂ
    def PadicLFunctions.rjwEisenstein {k : ℕ}
  (hk : 3 ≤ k) : UpperHalfPlane → ℂ
    RJW's normalisation of the Eisenstein series (TeX 2371):
`E_k = ζ(1−k)/2 + Σ_{n≥1}σ_{k−1}(n)qⁿ`, i.e. `(ζ(1−k)/2)·E` for mathlib's
constant-term-1 normalised `ModularForm.E`.

The constant term \zeta(1-k)/2 is precisely the special value interpolated by \zeta_p. The shape of the q-expansion already tells us what is left to do: interpolate the divisor sums \sigma_{k-1}(n), which only requires interpolating the power maps k \mapsto d^{k}.

Proposition8.1.2
uses 1used by 1✓L∃∀N

Let d be an integer coprime to p. Then the Dirac measure \delta_d \in \Lam(\Zpx) at d, i.e. evaluation at d, interpolates the power map: for every k \in \Z, \int_{\Zpx} x^{k} \cdot \delta_d = d^{k}. This rests on Definition 3.3.3.

Formalised at natural exponents and directly in the summed form the family needs: divisorMeasure_moment evaluates the divisor-sum measure A_n = \sum_{p\nmid d\mid n}\delta_d against x^k to \sigma^p_k(n); the single-Dirac case is its n-prime instance, with unitOfNat_coe realising "viewing d as an element of \Zpx".

Lean code for Proposition8.1.2●2 theorems
  • theoremdefined in PadicLFunctions/EisensteinFamily.lean
    complete
    theorem PadicLFunctions.unitOfNat_coe (p : ℕ) [hp : Fact (Nat.Prime p)] {d : ℕ}
  (hd : ¬p ∣ d) : ↑(PadicLFunctions.unitOfNat p d) = ↑d
    theorem PadicLFunctions.unitOfNat_coe (p : ℕ)
  [hp : Fact (Nat.Prime p)] {d : ℕ}
  (hd : ¬p ∣ d) :
  ↑(PadicLFunctions.unitOfNat p d) = ↑d
  • theoremdefined in PadicLFunctions/EisensteinFamily.lean
    complete
    theorem PadicLFunctions.divisorMeasure_moment (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n k : ℕ) :
  (PadicLFunctions.divisorMeasure p n) (PadicMeasure.unitsPowCM p k) =
    ↑(PadicLFunctions.sigmaP p k n)
    theorem PadicLFunctions.divisorMeasure_moment
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n k : ℕ) :
  (PadicLFunctions.divisorMeasure p n)
      (PadicMeasure.unitsPowCM p k) =
    ↑(PadicLFunctions.sigmaP p k n)
    R8 (RJW TeX 2413): `∫_{ℤ_p^×} x^k · A_n = σ^p_k(n)` — the Dirac measures
evaluate, `∫ x^k δ_d = d^k`.
Proof for Proposition 8.1.2
uses 0

Because d is coprime to p it is a unit, hence a genuine point of \Zpx. The Dirac measure \delta_d is by definition the point mass at d, so integration against it is evaluation: \int_{\Zpx} f \cdot \delta_d = f(d) for every continuous f. Taking f to be the character x \mapsto x^{k} gives \int_{\Zpx} x^{k} \cdot \delta_d = d^{k}. The identity holds for every k \in \Z since x \mapsto x^k is a continuous (indeed locally analytic) function on \Zpx for all integer exponents, including negative ones — exactly the contrast with k \mapsto p^k, where no such point exists.

Proposition8.1.3
uses 1used by 0✓L∃∀N

The power map k \mapsto p^{k} cannot be p-adically interpolated by a measure on \Zpx: there is no p-adic measure Definition 3.2.2 \theta_p on \Zpx with \int_{\Zpx} x^{k} \cdot \theta_p = p^{k} for all k.

The Lean proof replaces the notes' sequential-limit gloss with a single finitary congruence level: with K = 1 + \varphi(p^2), the uniform Euler congruence x^K \equiv x \bmod p^2 on \Zpx forces |p^K - p| \le p^{-2}, which is absurd. Notably p = 2 is allowed.

Lean code for Proposition8.1.3●1 theorem
  • theoremdefined in PadicLFunctions/EisensteinFamily.lean
    complete
    theorem PadicLFunctions.noMeasure_interpolates_pPow (p : ℕ)
  [hp : Fact (Nat.Prime p)] :
  ¬∃ θ, ∀ (k : ℕ), 0 < k → θ (PadicMeasure.unitsPowCM p k) = ↑p ^ k
    theorem PadicLFunctions.noMeasure_interpolates_pPow
  (p : ℕ) [hp : Fact (Nat.Prime p)] :
  ¬∃ θ,
      ∀ (k : ℕ),
        0 < k →
          θ
              (PadicMeasure.unitsPowCM p
                k) =
            ↑p ^ k
    R8 (RJW TeX 2379–2383): the function `k ↦ p^k` can never be interpolated
by a measure on `ℤ_p^×`. Finitary route (replan note in ticket T804): if a
measure `θ` interpolated `k ↦ p^k`, then at the single congruence level
`p²` the exponents `K := 1 + φ(p²)` and `1` agree on `ℤ_p^×` modulo `p²`
(`units_pow_totient_sq_sub_self_mem`), so `‖x^K − x^1‖ ≤ p^{-2}` as a sup
norm; boundedness of `θ` (`norm_apply_le`) forces `‖p^K − p‖ ≤ p^{-2}`.
But `‖p^K − p‖ = ‖p‖·‖p^{K−1} − 1‖ = p^{-1}` (`K − 1 = φ(p²) ≥ 1`, so the
second factor has norm one by the ultrametric isoceles), and `p^{-1} ≤ p^{-2}`
is false. Notably `p = 2` is allowed (no `hp2` is used).
Proof for Proposition 8.1.3
uses 0

The obstruction is twofold. First, p \notin \Zpx, so there is no Dirac measure at p. More fundamentally, suppose such a \theta_p existed and pick a strictly increasing sequence of integers k_n converging p-adically to a limit k. Integration against a measure is continuous in the character, so p^{k_n} = \int_{\Zpx} x^{k_n} \cdot \theta_p \to \int_{\Zpx} x^{k} \cdot \theta_p = p^{k}. But \val_p(p^{k_n}) = k_n \to \infty, so p^{k_n} \to 0 in \Cp, forcing p^k = 0, a contradiction. The map k \mapsto p^k simply behaves too badly to be continuous.