Normalized Eisenstein series with character

For a Dirichlet character psi modulo u and a primitive character phi modulo v, with the parity required in weight k, this file normalizes the character Eisenstein series so that its first Fourier coefficient is 1. Thus its positive Fourier coefficients are exactly the twisted divisor sums

sigma_(k-1)^(psi,phi)(n) = sum_(d | n) psi(n / d) phi(d) d^(k-1).

The raised series E_k^(psi,phi,t)(z) = E_k^(psi,phi)(t z) has coefficients supported on the multiples of t; at n = t m > 0, its coefficient is sigma_(k-1)^(psi,phi)(m). These are the canonical generators used for the Eisenstein subspace of a fixed nebentypus space.

The constant coefficient is intentionally left in terms of the raw lattice sum. Identifying it with a generalized Bernoulli number is a separate special-value theorem for Dirichlet L-series.

Main definitions

• TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMF: the series normalized to have first Fourier coefficient 1.
• TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMFRaise: its level raise by t.

References

• F. Diamond and J. Shurman, A first course in modular forms, Section 4.5, Theorem 4.5.1.
• T. Miyake, Modular forms, Section 7.1.

noncomputable def TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMF {u v N k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (huv : u * v ∣ N) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) ↑k

The character Eisenstein series scaled by the inverse of its expected first coefficient.

