[Merged by Bors] - Eisenstein series are mdifferentiable

Mathlib.lean

@@ -3111,6 +3111,7 @@ import Mathlib.NumberTheory.Modular
 import Mathlib.NumberTheory.ModularForms.Basic
 import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
+import Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold

Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

@@ -9,6 +9,7 @@ import Mathlib.Analysis.Convex.Normed
 import Mathlib.Analysis.Convex.Complex
 import Mathlib.Analysis.Complex.ReImTopology
 import Mathlib.Topology.Homotopy.Contractible
+import Mathlib.Topology.PartialHomeomorph
 
 #align_import analysis.complex.upper_half_plane.topology from "leanprover-community/mathlib"@"57f9349f2fe19d2de7207e99b0341808d977cdcf"
 
@@ -107,4 +108,16 @@ lemma subset_verticalStrip_of_isCompact {K : Set ℍ} (hK : IsCompact K) :
 
 end strips
 
+/-- A continuous section `ℂ → ℍ` of the natural inclusion map, bundled as a `PartialHomeomorph`. -/
+def ofComplex : PartialHomeomorph ℂ ℍ := (openEmbedding_coe.toPartialHomeomorph _).symm
+
+/-- Extend a function on `ℍ` arbitrarily to a function on all of `ℂ`. -/
+scoped notation "↑ₕ" f => f ∘ ofComplex
+
+lemma ofComplex_apply (z : ℍ) : ofComplex (z : ℂ) = z :=
+  OpenEmbedding.toPartialHomeomorph_left_inv ..
+
+lemma comp_ofComplex (f : ℍ → ℂ) (z : ℍ) : (↑ₕ f) z = f z := by
+  rw [Function.comp_apply, ofComplex_apply]
+
 end UpperHalfPlane

Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2024 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+
+import Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
+import Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
+import Mathlib.Analysis.Complex.LocallyUniformLimit
+import Mathlib.Geometry.Manifold.MFDeriv.FDeriv
+
+/-!
+# Holomorphicity of Eisenstein series
+
+We show that Eisenstein series of weight `k` and level `Γ(N)` with congruence condition
+`a : Fin 2 → ZMod N` are holomorphic on the upper half plane, which is stated as being
+MDifferentiable.
+-/
+
+noncomputable section
+
+open ModularForm EisensteinSeries UpperHalfPlane Set Filter Function Complex Manifold
+
+open scoped Topology BigOperators Nat Classical UpperHalfPlane
+
+namespace EisensteinSeries
+
+/-- Auxilary lemma showing that for any `k : ℤ` the function `z → 1/(c*z+d)^k` is
+differentiable on `{z : ℂ | 0 < z.im}`. -/
+lemma div_linear_zpow_differentiableOn (k : ℤ) (a : Fin 2 → ℤ) :
+    DifferentiableOn ℂ (fun z : ℂ => 1 / (a 0 * z + a 1) ^ k) {z : ℂ | 0 < z.im} := by
+  rcases ne_or_eq a 0 with ha | rfl
+  · apply DifferentiableOn.div (differentiableOn_const 1)
+    · apply DifferentiableOn.zpow
+      · fun_prop
+      · left
+        exact fun z hz ↦ linear_ne_zero _ ⟨z, hz⟩
+          ((comp_ne_zero_iff _ Int.cast_injective Int.cast_zero).mpr ha)
+    ·  exact fun z hz ↦ zpow_ne_zero k (linear_ne_zero (a ·)
+        ⟨z, hz⟩ ((comp_ne_zero_iff _ Int.cast_injective Int.cast_zero).mpr ha))
+  · simp only [ Fin.isValue, Pi.zero_apply, Int.cast_zero, zero_mul, add_zero, one_div]
+    apply differentiableOn_const
+
+/-- Auxilary lemma showing that for any `k : ℤ` and `(a : Fin 2 → ℤ)`
+the extension of `eisSummand` is differentiable on `{z : ℂ | 0 < z.im}`.-/
+lemma eisSummand_extension_differentiableOn (k : ℤ) (a : Fin 2 → ℤ) :
+    DifferentiableOn ℂ (↑ₕeisSummand k a) {z : ℂ | 0 < z.im} := by
+  apply DifferentiableOn.congr (div_linear_zpow_differentiableOn k a)
+  intro z hz
+  lift z to ℍ using hz
+  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
+  intro τ
+  suffices DifferentiableAt ℂ (↑ₕeisensteinSeries_SIF a k) τ.1 by
+    convert MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe
+    exact funext fun z ↦ (comp_ofComplex (eisensteinSeries_SIF a k) z).symm
+  refine DifferentiableOn.differentiableAt ?_
+    ((isOpen_lt continuous_const Complex.continuous_im).mem_nhds τ.2)
+  exact (eisensteinSeries_tendstoLocallyUniformlyOn hk a).differentiableOn
+    (eventually_of_forall fun s ↦ DifferentiableOn.sum
+      fun _ _ ↦ eisSummand_extension_differentiableOn _ _)
+        (isOpen_lt continuous_const continuous_im)

Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean

@@ -31,7 +31,8 @@ noncomputable section
 
 open Complex UpperHalfPlane Set Finset
 
-open scoped BigOperators
+open scoped BigOperators UpperHalfPlane
+
 
 variable (z : ℍ)
 
@@ -179,15 +180,13 @@ theorem eisensteinSeries_tendstoLocallyUniformly {k : ℤ} (hk : 3 ≤ k) {N : 
   simpa only [eisSummand, one_div, ← zpow_neg, norm_eq_abs, abs_zpow, ← Real.rpow_intCast,
     Int.cast_neg] using summand_bound_of_mem_verticalStrip (by positivity) p hB hz
 
-/-- Extend a function on `ℍ` arbitrarily to a function on all of `ℂ`. -/
-local notation "↑ₕ" f => f ∘ (PartialHomeomorph.symm (openEmbedding_coe.toPartialHomeomorph _))
-
 /-- Variant of `eisensteinSeries_tendstoLocallyUniformly` formulated with maps `ℂ → ℂ`, which is
 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 a )) ↦
-      ↑ₕ(fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k x z )) (↑ₕ(eisensteinSeries_SIF a k).toFun)
-          Filter.atTop (UpperHalfPlane.coe '' ⊤) := by
+      ↑ₕ(fun (z : ℍ) ↦ ∑ x in s, eisSummand k x z )) (↑ₕ(eisensteinSeries_SIF a k).toFun)
+          Filter.atTop {z : ℂ | 0 < z.im} := by
+  rw [← Subtype.coe_image_univ {z : ℂ | 0 < z.im}]
   apply TendstoLocallyUniformlyOn.comp (s := ⊤) _ _ _ (PartialHomeomorph.continuousOn_symm _)
   · simp only [SlashInvariantForm.toFun_eq_coe, Set.top_eq_univ, tendstoLocallyUniformlyOn_univ]
     apply eisensteinSeries_tendstoLocallyUniformly hk