feat(Complex/UpperHalfPlane): add vertical strips (#12443)

We define the vertical strips that are needed for proving Eisenstein series are modular forms #10377 . We also add the definition of sqrt{-1} as an elements of the upper half plane. Note that this is no longer needed for the modular forms PRs but its good to have.

Sorry about the typo in the PR name, its not my day!



Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

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 I := √-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/Topology.lean

@@ -74,4 +74,23 @@ instance : NoncompactSpace ℍ := by
 instance : LocallyCompactSpace ℍ :=
   openEmbedding_coe.locallyCompactSpace
 
+section strips
+
+/-- The vertical strip of width `A` and height `B`, defined by elements whose real part has absolute
+value less than or equal to `A` and imaginary part is at least `B`. -/
+def verticalStrip (A B : ℝ) := {z : ℍ | |z.re| ≤ A ∧ B ≤ z.im}
+
+theorem mem_verticalStrip_iff (A B : ℝ) (z : ℍ) : z ∈ verticalStrip A B ↔ |z.re| ≤ A ∧ B ≤ z.im :=
+  Iff.rfl
+
+lemma subset_verticalStrip_of_isCompact {K : Set ℍ} (hK : IsCompact K) :
+    ∃ A B : ℝ, 0 < B ∧ K ⊆ verticalStrip A B := by
+  rcases K.eq_empty_or_nonempty with rfl | hne
+  · exact ⟨1, 1, Real.zero_lt_one, empty_subset _⟩
+  obtain ⟨u, _, hu⟩ := hK.exists_isMaxOn hne (_root_.continuous_abs.comp continuous_re).continuousOn
+  obtain ⟨v, _, hv⟩ := hK.exists_isMinOn hne continuous_im.continuousOn
+  exact ⟨|re u|, im v, v.im_pos, fun k hk ↦ ⟨isMaxOn_iff.mp hu _ hk, isMinOn_iff.mp hv _ hk⟩⟩
+
+end strips
+
 end UpperHalfPlane