8.2. p-stabilisation🔗

The way around the obstruction is classical: pass to the p-stabilisation, which removes the divisors of n that are divisible by p and lowers the level to \Gamma_0(p).

Definition8.2.1

uses 1used by 1✓L∃∀N

The p-stabilisation of E_k is E_k^{(p)}(z) := E_k(z) - p^{k-1} E_k(pz). Its q-expansion is E_k^{(p)}(z) = \frac{(1 - p^{k-1})\,\zeta(1-k)}{2} + \sum_{n \geq 1} \sigma_{k-1}^{p}(n)\, q^n, \qquad \sigma_{k-1}^{p}(n) = \sum_{\substack{0 < d \mid n \\ p \nmid d}} d^{k-1}. It is a modular form of weight k and level \Gamma_0(p) = \set{\left(\begin{smallmatrix} a & b \\ c & d \end{smallmatrix}\right) \in \mathrm{SL}_2(\Z) : p \mid c}. This depends on Definition 8.1.1.

Fully formalised: the rational coefficient sequence is stabilisedCoeff, the q-expansion is the convergence statement hasSum_stabilisedEisenstein, and the \Gamma_0(p)-modularity — the "Note" of the source, given there without proof — is the genuine ModularForm ((Gamma0 p).map (mapGL ℝ)) k stabilisedEisenstein, built on the level-raising operator \iota_p f = f(p\,\cdot) of the LeanModularForms strong-multiplicity-one project (Miyake §4.6, Lemma 4.6.1).

Lean code for Definition8.2.1●5 declarations

defdefined in PadicLFunctions/EisensteinFamily.lean

complete

def PadicLFunctions.sigmaP (p k n : ℕ) : ℕ

def PadicLFunctions.sigmaP (p k n : ℕ) : ℕ

R8: the prime-to-`p` divisor power sum
`σ^p_k(n) = Σ_{0<d∣n, p∤d} d^k` (RJW TeX 2393).

defdefined in PadicLFunctions/EisensteinFamily.lean

complete

def PadicLFunctions.stabilisedCoeff (p k : ℕ) : ℕ → ℚ

def PadicLFunctions.stabilisedCoeff
  (p k : ℕ) : ℕ → ℚ

R8: the rational coefficient sequence of the p-stabilised Eisenstein
series `E_k^{(p)}` (RJW TeX 2391): constant term `(1−p^{k−1})·ζ(1−k)/2`,
`n`-th term `σ^p_{k−1}(n)`. This is the pivot between the p-adic family
(`eisensteinFamily_interpolation`) and the complex q-expansion
(`hasSum_stabilisedEisenstein` in `EisensteinComplex.lean`).

theoremdefined in PadicLFunctions/EisensteinComplex.lean

complete

theorem PadicLFunctions.hasSum_stabilisedEisenstein (p : ℕ)
  [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 4 ≤ k) (hk2 : Even k)
  (z : UpperHalfPlane) :
  HasSum
    (fun n ↦
      ↑(PadicLFunctions.stabilisedCoeff p k n) *
        Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n)
    (PadicLFunctions.rjwEisenstein ⋯ z -
      ↑p ^ (k - 1) *
        PadicLFunctions.rjwEisenstein ⋯ (PadicLFunctions.pScale p z))

theorem PadicLFunctions.hasSum_stabilisedEisenstein
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {k : ℕ} (hk : 4 ≤ k) (hk2 : Even k)
  (z : UpperHalfPlane) :
  HasSum
    (fun n ↦
      ↑(PadicLFunctions.stabilisedCoeff p
            k n) *
        Complex.exp
            (2 * ↑Real.pi * Complex.I *
              ↑z) ^
          n)
    (PadicLFunctions.rjwEisenstein ⋯ z -
      ↑p ^ (k - 1) *
        PadicLFunctions.rjwEisenstein ⋯
          (PadicLFunctions.pScale p z))

