chore: fix some names around Eisenstein series (#35055)

Per the naming convention,
- `eisensteinSeries_MF` should be `eisensteinSeriesMF`,
- `eisensteinSeries_SIF` should be `eisensteinSeriesSIF`, and
- `eisensteinSeries_SIF_MDifferentiable` should use suffix `_mdifferentiable`.

Author: grunweg

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean

@@ -30,19 +30,21 @@ open EisensteinSeries CongruenceSubgroup Matrix.SpecialLinearGroup
 
 /-- This defines Eisenstein series as modular forms of weight `k`, level `Γ(N)` and congruence
 condition given by `a : Fin 2 → ZMod N`. -/
-def eisensteinSeries_MF {k : ℤ} {N : ℕ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) :
+def eisensteinSeriesMF {k : ℤ} {N : ℕ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) :
     ModularForm Γ(N) k where
-  toFun := eisensteinSeries_SIF a k
-  slash_action_eq' := (eisensteinSeries_SIF a k).slash_action_eq'
-  holo' := eisensteinSeries_SIF_MDifferentiable hk a
+  toFun := eisensteinSeriesSIF a k
+  slash_action_eq' := (eisensteinSeriesSIF a k).slash_action_eq'
+  holo' := eisensteinSeriesSIF_mdifferentiable hk a
   bdd_at_cusps' {c} hc := by
     rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc
     rw [OnePoint.isBoundedAt_iff_forall_SL2Z hc]
-    exact fun γ hγ ↦ isBoundedAtImInfty_eisensteinSeries_SIF a hk γ
+    exact fun γ hγ ↦ isBoundedAtImInfty_eisensteinSeriesSIF a hk γ
+
+@[deprecated (since := "2026-02-10")] noncomputable alias eisensteinSeries_MF := eisensteinSeriesMF
 
 /-- Normalised Eisenstein series of level 1 and weight `k`,
 here they have been scaled by `1/2` since we sum over coprime pairs. -/
 noncomputable def E {k : ℕ} (hk : 3 ≤ k) : ModularForm Γ(1) k :=
-  (1 / 2 : ℂ) • eisensteinSeries_MF (mod_cast hk) 0
+  (1 / 2 : ℂ) • eisensteinSeriesMF (mod_cast hk) 0
 
 end ModularForm

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean

@@ -214,15 +214,20 @@ lemma eisensteinSeries_slash_apply (k : ℤ) (γ : SL(2, ℤ)) :
   congr 1
   exact (gammaSetEquiv a γ).tsum_eq (eisSummand k · z)
 
-/-- The SlashInvariantForm defined by an Eisenstein series of weight `k : ℤ`, level `Γ(N)`,
-  and congruence condition given by `a : Fin 2 → ZMod N`. -/
-def eisensteinSeries_SIF (k : ℤ) : SlashInvariantForm (Gamma N) k where
+/-- The `SlashInvariantForm` defined by an Eisenstein series of weight `k : ℤ`, level `Γ(N)`,
+and congruence condition given by `a : Fin 2 → ZMod N`. -/
+def eisensteinSeriesSIF (k : ℤ) : SlashInvariantForm (Gamma N) k where
   toFun := eisensteinSeries a k
   slash_action_eq' A hA := by
     obtain ⟨A, (hA : A ∈ Γ(N)), rfl⟩ := hA
     simp [SpecialLinearGroup.mapGL, ← SL_slash, eisensteinSeries_slash_apply, Gamma_mem'.mp hA]
 
-lemma eisensteinSeries_SIF_apply (k : ℤ) (z : ℍ) :
-    eisensteinSeries_SIF a k z = eisensteinSeries a k z := rfl
+@[deprecated (since := "2026-02-10")]
+noncomputable alias eisensteinSeries_SIF := eisensteinSeriesSIF
+
+lemma eisensteinSeriesSIF_apply (k : ℤ) (z : ℍ) :
+    eisensteinSeriesSIF a k z = eisensteinSeries a k z := rfl
+
+@[deprecated (since := "2026-02-10")] alias eisensteinSeries_SIF_apply := eisensteinSeriesSIF_apply
 
 end EisensteinSeries

Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean

@@ -54,14 +54,14 @@ lemma norm_le_tsum_norm (N : ℕ) (a : Fin 2 → ZMod N) (k : ℤ) (hk : 3 ≤ k
       (summable_norm_eisSummand hk z))
 
 /-- Eisenstein series are bounded at infinity. -/
-theorem isBoundedAtImInfty_eisensteinSeries_SIF {N : ℕ} [NeZero N] (a : Fin 2 → ZMod N) {k : ℤ}
-    (hk : 3 ≤ k) (A : SL(2, ℤ)) : IsBoundedAtImInfty (eisensteinSeries_SIF a k ∣[k] A) := by
-  simp_rw [UpperHalfPlane.isBoundedAtImInfty_iff, eisensteinSeries_SIF] at *
+theorem isBoundedAtImInfty_eisensteinSeriesSIF {N : ℕ} [NeZero N] (a : Fin 2 → ZMod N) {k : ℤ}
+    (hk : 3 ≤ k) (A : SL(2, ℤ)) : IsBoundedAtImInfty (eisensteinSeriesSIF a k ∣[k] A) := by
+  simp_rw [UpperHalfPlane.isBoundedAtImInfty_iff, eisensteinSeriesSIF] at *
   refine ⟨∑'(x : Fin 2 → ℤ), r ⟨⟨N, 2⟩, Nat.ofNat_pos⟩ ^ (-k) * ‖x‖ ^ (-k), 2, ?_⟩
   intro z hz
   obtain ⟨n, hn⟩ := (ModularGroup_T_zpow_mem_verticalStrip z (NeZero.pos N))
-  rw [SlashInvariantForm.coe_mk, eisensteinSeries_slash_apply, ← eisensteinSeries_SIF_apply,
-    ← T_zpow_width_invariant N k n (eisensteinSeries_SIF (a ᵥ* A) k) z]
+  rw [SlashInvariantForm.coe_mk, eisensteinSeries_slash_apply, ← eisensteinSeriesSIF_apply,
+    ← T_zpow_width_invariant N k n (eisensteinSeriesSIF (a ᵥ* A) k) z]
   apply le_trans (norm_le_tsum_norm N (a ᵥ* A) k hk _)
   have hk' : (2 : ℝ) < k := by norm_cast
   apply (summable_norm_eisSummand hk _).tsum_le_tsum _
@@ -72,4 +72,7 @@ theorem isBoundedAtImInfty_eisensteinSeries_SIF {N : ℕ} [NeZero N] (a : Fin 2
       summand_bound_of_mem_verticalStrip (lt_trans two_pos hk').le x two_pos
       (verticalStrip_anti_right N hz hn)
 
+@[deprecated (since := "2026-02-10")]
+alias isBoundedAtImInfty_eisensteinSeries_SIF := isBoundedAtImInfty_eisensteinSeriesSIF
+
 end EisensteinSeries

Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean

@@ -49,15 +49,18 @@ lemma eisSummand_extension_differentiableOn (k : ℤ) (a : Fin 2 → ℤ) :
   apply comp_ofComplex
 
 /-- Eisenstein series are MDifferentiable (i.e. holomorphic functions from `ℍ → ℂ`). -/
-theorem eisensteinSeries_SIF_MDifferentiable {k : ℤ} {N : ℕ} (hk : 3 ≤ k) (a : Fin 2 → ZMod N) :
-    MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (eisensteinSeries_SIF a k) := by
+theorem eisensteinSeriesSIF_mdifferentiable {k : ℤ} {N : ℕ} (hk : 3 ≤ k) (a : Fin 2 → ZMod N) :
+    MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (eisensteinSeriesSIF a k) := by
   intro τ
-  suffices DifferentiableAt ℂ (↑ₕeisensteinSeries_SIF a k) τ.1 by
+  suffices DifferentiableAt ℂ (↑ₕeisensteinSeriesSIF a k) τ.1 by
     convert MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe
-    exact funext fun z ↦ (comp_ofComplex (eisensteinSeries_SIF a k) z).symm
+    exact funext fun z ↦ (comp_ofComplex (eisensteinSeriesSIF a k) z).symm
   refine DifferentiableOn.differentiableAt ?_ (isOpen_upperHalfPlaneSet.mem_nhds τ.2)
   exact (eisensteinSeries_tendstoLocallyUniformlyOn hk a).differentiableOn
     (Eventually.of_forall fun s ↦ DifferentiableOn.fun_sum
     fun _ _ ↦ eisSummand_extension_differentiableOn _ _) isOpen_upperHalfPlaneSet
 
+@[deprecated (since := "2026-02-09")]
+alias eisensteinSeries_SIF_MDifferentiable := eisensteinSeriesSIF_mdifferentiable
+
 end EisensteinSeries

Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean

@@ -270,8 +270,8 @@ lemma tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries {k : ℕ} (hk : 3 ≤
 lemma EisensteinSeries.q_expansion_riemannZeta {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) (z : ℍ) :
     E hk z = 1 + (riemannZeta k)⁻¹ * (-2 * π * I) ^ k / (k - 1)! *
     ∑' n : ℕ+, σ (k - 1) n * cexp (2 * π * I * z) ^ (n : ℤ) := by
-  have : eisensteinSeries_MF (Int.toNat_le.mp hk) 0 z = eisensteinSeries_SIF (N := 1) 0 k z := rfl
-  rw [E, ModularForm.IsGLPos.smul_apply, this, eisensteinSeries_SIF_apply 0 k z, eisensteinSeries]
+  have : eisensteinSeriesMF (Int.toNat_le.mp hk) 0 z = eisensteinSeriesSIF (N := 1) 0 k z := rfl
+  rw [E, ModularForm.IsGLPos.smul_apply, this, eisensteinSeriesSIF_apply 0 k z, eisensteinSeries]
   have HE1 := tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow hk hk2 z
   have HE2 := tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries hk z
   have z2 : riemannZeta k ≠ 0 := riemannZeta_ne_zero_of_one_lt_re <| by norm_cast; grind

Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean

@@ -58,7 +58,7 @@ theorem eisensteinSeries_tendstoLocallyUniformly {k : ℤ} (hk : 3 ≤ k) {N : 
 nice to have for holomorphicity later. -/
 lemma eisensteinSeries_tendstoLocallyUniformlyOn {k : ℤ} {N : ℕ} (hk : 3 ≤ k)
     (a : Fin 2 → ZMod N) : TendstoLocallyUniformlyOn (fun (s : Finset (gammaSet N 1 a)) ↦
-      ↑ₕ(fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k x z)) (↑ₕ(eisensteinSeries_SIF a k))
+      ↑ₕ(fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k x z)) (↑ₕ(eisensteinSeriesSIF a k))
           Filter.atTop {z : ℂ | 0 < z.im} := by
   rw [← upperHalfPlaneSet, ← range_coe, ← image_univ]
   apply TendstoLocallyUniformlyOn.comp (s := ⊤) _ _ _ (OpenPartialHomeomorph.continuousOn_symm _)