Eisenstein series weighted by a function of residues

For a level N, a weight k and a function W : (Fin 2 → ZMod N) → ℂ, the series ∑_{v ∈ ℤ²} W(v mod N) · (v₀ z + v₁)^(-k).

Mathlib's eisensteinSeries sums over the coprime pairs in one residue class. The Eisenstein series with character of Diamond–Shurman §4.5 are instead built from the sums G_k^{a}(z) = ∑_{v ≡ a mod N} (v₀ z + v₁)^(-k) over all pairs in a residue class, weighted by character values; every such combination is the series of this file for a suitable W (G_k^{a} itself is the indicator function of a). Allowing an arbitrary weight keeps the analytic input in one place.

For 3 ≤ k the series converges absolutely and locally uniformly, and slashing by γ ∈ SL(2, ℤ) only changes the weight, to a ↦ W (a ᵥ* γ⁻¹) (weightedEisensteinSeries_slash_apply). Hence the series is a modular form of level Γ(N) (weightedEisensteinSeriesMF); the character is then read off from the transformation of the weight under Γ₀(N).

Main definitions

• TauCeti.EisensteinSeries.weightedEisensteinSeries: the weighted series, as a function.
• TauCeti.EisensteinSeries.weightedEisensteinSeriesSIF: it is slash invariant of level Γ(N).
• TauCeti.EisensteinSeries.weightedEisensteinSeriesMF: for 3 ≤ k, a modular form of level Γ(N).

Main results

• TauCeti.EisensteinSeries.weightedEisensteinSeries_slash_apply: the slash action on the series.
• TauCeti.EisensteinSeries.weightedEisensteinSeries_eq_tsum_eisensteinSeries: the series in terms of Mathlib's coprime-pair eisensteinSeries, through the gammaSet decomposition by gcd and residue class.
• TauCeti.EisensteinSeries.weightedEisensteinSeries_smul, TauCeti.EisensteinSeries.weightedEisensteinSeries_add: linearity in the weight.

References

• F. Diamond and J. Shurman, A first course in modular forms, §4.2, §4.5.
• The uniform-convergence argument follows Mathlib's EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly (Chris Birkbeck and David Loeffler), while the holomorphy and boundedness arguments follow EisensteinSeries.eisensteinSeriesSIF_mdifferentiable and EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF (Chris Birkbeck), with the sum over a coprime residue class replaced by a sum over all pairs with bounded weights.

noncomputable def TauCeti.EisensteinSeries.weightedEisensteinSeries {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) (k : ℤ) (z : UpperHalfPlane) : ℂ

The Eisenstein series of weight k weighted by W : (Fin 2 → ZMod N) → ℂ: ∑' v : ℤ², W (v mod N) * (v 0 * z + v 1) ^ (-k).

Equations

• TauCeti.EisensteinSeries.weightedEisensteinSeries W k z = ∑' (v : Fin 2 → ℤ), W (Int.cast ∘ v) * EisensteinSeries.eisSummand k v z

theorem TauCeti.EisensteinSeries.weightedEisensteinSeries_def {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) (k : ℤ) (z : UpperHalfPlane) : weightedEisensteinSeries W k z = ∑' (v : Fin 2 → ℤ), W (Int.cast ∘ v) * EisensteinSeries.eisSummand k v z

theorem TauCeti.EisensteinSeries.weightedEisensteinSeries_smul {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) (k : ℤ) (c : ℂ) : weightedEisensteinSeries (c • W) k = c • weightedEisensteinSeries W k

The series is linear in the weight: scalar multiples.

theorem TauCeti.EisensteinSeries.intCast_comp_vecMul {N : ℕ} (v : Fin 2 → ℤ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : Int.cast ∘ Matrix.vecMul v ↑γ = Matrix.vecMul (Int.cast ∘ v) ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)

Reduction modulo N commutes with right multiplication by γ ∈ SL(2, ℤ).

theorem TauCeti.EisensteinSeries.weightedEisensteinSeries_slash_apply {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) (k : ℤ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map k γ (weightedEisensteinSeries W k) = weightedEisensteinSeries (fun (a : Fin 2 → ZMod N) => W (Matrix.vecMul a ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ⁻¹))) k

The slash action on a weighted Eisenstein series. Slashing by γ ∈ SL(2, ℤ) replaces the weight W by a ↦ W (a ᵥ* γ⁻¹).

noncomputable def TauCeti.EisensteinSeries.weightedEisensteinSeriesSIF {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) (k : ℤ) : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k