**RJW TeX 2387–2393** (the p-stabilisation and its q-expansion): for even
`k ≥ 4` and every `z ∈ ℍ`, the series `Σ_n stabilisedCoeff(k,n)·qⁿ` with
`q = e^{2πiz}` sums to `E_k^{(p)}(z) = E_k(z) − p^{k−1}E_k(pz)` (in RJW's
normalisation). The coefficients: constant term `(1−p^{k−1})ζ(1−k)/2`,
`n`-th term `σ^p_{k−1}(n)`.

defdefined in PadicLFunctions/EisensteinComplex.lean

complete

def PadicLFunctions.stabilisedEisenstein (p : ℕ) [hp : Fact (Nat.Prime p)]
  {k : ℕ} (hk : 3 ≤ k) :
  ModularForm
    (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
      (CongruenceSubgroup.Gamma0 p))
    ↑k

def PadicLFunctions.stabilisedEisenstein
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {k : ℕ} (hk : 3 ≤ k) :
  ModularForm
    (Subgroup.map
      (Matrix.SpecialLinearGroup.mapGL ℝ)
      (CongruenceSubgroup.Gamma0 p))
    ↑k

The `p`-stabilised Eisenstein series `E_k^{(p)}(z) = E_k(z) − p^{k−1}E_k(pz)` as a
genuine modular form of weight `k` and level `Γ₀(p)` (RJW TeX 2394; Miyake §4.6
Lemma 4.6.1 for the underlying level-raising operator).

Built from `stabilisedDiff` (the same difference at level `Γ₁(p·1)`) by promoting the
slash-invariance from `Γ₁(p·1)` to the larger group `Γ₀(p)` via
`stabilisedDiff_slash_mapGL`; holomorphy is inherited and boundedness at the cusps of
`Γ₀(p)` transfers from `Γ₁(p·1)` because both groups are arithmetic, hence share the
`SL(2, ℤ)`-cusps (`Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z`). The convention
matches `rjwEisenstein` only up to the `ζ(1−k)/2` factor — see
`stabilisedEisenstein_smul_apply`.

theoremdefined in PadicLFunctions/EisensteinComplex.lean

complete

theorem PadicLFunctions.stabilisedEisenstein_apply (p : ℕ)
  [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 3 ≤ k) (z : UpperHalfPlane) :
  (PadicLFunctions.stabilisedEisenstein p hk) z =
    (ModularForm.E hk) z -
      ↑p ^ (k - 1) * (ModularForm.E hk) (PadicLFunctions.pScale p z)

theorem PadicLFunctions.stabilisedEisenstein_apply
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {k : ℕ} (hk : 3 ≤ k)
  (z : UpperHalfPlane) :
  (PadicLFunctions.stabilisedEisenstein p
        hk)
      z =
    (ModularForm.E hk) z -
      ↑p ^ (k - 1) *
        (ModularForm.E hk)
          (PadicLFunctions.pScale p z)

**RJW TeX 2394** (pointwise formula): the `Γ₀(p)`-modular form `stabilisedEisenstein`
is the `p`-stabilisation `E_k(z) − p^{k−1}E_k(pz)`, where `E_k` is mathlib's normalised
`ModularForm.E` and `pz = pScale p z`.

Proof for Definition 8.2.1

uses 0

Substituting q \mapsto q^p (i.e. z \mapsto pz) into the q-expansion of E_k and forming E_k - p^{k-1} E_k(p\,\cdot) multiplies the n-th coefficient of the second copy by p^{k-1}. On the constant term this produces the Euler factor 1 - p^{k-1}. On the coefficient of q^n it subtracts p^{k-1}\sigma_{k-1}(n/p) (when p \mid n) from \sigma_{k-1}(n); since p^{k-1} d^{k-1} = (pd)^{k-1}, this cancels exactly the divisors of n that are divisible by p, leaving the p-restricted divisor sum \sigma_{k-1}^{p}(n). The constant term is now the Euler-factor-twisted value (1 - p^{k-1})\zeta(1-k)/2 — precisely the quantity interpolated by \zeta_p.

The crucial gain is that \sigma_{k-1}^{p}(n) involves only divisors coprime to p, so it is built entirely from the well-behaved power maps k \mapsto d^{k} with p \nmid d, which Dirac measures interpolate.