feat(NumberTheory/ModularForm/EisensteinSeries/E2): Prove E2 is MDifferentiable (leanprover-community#35819)

Proof that E2 is MDifferentiable. This proof comes from the Sphere packing project where it was produced by Gauss.

Co-authored-by: Math.inc's Gauss

Author: CBirkbeck

Mathlib.lean

@@ -5469,6 +5469,7 @@ public import Mathlib.NumberTheory.ModularForms.DedekindEta
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
+public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty

Mathlib/NumberTheory/ModularForms/DedekindEta.lean

@@ -62,7 +62,8 @@ lemma one_sub_eta_q_ne_zero (n : ℕ) {z : ℂ} (hz : z ∈ ℍₒ) : 1 - eta_q
 /-- The eta function, whose value at z is `q^ 1 / 24 * ∏' 1 - q ^ (n + 1)` for `q = e ^ 2 π i z`. -/
 noncomputable def eta (z : ℂ) := 𝕢 24 z * ∏' n, (1 - eta_q n z)
 
-local notation "η" => eta
+/-- Notation for the Dedekind eta function. -/
+scoped[ModularForm] notation "η" => eta
 
 theorem summable_eta_q (z : ℍ) : Summable fun n ↦ ‖-eta_q n z‖ := by
   simp [eta_q, eta_q_eq_pow, summable_nat_add_iff 1, norm_exp_two_pi_I_lt_one z]

Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/MDifferentiable.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2026 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck, Gauss AI (Math Inc)
+-/
+
+module
+
+public import Mathlib.NumberTheory.ModularForms.DedekindEta
+
+/-!
+# MDifferentiability of the weight 2 Eisenstein series
+
+We show that the weight 2 Eisenstein series `E2` is MDifferentiable (i.e. holomorphic as a
+function `ℍ → ℂ`). The proof uses the relation between `E2` and the logarithmic derivative of
+the Dedekind eta function.
+-/
+
+@[expose] public section
+
+open UpperHalfPlane hiding I
+open Real Complex EisensteinSeries ModularForm Manifold
+
+
+--This proof was provided by Gauss to the sphere packing project.
+/-- The weight 2 Eisenstein series `E2` is MDifferentiable -/
+lemma E2_mdifferentiable : MDiff E2 := by
+  rw [UpperHalfPlane.mdifferentiable_iff]
+  have hη : DifferentiableOn ℂ η _ := fun z hz ↦
+    (differentiableAt_eta_of_mem_upperHalfPlaneSet hz).differentiableWithinAt
+  have hlog : DifferentiableOn ℂ (logDeriv η) _ :=
+    (hη.deriv isOpen_upperHalfPlaneSet).div hη (fun _ hz ↦ eta_ne_zero hz)
+  refine (hlog.const_mul (π * I / 12)⁻¹).congr (fun z hz ↦ ?_)
+  simp [ofComplex_apply_of_im_pos hz, logDeriv_eta_eq_E2 ⟨z, hz⟩]
+  field_simp
+
+end