feat(ModularForm): add eisensteinSeries G_k^v

Mathlib/Data/ZMod/Basic.lean

@@ -794,6 +794,16 @@ theorem coe_unitOfCoprime {n : ℕ} (x : ℕ) (h : Nat.Coprime x n) :
     (unitOfCoprime x h : ZMod n) = x :=
   rfl
 
+/-- Variant of `ZMod.unitOfCoprime`, sending a natural number `r` coprime to `N` to the unit
+of `ZMod N` it represents. -/
+def coprimeUnitMap (r : {r : ℕ // r.Coprime n}) : (ZMod n)ˣ :=
+  ZMod.unitOfCoprime r.1 r.2
+
+@[simp]
+theorem coe_coprimeUnitMap {n : ℕ} (r : {r : ℕ // r.Coprime n}) :
+    (coprimeUnitMap r : ZMod n) = r.1 :=
+  rfl
+
 set_option backward.isDefEq.respectTransparency false in
 theorem val_coe_unit_coprime {n : ℕ} (u : (ZMod n)ˣ) : Nat.Coprime (u : ZMod n).val n := by
   rcases n with - | n

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.NumberTheory.ModularForms.Basic
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
+public import Mathlib.NumberTheory.LSeries.ZMod
 
 /-!
 # Eisenstein series are Modular Forms
@@ -40,6 +41,9 @@ def eisensteinSeriesMF {k : ℤ} {N : ℕ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2
     rw [OnePoint.isBoundedAt_iff_forall_SL2Z hc]
     exact fun γ hγ ↦ isBoundedAtImInfty_eisensteinSeriesSIF a hk γ
 
+lemma eisensteinSeriesMF_apply {k : ℤ} {N : ℕ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) :
+  eisensteinSeriesMF hk a = eisensteinSeries a k := rfl
+
 @[deprecated (since := "2026-02-10")] noncomputable alias eisensteinSeries_MF := eisensteinSeriesMF
 
 /-- Normalised Eisenstein series of level 1 and weight `k`,
@@ -54,3 +58,111 @@ abbrev E₄ : ModularForm 𝒮ℒ 4 := E (by norm_num : 3 ≤ 4)
 abbrev E₆ : ModularForm 𝒮ℒ 6 := E (by norm_num : 3 ≤ 6)
 
 end ModularForm
+
+section G_eq_sum_E
+
+open UpperHalfPlane EisensteinSeries
+
+variable {N : ℕ} {r : ℕ} (a : Fin 2 → ZMod N)
+
+/-- The modified zeta function `ζ₊ⁿ(k)`, i.e. the sum of `m ^ (-k)` over the positive integers
+`m ≡ n (mod N)`, is the value at `k` of the `L`-function of the indicator function of the
+residue class `n`. -/
+lemma tsum_zpow_eq_LFunction [NeZero N] (n : (ZMod N)ˣ) {k : ℤ} (hk : 1 < k) :
+    ∑' m : {m : ℕ // 0 < m ∧ (m : ZMod N) = n}, (m : ℂ) ^ (-k) =
+      ZMod.LFunction (Pi.single n.val 1) k := by
+  rw [ZMod.LFunction_eq_LSeries _ (mod_cast hk)]
+  calc
+    _ = ∑' m : {m : ℕ // 0 < m ∧ (m : ZMod N) = n},
+        LSeries.term (fun j : ℕ ↦ (Pi.single n.val 1 : ZMod N → ℂ) (j : ZMod N)) k m.1 := by
+      refine tsum_congr fun m ↦ ?_
+      simp [LSeries.term_of_ne_zero m.2.1.ne', m.2.2]
+    _ = LSeries (fun j : ℕ ↦ (Pi.single n.val 1 : ZMod N → ℂ) (j : ZMod N)) k := by
+      refine Function.Injective.tsum_eq (fun _ _ h ↦ Subtype.ext h) fun b hb ↦ ?_
+      rcases Nat.eq_zero_or_pos b with rfl | hb0
+      · simp at hb
+      · by_contra hbn
+        have hbn' : (b : ZMod N) ≠ (n : ZMod N) := fun hc ↦ hbn ⟨⟨b, hb0, hc⟩, rfl⟩
+        exact hb (by simp [LSeries.term_of_ne_zero hb0.ne', Pi.single_eq_of_ne hbn'])
+
+/-- The sum of `eisSummand` over `gammaSet N r a` for `r` coprime to `N` is `r ^ (-k)` times
+an Eisenstein series with congruence condition `r⁻¹ • a`. -/
+lemma tsum_gammaSet_eisSummand_of_coprime {k : ℤ} (hk : k ≠ 0) (z : ℍ) (h : r.Coprime N) :
+    ∑' v : gammaSet N r a, eisSummand k v z =
+      (r : ℂ) ^ (-k) * eisensteinSeries ((ZMod.unitOfCoprime r h)⁻¹ • a) k z := by
+  rcases Nat.eq_zero_or_pos r with rfl | hr
+  · have hN : N = 1 := N.coprime_zero_left.mp h
+    subst hN
+    have h0 : gammaSet 1 0 a = {0} := by
+      ext
+      simp [gammaSet_one_eq, Int.gcd_eq_zero_iff, funext_iff]
+    rw [h0, tsum_singleton 0 (eisSummand k · z)]
+    simp [eisSummand, _root_.zero_zpow _ (neg_ne_zero.mpr hk)]
+  · have : NeZero r := ⟨hr.ne'⟩
+    calc
+      _ = ∑' v : gammaSet N r a, (r : ℂ) ^ (-k) * eisSummand k (divIntMap r v) z := by
+        congr! 2 with v
+        conv_lhs => rw [gammaSet_eq_gcd_mul_divIntMap ((gammaSet_one_mem_iff r _).mpr v.2.2),
+          ← natCast_zsmul, eisSummand_smul]
+        norm_cast
+      _ = (r : ℂ) ^ (-k) * eisensteinSeries ((ZMod.unitOfCoprime r h)⁻¹ • a) k z := by
+        rw [tsum_mul_left]
+        congr! 1
+        exact ((bijOn_divIntMap_gammaSet _ _ a h).equiv _).tsum_eq (eisSummand k · z)
+
+/-- Mapping a positive natural number `m` congruent to `n`
+mod `N` to the corresponding element of the fiber of `coprimeUnitMap` over `n`. -/
+def toCoprimeUnitFiber (n : (ZMod N)ˣ)
+    (m : {m : ℕ // 0 < m ∧ (m : ZMod N) = n}) : ZMod.coprimeUnitMap ⁻¹' {n} :=
+  ⟨⟨m.1, (ZMod.isUnit_iff_coprime m.1 N).mp (by simp [m.2.2])⟩,
+    Units.ext (by simp [ZMod.coprimeUnitMap, m.2.2])⟩
+
+/-- The Eisenstein series `G` with congruence condition `a`
+mod `N` is the sum over `n ∈ (ZMod N)ˣ` of `ζ₊ⁿ(k) * E (n⁻¹ • a)`, where `ζ₊ⁿ(k)` is the
+`L`-function of the indicator function of the residue class `n` and `E` is `eisensteinSeries`. -/
+theorem G_eq_sum_E [NeZero N] {k : ℤ} (hk : 3 ≤ k) (z : ℍ) :
+    eisensteinSeriesG a k z = ∑ n : (ZMod N)ˣ,
+      ZMod.LFunction (Pi.single n.val 1) k * eisensteinSeries (n⁻¹ • a) k z := by
+  have hk0 : k ≠ 0 := by omega
+  have hσ := summable_coprime_eisSummand a hk z
+  have h1 : eisensteinSeriesG a k z =
+      ∑' p : Σ r : {r : ℕ // r.Coprime N}, gammaSet N r.1 a, eisSummand k p.2 z :=
+    ((gammaSetCoprimeSigmaEquiv a).symm.tsum_eq (eisSummand k · z)).symm
+  rw [h1, hσ.tsum_sigma, ← (hσ.sigma.hasSum.tsum_fiberwise ZMod.coprimeUnitMap).tsum_eq,
+    tsum_fintype]
+  refine Finset.sum_congr rfl fun n _ ↦ ?_
+  have h3 : ∀ p : ZMod.coprimeUnitMap ⁻¹' {n}, ∑' v : gammaSet N p.1 a, eisSummand k v z =
+      p.1 ^ (-k) * eisensteinSeries (n⁻¹ • a) k z := by
+    intro ⟨r, hr⟩
+    rw [tsum_gammaSet_eisSummand_of_coprime a hk0 z r.2]
+    congr
+  rw [tsum_congr h3, tsum_mul_right, ← tsum_zpow_eq_LFunction n (by omega)]
+  congr! 1
+  refine (Function.Injective.tsum_eq (g := toCoprimeUnitFiber n)
+    (fun _ _ hm ↦ Subtype.ext (congrArg (fun x ↦ x.1.1) hm)) fun x hx ↦ ?_).symm
+  have hx0 : x.1.1 ≠ 0 := fun h0 ↦ hx (by simp [h0, _root_.zero_zpow _ hk0])
+  simp only [Set.mem_range, Subtype.exists]
+  use x.1.1, ⟨Nat.pos_of_ne_zero hx0, (ZMod.coe_unitOfCoprime _ _).symm.trans
+    (congrArg Units.val x.2)⟩
+  rfl
+
+end G_eq_sum_E
+
+namespace ModularForm
+
+open UpperHalfPlane EisensteinSeries CongruenceSubgroup
+
+/-- The Eisenstein series `G` of weight `k`, level `Γ(N)` and congruence condition
+`a : Fin 2 → ZMod N` as a modular form. -/
+def eisensteinSeriesGMF {k : ℤ} {N : ℕ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) :
+    ModularForm Γ(N) k :=
+  ∑ n : (ZMod N)ˣ, ZMod.LFunction (Pi.single n.val 1) k • eisensteinSeriesMF hk (n⁻¹ • a)
+
+lemma eisensteinSeriesGMF_apply {k : ℤ} {N : ℕ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N)
+    (z : ℍ) : eisensteinSeriesGMF hk a z = eisensteinSeriesG a k z := by
+  rw [G_eq_sum_E a hk z]
+  have := congr_fun (map_sum coeHom (fun n : (ZMod N)ˣ ↦
+    ZMod.LFunction (Pi.single n.val 1) k • eisensteinSeriesMF hk (n⁻¹ • a)) Finset.univ) z
+  rwa [coeHom_apply, Finset.sum_apply] at this
+
+end ModularForm

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean

@@ -139,6 +139,48 @@ def gammaSetDivGcdSigmaEquiv : (Fin 2 → ℤ) ≃ (Σ r : ℕ, gammaSet 1 r 0)
 lemma gammaSetDivGcdSigmaEquiv_symm_eq (v : Σ r : ℕ, gammaSet 1 r 0) :
     (gammaSetDivGcdSigmaEquiv.symm v) = v.2 := rfl
 
+variable {N} in
+/-- The equivalence between the index set of `eisensteinSeriesG` and the disjoint union of
+the `gammaSet N r a` over `r` coprime to `N`. -/
+def gammaSetCoprimeSigmaEquiv : {v : Fin 2 → ℤ | (↑) ∘ v = a ∧ (finGcdMap v).gcd N = 1} ≃
+    Σ r : {r : ℕ // r.Coprime N}, gammaSet N r a where
+  toFun v := ⟨⟨finGcdMap v.1, v.2.2⟩, v.1, v.2.1, rfl⟩
+  invFun p := ⟨p.2.1, p.2.2.1, by simp [p.2.2.2, p.1.2]⟩
+  left_inv v := rfl
+  right_inv p := Sigma.subtype_ext (Subtype.ext p.2.2.2) rfl
+
+/-- For `r ≠ 0` coprime to `N`, dividing by `r` maps `gammaSet N r a` bijectively onto the set
+of coprime vectors congruent to `r⁻¹ • a` mod `N`. -/
+lemma bijOn_divIntMap_gammaSet [NeZero r] (a) (h : r.Coprime N) :
+    Set.BijOn (divIntMap r) (gammaSet N r a)
+      (gammaSet N 1 ((ZMod.unitOfCoprime r h)⁻¹ • a)) := by
+  refine ⟨fun v hv ↦ ⟨?_, Int.isCoprime_iff_gcd_eq_one.mp (finGcdMap_div v hv.2)⟩, ?_, ?_⟩
+  · funext i
+    have h1 : (r : ZMod N) * ((divIntMap r v) i : ℤ) = a i := by
+      have h2 : (((r • divIntMap r v) i : ℤ) : ZMod N) = a i := by
+        rw [← gammaSet_eq_gcd_mul_divIntMap ((gammaSet_one_mem_iff r v).mpr hv.2)]
+        exact congr_fun hv.1 i
+      rw [← h2, Pi.smul_apply, nsmul_eq_mul, Int.cast_mul, Int.cast_natCast]
+    simp only [Function.comp_apply, Pi.smul_apply, Units.smul_def, smul_eq_mul]
+    rw [Units.eq_inv_mul_iff_mul_eq, ZMod.coe_unitOfCoprime]
+    exact h1
+  · intro x hx y hy hxy
+    ext i
+    exact (Int.ediv_left_inj (gammaSet_div_gcd ((gammaSet_one_mem_iff r x).mpr hx.2) i)
+      (gammaSet_div_gcd ((gammaSet_one_mem_iff r y).mpr hy.2) i)).mp (congr_fun hxy i)
+  · intro w hw
+    use r • w
+    constructor
+    · constructor
+      · funext i
+        have := congr_fun hw.1 i
+        simp only [Function.comp_apply, Pi.smul_apply, Units.smul_def, smul_eq_mul] at this ⊢
+        rw [Int.nsmul_eq_mul, Int.cast_mul,Int.cast_natCast, this, ← ZMod.coe_unitOfCoprime r h,
+          ← mul_assoc, Units.mul_inv, one_mul]
+      · simpa [finGcdMap] using finGcdMap_smul r hw.2
+    · ext i
+      simpa using Int.mul_ediv_cancel_left _ (mod_cast NeZero.ne r)
+
 end gammaSet_def
 
 variable {N a r} [NeZero r]
@@ -185,6 +227,12 @@ section eisSummand
 /-- The function on `(Fin 2 → ℤ)` whose sum defines an Eisenstein series. -/
 def eisSummand (k : ℤ) (v : Fin 2 → ℤ) (z : ℍ) : ℂ := (v 0 * z + v 1) ^ (-k)
 
+/-- How the `eisSummand` function changes under scalar multiplication of the vector. -/
+lemma eisSummand_smul (k c : ℤ) (v : Fin 2 → ℤ) (z : ℍ) :
+    eisSummand k (c • v) z = (c : ℂ) ^ (-k) * eisSummand k v z := by
+  simp only [eisSummand, Pi.smul_apply, smul_eq_mul, Int.cast_mul, ← mul_zpow]
+  ring_nf
+
 /-- How the `eisSummand` function changes under the Moebius action. -/
 theorem eisSummand_SL2_apply (k : ℤ) (i : (Fin 2 → ℤ)) (A : SL(2, ℤ)) (z : ℍ) :
     eisSummand k i (A • z) = (denom A z) ^ k * eisSummand k (i ᵥ* A) z := by
@@ -229,4 +277,8 @@ lemma eisensteinSeriesSIF_apply (k : ℤ) (z : ℍ) :
 
 @[deprecated (since := "2026-02-10")] alias eisensteinSeries_SIF_apply := eisensteinSeriesSIF_apply
 
+/-- An Eisenstein series of weight `k` and level `Γ(N)`, with congruence condition `a`. -/
+def _root_.eisensteinSeriesG (k : ℤ) (z : ℍ) : ℂ :=
+  ∑' x : {v : Fin 2 → ℤ | (↑) ∘ v = a ∧ (finGcdMap v).gcd N = 1}, eisSummand k x z
+
 end EisensteinSeries

Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean

@@ -45,6 +45,11 @@ lemma summable_norm_eisSummand {k : ℤ} (hk : 3 ≤ k) (z : ℍ) :
   simp only [eisSummand, norm_zpow]
   exact_mod_cast summand_bound z (show 0 ≤ (k : ℝ) by positivity) b
 
+lemma summable_coprime_eisSummand {N : ℕ} {k : ℤ} (a : Fin 2 → ZMod N) (hk : 3 ≤ k) (z : ℍ) :
+    Summable fun p : Σ r : {r : ℕ // r.Coprime N}, gammaSet N r.1 a ↦ eisSummand k p.2 z := by
+  rw [← Equiv.summable_iff (gammaSetCoprimeSigmaEquiv a)]
+  exact ((summable_norm_eisSummand hk z).of_norm.subtype _)
+
 /-- The norm of the restricted sum is less than the full sum of the norms. -/
 lemma norm_le_tsum_norm (N : ℕ) (a : Fin 2 → ZMod N) (k : ℤ) (hk : 3 ≤ k) (z : ℍ) :
     ‖eisensteinSeries a k z‖ ≤ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x z‖ := by