feat(number_theory/modular): fundamental domain part 2 (#8985)

This completes the argument that the standard open domain `{z : |z|>1, |\Re(z)|<1/2}` is a fundamental domain for the action of `SL(2,\Z)` on `\H`. The first PR (#8611) showed that every point in the upper half plane has a representative inside its closure, and here we show that representatives in the open domain are unique.

Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Marc Masdeu <marc.masdeu@gmail.com>



Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Marc Masdeu <marc.masdeu@gmail.com>

Author: 3 people

src/algebra/group_power/order.lean

@@ -400,6 +400,9 @@ have t : 1^2 ≤ x^2 ↔ |1| ≤ |x| := ⟨abs_le_abs_of_sq_le_sq, sq_le_sq⟩,
 @[simp] lemma one_lt_sq_iff_one_lt_abs (x : R) : 1 < x^2 ↔ 1 < |x| :=
 have t : 1^2 < x^2 ↔ |1| < |x| := ⟨abs_lt_abs_of_sq_lt_sq, sq_lt_sq⟩, by simpa using t
 
+lemma pow_four_le_pow_two_of_pow_two_le {x y : R} (h : x^2 ≤ y) : x^4 ≤ y^2 :=
+(pow_mul x 2 2).symm ▸ pow_le_pow_of_le_left (sq_nonneg x) h 2
+
 end linear_ordered_ring
 
 section linear_ordered_comm_ring

src/algebra/order/group.lean

@@ -1146,6 +1146,9 @@ abs_le.2 ⟨(neg_add (|a|) (|b|)).symm ▸
   add_le_add (neg_le.2 $ neg_le_abs_self _) (neg_le.2 $ neg_le_abs_self _),
   add_le_add (le_abs_self _) (le_abs_self _)⟩
 
+lemma abs_add' (a b : α) : |a| ≤ |b| + |b + a| :=
+by simpa using abs_add (-b) (b + a)
+
 theorem abs_sub (a b : α) :
   |a - b| ≤ |a| + |b| :=
 by { rw [sub_eq_add_neg, ←abs_neg b], exact abs_add a _ }

src/analysis/complex/upper_half_plane.lean

@@ -159,4 +159,13 @@ begin
   ring,
 end
 
+lemma c_mul_im_sq_le_norm_sq_denom (z : ℍ) (g : SL(2, ℝ)) :
+  ((↑ₘg 1 0 : ℝ) * (z.im))^2 ≤ complex.norm_sq (denom g z) :=
+begin
+  let c := (↑ₘg 1 0 : ℝ),
+  let d := (↑ₘg 1 1 : ℝ),
+  calc (c * z.im)^2 ≤ (c * z.im)^2 + (c * z.re + d)^2 : by nlinarith
+                ... = complex.norm_sq (denom g z) : by simp [complex.norm_sq]; ring,
+end
+
 end upper_half_plane

src/data/int/basic.lean

@@ -221,6 +221,9 @@ le_sub_iff_add_le
 lemma abs_le_one_iff {a : ℤ} : |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1 :=
 by rw [le_iff_lt_or_eq, abs_lt_one_iff, abs_eq (@zero_le_one ℤ _)]
 
+lemma one_le_abs {z : ℤ} (h₀: z ≠ 0) : 1 ≤ |z| :=
+add_one_le_iff.mpr (abs_pos.mpr h₀)
+
 @[elab_as_eliminator] protected lemma induction_on {p : ℤ → Prop}
   (i : ℤ) (hz : p 0) (hp : ∀ i : ℕ, p i → p (i + 1)) (hn : ∀ i : ℕ, p (-i) → p (-i - 1)) : p i :=
 begin
@@ -1290,6 +1293,18 @@ begin
   { exact is_unit_one.neg }
 end
 
+lemma eq_one_or_neg_one_of_mul_eq_one {z w : ℤ} (h : z * w = 1) : z = 1 ∨ z = -1 :=
+is_unit_iff.mp (is_unit_of_mul_eq_one z w h)
+
+lemma eq_one_or_neg_one_of_mul_eq_one' {z w : ℤ} (h : z * w = 1) :
+  (z = 1 ∧ w = 1) ∨ (z = -1 ∧ w = -1) :=
+begin
+  have h' : w * z = 1 := (mul_comm z w) ▸ h,
+  rcases eq_one_or_neg_one_of_mul_eq_one h with rfl | rfl;
+  rcases eq_one_or_neg_one_of_mul_eq_one h' with rfl | rfl;
+  tauto,
+end
+
 theorem is_unit_iff_nat_abs_eq {n : ℤ} : is_unit n ↔ n.nat_abs = 1 :=
 by simp [nat_abs_eq_iff, is_unit_iff]
 

src/data/int/cast.lean

@@ -143,6 +143,10 @@ by rw [bit1, cast_add, cast_one, cast_bit0]; refl
 
 lemma cast_two [ring α] : ((2 : ℤ) : α) = 2 := by simp
 
+lemma cast_three [ring α] : ((3 : ℤ) : α) = 3 := by simp
+
+lemma cast_four [ring α] : ((4 : ℤ) : α) = 4 := by simp
+
 theorem cast_mono [ordered_ring α] : monotone (coe : ℤ → α) :=
 begin
   intros m n h,
@@ -177,22 +181,49 @@ by rw [← cast_zero, cast_lt]
 @[simp] theorem cast_lt_zero [ordered_ring α] [nontrivial α] {n : ℤ} : (n : α) < 0 ↔ n < 0 :=
 by rw [← cast_zero, cast_lt]
 
-@[simp, norm_cast] theorem cast_min [linear_ordered_ring α] {a b : ℤ} :
-  (↑(min a b) : α) = min a b :=
+section linear_ordered_ring
+
+variables [linear_ordered_ring α] {a b : ℤ} (n : ℤ)
+
+@[simp, norm_cast] theorem cast_min : (↑(min a b) : α) = min a b :=
 monotone.map_min cast_mono
 
-@[simp, norm_cast] theorem cast_max [linear_ordered_ring α] {a b : ℤ} :
-  (↑(max a b) : α) = max a b :=
+@[simp, norm_cast] theorem cast_max : (↑(max a b) : α) = max a b :=
 monotone.map_max cast_mono
 
-@[simp, norm_cast] theorem cast_abs [linear_ordered_ring α] {q : ℤ} :
-  ((|q| : ℤ) : α) = |q| :=
+@[simp, norm_cast] theorem cast_abs : ((|a| : ℤ) : α) = |a| :=
 by simp [abs_eq_max_neg]
 
-lemma cast_nat_abs {R : Type*} [linear_ordered_ring R] : ∀ (n : ℤ), (n.nat_abs : R) = |n|
-| (n : ℕ) := by simp only [int.nat_abs_of_nat, int.cast_coe_nat, nat.abs_cast]
-| -[1+n]  := by simp only [int.nat_abs, int.cast_neg_succ_of_nat, abs_neg,
-                           ← nat.cast_succ, nat.abs_cast]
+lemma cast_one_le_of_pos (h : 0 < a) : (1 : α) ≤ a :=
+by exact_mod_cast int.add_one_le_of_lt h
+
+lemma cast_le_neg_one_of_neg (h : a < 0) : (a : α) ≤ -1 :=
+by exact_mod_cast int.le_sub_one_of_lt h
+
+lemma nneg_mul_add_sq_of_abs_le_one {x : α} (hx : |x| ≤ 1) :
+  (0 : α) ≤ n * x + n * n :=
+begin
+  have hnx : 0 < n → 0 ≤ x + n := λ hn, by
+  { convert add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn),
+    rw add_left_neg, },
+  have hnx' : n < 0 → x + n ≤ 0 := λ hn, by
+  { convert add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn),
+    rw add_right_neg, },
+  rw [← mul_add, mul_nonneg_iff],
+  rcases lt_trichotomy n 0 with h | rfl | h,
+  { exact or.inr ⟨by exact_mod_cast h.le, hnx' h⟩, },
+  { simp [le_total 0 x], },
+  { exact or.inl ⟨by exact_mod_cast h.le, hnx h⟩, },
+end
+
+lemma cast_nat_abs : (n.nat_abs : α) = |n| :=
+begin
+  cases n,
+  { simp, },
+  { simp only [int.nat_abs, int.cast_neg_succ_of_nat, abs_neg, ← nat.cast_succ, nat.abs_cast], },
+end
+
+end linear_ordered_ring
 
 lemma coe_int_dvd [comm_ring α] (m n : ℤ) (h : m ∣ n) :
   (m : α) ∣ (n : α) :=