[Merged by Bors] - Eisenstein series uniform convergence

Mathlib.lean

@@ -3014,7 +3014,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.JacobiTheta.Bounds
+import Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -137,6 +137,18 @@ theorem ne_zero (z : ℍ) : (z : ℂ) ≠ 0 :=
   mt (congr_arg Complex.im) z.im_ne_zero
 #align upper_half_plane.ne_zero UpperHalfPlane.ne_zero
 
+/-- Define √-1 as an element on the upper half plane.-/
+def I : ℍ := ⟨Complex.I, by simp⟩
+
+@[simp]
+lemma I_im : I.im = 1 := rfl
+
+@[simp]
+lemma I_re : I.re = 0 := rfl
+
+@[simp, norm_cast]
+lemma coe_I : I = Complex.I := rfl
+
 end UpperHalfPlane
 
 namespace Mathlib.Meta.Positivity

Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean

@@ -385,4 +385,43 @@ instance : IsometricSMul SL(2, ℝ) ℍ :=
       exact
         (isometry_real_vadd w).comp (h₀.comp <| (isometry_real_vadd v).comp <| isometry_pos_mul u)⟩
 
+section slices
+
+/--The vertical strip of width A and height B-/
+def upperHalfPlaneSlice (A B : ℝ) :=
+  {z : ℍ | Complex.abs z.1.1 ≤ A ∧ B ≤ Complex.abs z.1.2}
+
+theorem slice_mem_iff (A B : ℝ) (z : ℍ) :
+    z ∈ upperHalfPlaneSlice A B ↔ Complex.abs z.1.1 ≤ A ∧ B ≤ Complex.abs z.1.2 := Iff.rfl
+
+lemma subset_slice_of_isCompact {K : Set ℍ} (hK : IsCompact K) : ∃ A B : ℝ, 0 < B ∧
+    K ⊆ upperHalfPlaneSlice A B := by
+  obtain rfl | hne := K.eq_empty_or_nonempty
+  exact ⟨1, 1, Real.zero_lt_one, by simp⟩
+  have hcts : ContinuousOn (fun t => t.im) K := by
+      apply Continuous.continuousOn UpperHalfPlane.continuous_im
+  obtain ⟨b, _, HB⟩ := IsCompact.exists_isMinOn hK hne hcts
+  obtain ⟨r, _, hr2⟩ := Bornology.IsBounded.subset_closedBall_lt hK.isBounded 0 UpperHalfPlane.I
+  refine' ⟨Real.sinh r + Complex.abs ((UpperHalfPlane.center UpperHalfPlane.I r)), b.im, b.2, _⟩
+  intro z hz
+  simp only [I_im, slice_mem_iff, abs_ofReal, ge_iff_le] at *
+  constructor
+  · have hr3 := hr2 hz
+    simp only [Metric.mem_closedBall] at hr3
+    apply le_trans (abs_re_le_abs z)
+    have := Complex.abs.sub_le (z : ℂ) (UpperHalfPlane.center UpperHalfPlane.I r) 0
+    simp only [sub_zero, ge_iff_le] at this
+    rw [dist_le_iff_dist_coe_center_le] at hr3
+    apply le_trans this
+    simp only [I_im, one_mul, add_le_add_iff_right] at *
+    exact hr3
+  · have hbz := HB hz
+    simp only [mem_setOf_eq, ge_iff_le] at *
+    convert hbz
+    rw [UpperHalfPlane.im]
+    apply abs_eq_self.mpr z.2.le
+
+
+end slices
+
 end UpperHalfPlane

Mathlib/Data/Finset/LocallyFinite/Box.lean

@@ -48,6 +48,16 @@ lemma box_succ_disjUnion (n : ℕ) :
 
 @[simp] lemma zero_mem_box : (0 : α) ∈ box n ↔ n = 0 := by cases n <;> simp [box_succ_eq_sdiff]
 
+lemma mem_box_eq_zero_iff_eq_zero (x : α) (hx : x ∈ box n) : x = 0 ↔ n = 0 := by
+  rw [← zero_mem_box (α := α)]
+  constructor
+  · intro h
+    rw [h] at hx
+    exact hx
+  · intro h
+    simp only [(zero_mem_box (α := α) (n := n)).mp h, box_zero, mem_singleton] at hx
+    exact hx
+
 end Finset
 
 open Finset

Mathlib/Logic/Equiv/Set.lean

@@ -179,6 +179,14 @@ def setProdEquivSigma {α β : Type*} (s : Set (α × β)) :
   right_inv := fun ⟨x, y, h⟩ => rfl
 #align equiv.set_prod_equiv_sigma Equiv.setProdEquivSigma
 
+/-- Equivalence between the sigma of a family of finsets of `β` and `β`. -/
+noncomputable def sigmaEquiv {ι κ : Type*} (s : κ → Set ι) (hs : ∀ i, ∃! j, i ∈ s j) :
+    (Σ j, s j) ≃ ι where
+  toFun x := x.2
+  invFun x := ⟨(hs x).choose, x, (hs x).choose_spec.1⟩
+  left_inv x := by ext; exacts [((hs x.2).choose_spec.2 x.1 x.2.2).symm, rfl]
+  right_inv x := by rfl
+
 /-- The subtypes corresponding to equal sets are equivalent. -/
 @[simps! apply]
 def setCongr {α : Type*} {s t : Set α} (h : s = t) : s ≃ t :=