[Merged by Bors] - Eisenstein series uniform convergence

Mathlib.lean

@@ -2845,6 +2845,8 @@ 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.Finset_Decomposition
+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

@@ -123,6 +123,8 @@ theorem mk_coe (z : ℍ) (h : 0 < (z : ℂ).im := z.2) : mk z h = z :=
   rfl
 #align upper_half_plane.mk_coe UpperHalfPlane.mk_coe
 
+lemma coe_eq_fst (z : ℍ) : (z : ℂ) = z.1 := rfl
+
 theorem re_add_im (z : ℍ) : (z.re + z.im * Complex.I : ℂ) = z :=
   Complex.re_add_im z
 #align upper_half_plane.re_add_im UpperHalfPlane.re_add_im

Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean

@@ -384,4 +384,51 @@ instance : IsometricSMul SL(2, ℝ) ℍ :=
       exact
         (isometry_real_vadd w).comp (h₀.comp <| (isometry_real_vadd v).comp <| isometry_pos_mul u)⟩
 
+section slices
+
+/--The verticel strip of width A and height B-/
+def upperHalfPlaneSlice (A B : ℝ) :=
+  {z : ℍ | Complex.abs z.1.1 ≤ A ∧ Complex.abs z.1.2 ≥ B}
+
+theorem slice_mem (A B : ℝ) (z : ℍ) :
+    z ∈ upperHalfPlaneSlice A B ↔ Complex.abs z.1.1 ≤ A ∧ Complex.abs z.1.2 ≥ B := Iff.rfl
+
+lemma compact_in_some_slice (K : Set ℍ) (hK : IsCompact K) : ∃  A B : ℝ, 0 < B ∧
+    K ⊆ upperHalfPlaneSlice A B  := by
+  by_cases hne : Set.Nonempty K
+  · have hcts : ContinuousOn (fun t =>  t.im) K := by
+       apply Continuous.continuousOn UpperHalfPlane.continuous_im
+    obtain ⟨b, _, HB⟩ :=  IsCompact.exists_isMinOn hK hne hcts
+    let t := (⟨Complex.I, by simp⟩ : ℍ)
+    have  ht : UpperHalfPlane.im t = I.im := by rfl
+    obtain ⟨r, _, hr2⟩ := Bornology.IsBounded.subset_closedBall_lt hK.isBounded 0 t
+    refine' ⟨Real.sinh (r) + Complex.abs ((UpperHalfPlane.center t r)), b.im, b.2, _⟩
+    intro z hz
+    simp only [I_im, slice_mem, 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 t 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
+    have htim : UpperHalfPlane.im t = 1 := by
+      simp only [ht]
+    rw [htim] at hr3
+    simp only [one_mul, add_le_add_iff_right, ge_iff_le] 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
+  · rw [not_nonempty_iff_eq_empty] at hne
+    rw [hne]
+    simp only [empty_subset, and_true, exists_const]
+    use 1
+    linarith
+
+end slices
+
 end UpperHalfPlane

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Finset_Decomposition.lean

@@ -0,0 +1,121 @@
+/-
+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.Data.Complex.Abs
+import Mathlib.Data.IsROrC.Basic
+
+/-! # Decomposing `ℤ × ℤ` into squares
+
+We partition `ℤ × ℤ` into squares of the form `Icc (-n) n × Icc (-n) n` for `n : ℕ`. This is useful
+for bounding Eisenstein series.
+-/
+
+open Complex
+
+open scoped BigOperators NNReal Classical Filter Matrix
+
+noncomputable section
+
+namespace EisensteinSeries
+
+open Finset
+
+/-- For  `m : ℤ` this is the finset of `ℤ × ℤ` of elements such that the maximum of the
+absolute values of the pair is `m` -/
+def square (m : ℤ) : Finset (ℤ × ℤ) :=
+  ((Icc (-m) (m)) ×ˢ (Icc (-m) (m))).filter fun x => max x.1.natAbs x.2.natAbs = m
+
+-- a re-definition in simp-normal form
+lemma square_eq (m : ℤ) :
+    square m = ((Icc (-m) m) ×ˢ (Icc (-m) m)).filter fun x => max |x.1| |x.2| = m := by
+  simp [square]
+
+lemma mem_square_aux {m : ℤ} {i} : i ∈ Icc (-m) m ×ˢ Icc (-m) m ↔ max |i.1| |i.2| ≤ m := by
+  simp [abs_le]
+
+lemma square_disj {n : ℤ} : Disjoint (square (n+1)) (Icc (-n) n ×ˢ Icc (-n) n) := by
+  rw [square_eq]
+  simp only [Finset.disjoint_left, mem_filter, mem_square_aux]
+  rintro x ⟨-, hx⟩
+  simp [hx]
+
+lemma square_union {n : ℤ} :
+    square (n+1) ∪ Icc (-n) n ×ˢ Icc (-n) n = Icc (-(n+1)) (n+1) ×ˢ Icc (-(n+1)) (n+1) := by
+  ext x
+  rw [mem_union, square_eq, mem_filter, mem_square_aux, mem_square_aux,
+    and_iff_right_of_imp le_of_eq, Int.le_add_one_iff, or_comm]
+
+lemma square_disjunion (n : ℤ) :
+    (square (n+1)).disjUnion (Icc (-n) n ×ˢ Icc (-n) n) square_disj =
+    Icc (-(n+1)) (n+1) ×ˢ Icc (-(n+1)) (n+1) := by rw [disjUnion_eq_union, square_union]
+
+theorem square_size (n : ℕ) : Finset.card (square (n + 1)) = 8 * (n + 1) := by
+  have : (((square (n+1)).disjUnion (Icc (-n : ℤ) n ×ˢ Icc (-n : ℤ) n) square_disj).card : ℤ) =
+    (Icc (-(n+1 : ℤ)) (n+1) ×ˢ Icc (-(n+1 : ℤ)) (n+1)).card
+  · rw [square_disjunion]
+  rw [card_disjUnion, card_product, Nat.cast_add, Nat.cast_mul, card_product, Nat.cast_mul,
+    Int.card_Icc, Int.card_Icc, Int.toNat_sub_of_le, Int.toNat_sub_of_le,
+    ← eq_sub_iff_add_eq] at this
+  · rw [← Nat.cast_inj (R := ℤ), this, Nat.cast_mul, Nat.cast_ofNat, Nat.cast_add_one]
+    ring_nf
+  · linarith
+  · linarith
+
+theorem natAbs_le_iff_mem_Icc (a : ℤ) (n : ℕ) :
+    Int.natAbs a ≤ n ↔ a ∈ Finset.Icc (-(n : ℤ)) n := by
+  rw [mem_Icc, ← abs_le, Int.abs_eq_natAbs, Int.ofNat_le]
+
+@[simp]
+theorem square_mem (n : ℕ) (x : ℤ × ℤ) : x ∈ square n ↔ max x.1.natAbs x.2.natAbs = n := by
+  simp_rw [square, Finset.mem_filter, Nat.cast_inj, mem_product, and_iff_right_iff_imp,
+    ← natAbs_le_iff_mem_Icc]
+  rintro rfl
+  simp only [le_max_iff, le_refl, true_or, or_true, and_self]
+
+theorem square_size' {n : ℕ} (h : n ≠ 0) : Finset.card (square n) = 8 * n := by
+  obtain ⟨n, rfl⟩ := n.exists_eq_succ_of_ne_zero h
+  exact mod_cast square_size n
+
+theorem squares_cover_all (y : ℤ × ℤ) : ∃! i : ℕ, y ∈ square i := by
+  use max y.1.natAbs y.2.natAbs
+  simp only [square_mem, and_self_iff, forall_eq']
+
+@[simp]
+lemma square_zero : square 0 = {(0, 0)} := rfl
+
+theorem square_zero_card : Finset.card (square 0) = 1 := by
+  rw [square_zero, card_singleton]
+
+lemma Complex_abs_eq_of_mem_square (n : ℕ) (x : ℤ × ℤ) (h : x ∈ square n) :
+    Complex.abs x.1 = n ∨ Complex.abs x.2 = n := by
+  simp_rw [eq_comm (b := (n : ℝ)), ← int_cast_abs, square_mem] at *
+  norm_cast
+  subst n
+  simp only [Nat.cast_max, Int.coe_natAbs, max_eq_left_iff, max_eq_right_iff] at *
+  exact Int.le_total |x.2| |x.1|
+
+lemma Complex_abs_square_left_ne (n : ℕ) (x : ℤ × ℤ) (h : x ∈ square n)
+    (hx : Complex.abs (x.1) ≠ n) : Complex.abs (x.2) = n :=
+  Complex_abs_eq_of_mem_square n x h |>.resolve_left hx
+
+lemma fun_ne_zero_cases (x : Fin 2 → ℤ) : x ≠ 0 ↔ x 0 ≠ 0 ∨ x 1 ≠ 0 := by
+  rw [Function.ne_iff]
+  exact Fin.exists_fin_two
+
+lemma square_ne_zero (n : ℕ) (x : Fin 2 → ℤ) (hx : ⟨x 0, x 1 ⟩ ∈ square n) : x ≠ 0 ↔ n ≠ 0 := by
+  constructor
+  intro h h0
+  rw [h0] at hx
+  simp only [Nat.cast_zero, square_zero, mem_singleton, Prod.mk.injEq] at hx
+  rw [fun_ne_zero_cases, hx.1, hx.2] at h
+  simp only [ne_eq, not_true_eq_false, or_self] at *
+  intro hn h
+  have hx0 : x 0 = 0 := by
+    simp only [h, Pi.zero_apply]
+  have hx1 : x 1 = 0 := by
+    simp only [h, Pi.zero_apply]
+  rw [hx0, hx1] at hx
+  simp only [square_mem, Int.natAbs_zero, max_self] at hx
+  exact hn (id hx.symm)