The weighted Eisenstein series as a slash invariant form of level Γ(N): an element of Γ(N) reduces to the identity modulo N, so it does not change the weight.

Equations

• TauCeti.EisensteinSeries.weightedEisensteinSeriesSIF W k = { toFun := TauCeti.EisensteinSeries.weightedEisensteinSeries W k, slash_action_eq' := ⋯ }

@[simp]

theorem TauCeti.EisensteinSeries.coe_weightedEisensteinSeriesSIF {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) (k : ℤ) : ⇑(weightedEisensteinSeriesSIF W k) = weightedEisensteinSeries W k

Analytic properties

theorem TauCeti.EisensteinSeries.summable_norm_weightedEisensteinSummand {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (z : UpperHalfPlane) : Summable fun (v : Fin 2 → ℤ) => ‖W (Int.cast ∘ v) * EisensteinSeries.eisSummand k v z‖

The weighted series is absolutely convergent for 3 ≤ k.

theorem TauCeti.EisensteinSeries.weightedEisensteinSeries_add {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (W' : (Fin 2 → ZMod N) → ℂ) : weightedEisensteinSeries (W + W') k = weightedEisensteinSeries W k + weightedEisensteinSeries W' k

The series is linear in the weight: sums.

theorem TauCeti.EisensteinSeries.weightedEisensteinSeries_tendstoLocallyUniformly {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) : TendstoLocallyUniformly (fun (s : Finset (Fin 2 → ℤ)) (x : UpperHalfPlane) => ∑ v ∈ s, W (Int.cast ∘ v) * EisensteinSeries.eisSummand k v x) (fun (x : UpperHalfPlane) => weightedEisensteinSeries W k x) Filter.atTop

The partial sums of the weighted series converge locally uniformly on ℍ.

theorem TauCeti.EisensteinSeries.weightedEisensteinSeries_mdifferentiable {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) : MDiff ⇑(weightedEisensteinSeriesSIF W k)

The weighted series is holomorphic on ℍ.

theorem TauCeti.EisensteinSeries.isBoundedAtImInfty_weightedEisensteinSeriesSIF {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k γ ⇑(weightedEisensteinSeriesSIF W k))

Every SL(2, ℤ)-translate of the weighted series is bounded at i∞.

theorem TauCeti.EisensteinSeries.weightedEisensteinSeries_eq_tsum_eisensteinSeries {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (z : UpperHalfPlane) : weightedEisensteinSeries W k z = ∑' (r : ℕ), (↑r ^ k)⁻¹ * ∑ a : Fin 2 → ZMod N, W (r • a) * eisensteinSeries a k z

The weighted series in terms of Mathlib's eisensteinSeries. Writing each nonzero pair as its gcd r times a coprime pair and sorting the coprime pairs by residue class, ∑_v W(v) (v₀ z + v₁)^(-k) = ∑_r r^(-k) ∑_a W(r a) eisensteinSeries a k z.

noncomputable def TauCeti.EisensteinSeries.weightedEisensteinSeriesMF {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k

The weighted Eisenstein series is a modular form of weight k ≥ 3 and level Γ(N).

Equations

• TauCeti.EisensteinSeries.weightedEisensteinSeriesMF W hk = { toSlashInvariantForm := TauCeti.EisensteinSeries.weightedEisensteinSeriesSIF W k, holo' := ⋯, bdd_at_cusps' := ⋯ }

@[simp]

theorem TauCeti.EisensteinSeries.coe_weightedEisensteinSeriesMF {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) : ⇑(weightedEisensteinSeriesMF W hk) = weightedEisensteinSeries W k

@[simp]

theorem TauCeti.EisensteinSeries.weightedEisensteinSeriesMF_zero {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) : weightedEisensteinSeriesMF 0 hk = 0

@[simp]

theorem TauCeti.EisensteinSeries.weightedEisensteinSeriesMF_add {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (W' : (Fin 2 → ZMod N) → ℂ) : weightedEisensteinSeriesMF (W + W') hk = weightedEisensteinSeriesMF W hk + weightedEisensteinSeriesMF W' hk

@[simp]

theorem TauCeti.EisensteinSeries.weightedEisensteinSeriesMF_smul {N : ℕ} (W : (Fin 2 → ZMod N) → ℂ) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (c : ℂ) : weightedEisensteinSeriesMF (c • W) hk = c • weightedEisensteinSeriesMF W hk