The scalar is the inverse of the first coefficient of charEisensteinSeriesMF; its Gauss-sum factor is nonzero when phi is primitive, in which case the parity condition implies that the result has first Fourier coefficient 1.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.EisensteinSeries.qExpansion_normalizedCharEisensteinSeriesMF_coeff {u v N k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (huv : u * v ∣ N) (hpar : psi (-1) * phi (-1) = (-1) ^ ↑k) (hphi : phi.IsPrimitive) {n : ℕ} (hn : n ≠ 0) : (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑(normalizedCharEisensteinSeriesMF psi phi hk huv)) = (DirichletCharacter.twistedDivisorSum (k - 1) psi phi) n

The positive Fourier coefficients of the normalized character Eisenstein series are the twisted divisor sums sigma_(k-1)^(psi,phi).

@[simp]

theorem TauCeti.EisensteinSeries.qExpansion_normalizedCharEisensteinSeriesMF_coeff_one {u v N k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (huv : u * v ∣ N) (hpar : psi (-1) * phi (-1) = (-1) ^ ↑k) (hphi : phi.IsPrimitive) : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑(normalizedCharEisensteinSeriesMF psi phi hk huv)) = 1

The normalized character Eisenstein series has first Fourier coefficient 1.

theorem TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMF_ne_zero {u v N k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (huv : u * v ∣ N) (hpar : psi (-1) * phi (-1) = (-1) ^ ↑k) (hphi : phi.IsPrimitive) : normalizedCharEisensteinSeriesMF psi phi hk huv ≠ 0

A normalized character Eisenstein series is nonzero.

theorem TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMF_mem_modFormCharSpace {u v N k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (huv : u * v ∣ N) : normalizedCharEisensteinSeriesMF psi phi hk huv ∈ modFormCharSpace (↑k) (MulChar.toUnitHom ((DirichletCharacter.changeLevel ⋯) psi * (DirichletCharacter.changeLevel ⋯) phi))

The normalized series has the same nebentypus as the raw character Eisenstein series.

noncomputable def TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMFRaise {u v N k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (t : ℕ) (hk : 3 ≤ ↑k) (htuv : t * (u * v) ∣ N) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) ↑k

The level raise by t of the character Eisenstein series scaled by the inverse of its expected first coefficient: E_k^(psi,phi,t) = V_t E_k^(psi,phi). Under the parity and primitivity hypotheses, its coefficient at index t is 1.

Equations

• TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMFRaise psi phi t hk htuv = TauCeti.ModularForm.levelRaise t ⋯ (TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMF psi phi hk ⋯)

@[simp]

theorem TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMFRaise_apply {u v N t k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (htuv : t * (u * v) ∣ N) (z : UpperHalfPlane) : (normalizedCharEisensteinSeriesMFRaise psi phi t hk htuv) z = (normalizedCharEisensteinSeriesMF psi phi hk ⋯) (scaleGL t • z)

The raised normalized character Eisenstein series is the base series evaluated at t z.

@[simp]

theorem TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMFRaise_one {u v N k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (huv : u * v ∣ N) : normalizedCharEisensteinSeriesMFRaise psi phi 1 hk ⋯ = ModularForm.ofLe ⋯ (normalizedCharEisensteinSeriesMF psi phi hk ⋯)

At t = 1, the raised normalized series is the base series restricted from level uv to level N.

@[simp]

theorem TauCeti.EisensteinSeries.qExpansion_normalizedCharEisensteinSeriesMFRaise {u v N t k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (htuv : t * (u * v) ∣ N) : UpperHalfPlane.qExpansion 1 ⇑(normalizedCharEisensteinSeriesMFRaise psi phi t hk htuv) = (PowerSeries.expand t ⋯) (UpperHalfPlane.qExpansion 1 ⇑(normalizedCharEisensteinSeriesMF psi phi hk ⋯))

The q-expansion of a raised normalized character Eisenstein series is obtained by substituting q ↦ q^t in the q-expansion of the base series.

theorem TauCeti.EisensteinSeries.isSupportedOnDvd_qExpansion_normalizedCharEisensteinSeriesMFRaise {u v N t k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (htuv : t * (u * v) ∣ N) : PowerSeries.IsSupportedOnDvd t (UpperHalfPlane.qExpansion 1 ⇑(normalizedCharEisensteinSeriesMFRaise psi phi t hk htuv))

The q-expansion of a raised normalized Eisenstein series is supported on the multiples of t.

theorem TauCeti.EisensteinSeries.qExpansion_normalizedCharEisensteinSeriesMFRaise_coeff {u v N t k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (htuv : t * (u * v) ∣ N) (hpar : psi (-1) * phi (-1) = (-1) ^ ↑k) (hphi : phi.IsPrimitive) {n : ℕ} (hn : n ≠ 0) : (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑(normalizedCharEisensteinSeriesMFRaise psi phi t hk htuv)) = if t ∣ n then (DirichletCharacter.twistedDivisorSum (k - 1) psi phi) (n / t) else 0

The Fourier coefficients of a raised normalized Eisenstein series are the twisted divisor sums on indices divisible by t, and zero on the other positive indices.

theorem TauCeti.EisensteinSeries.qExpansion_normalizedCharEisensteinSeriesMFRaise_coeff_self {u v N t k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (htuv : t * (u * v) ∣ N) (hpar : psi (-1) * phi (-1) = (-1) ^ ↑k) (hphi : phi.IsPrimitive) : (PowerSeries.coeff t) (UpperHalfPlane.qExpansion 1 ⇑(normalizedCharEisensteinSeriesMFRaise psi phi t hk htuv)) = 1

The first positive supported coefficient of a raised normalized Eisenstein series is 1.

theorem TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMFRaise_ne_zero {u v N t k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (htuv : t * (u * v) ∣ N) (hpar : psi (-1) * phi (-1) = (-1) ^ ↑k) (hphi : phi.IsPrimitive) : normalizedCharEisensteinSeriesMFRaise psi phi t hk htuv ≠ 0

A raised normalized character Eisenstein series is nonzero.

theorem TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMFRaise_mem_modFormCharSpace {u v N t k : ℕ} [NeZero N] (psi : DirichletCharacter ℂ u) (phi : DirichletCharacter ℂ v) (hk : 3 ≤ ↑k) (htuv : t * (u * v) ∣ N) : normalizedCharEisensteinSeriesMFRaise psi phi t hk htuv ∈ modFormCharSpace (↑k) (MulChar.toUnitHom ((DirichletCharacter.changeLevel ⋯) psi * (DirichletCharacter.changeLevel ⋯) phi))

The raised normalized Eisenstein series belongs to the target nebentypus space.