Add(NumberTheory/ModularForms/Identities): periods of modular forms. (#12601)

Add some basic results about `ModularGroup.T` relating to slash invariant forms of level Gamma(N) and moving elements into verticalStrips. Needed for #12456
 


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

Author: CBirkbeck

Mathlib.lean

@@ -3115,6 +3115,7 @@ 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.Identities
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

@@ -106,6 +106,23 @@ lemma subset_verticalStrip_of_isCompact {K : Set ℍ} (hK : IsCompact K) :
   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⟩⟩
 
+theorem ModularGroup_T_zpow_mem_verticalStrip (z : ℍ) {N : ℕ} (hn : 0 < N) :
+    ∃ n : ℤ, ModularGroup.T ^ (N * n) • z ∈ verticalStrip N z.im := by
+  let n := Int.floor (z.re/N)
+  use -n
+  rw [modular_T_zpow_smul z (N * -n)]
+  refine ⟨?_, (by simp only [mul_neg, Int.cast_neg, Int.cast_mul, Int.cast_natCast, vadd_im,
+    le_refl])⟩
+  have h : (N * (-n : ℝ) +ᵥ z).re = -N * Int.floor (z.re / N) + z.re := by
+    simp only [Int.cast_natCast, mul_neg, vadd_re, neg_mul]
+  norm_cast at *
+  rw [h, add_comm]
+  simp only [neg_mul, Int.cast_neg, Int.cast_mul, Int.cast_natCast, ge_iff_le]
+  have hnn : (0 : ℝ) < (N : ℝ) := by norm_cast at *
+  have h2 : z.re + -(N * n) =  z.re - n * N := by ring
+  rw [h2, abs_eq_self.2 (Int.sub_floor_div_mul_nonneg (z.re : ℝ) hnn)]
+  apply (Int.sub_floor_div_mul_lt (z.re : ℝ) hnn).le
+
 end strips
 
 /-- A continuous section `ℂ → ℍ` of the natural inclusion map, bundled as a `PartialHomeomorph`. -/

Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

@@ -88,6 +88,14 @@ theorem Gamma_zero_bot : Gamma 0 = ⊥ := by
     simp [h]
 #align Gamma_zero_bot Gamma_zero_bot
 
+lemma ModularGroup_T_pow_mem_Gamma (N M : ℤ) (hNM : N ∣ M) :
+    (ModularGroup.T ^ M) ∈ _root_.Gamma (Int.natAbs N) := by
+  simp only [Gamma_mem, Fin.isValue, ModularGroup.coe_T_zpow, of_apply, cons_val', cons_val_zero,
+    empty_val', cons_val_fin_one, Int.cast_one, cons_val_one, head_cons, head_fin_const,
+    Int.cast_zero, and_self, and_true, true_and]
+  refine Iff.mpr (ZMod.intCast_zmod_eq_zero_iff_dvd M (Int.natAbs N)) ?_
+  simp only [Int.natCast_natAbs, abs_dvd, hNM]
+
 /-- The congruence subgroup of `SL(2, ℤ)` of matrices whose lower left-hand entry reduces to zero
 modulo `N`. -/
 def Gamma0 (N : ℕ) : Subgroup SL(2, ℤ) where

Mathlib/NumberTheory/ModularForms/Identities.lean

@@ -0,0 +1,39 @@
+/-
+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.SlashInvariantForms
+import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
+
+/-!
+# Identities of ModularForms and SlashInvariantForms
+Collection of useful identities of modular forms.
+-/
+
+noncomputable section
+
+open ModularForm UpperHalfPlane Matrix
+
+namespace SlashInvariantForm
+
+/- TODO: Once we have cusps, do this more generally, same below. -/
+theorem vAdd_width_periodic (N : ℕ) (k n : ℤ) (f : SlashInvariantForm (Gamma N) k) (z : ℍ) :
+    f (((N * n) : ℝ) +ᵥ z) = f z := by
+  norm_cast
+  rw [← modular_T_zpow_smul z (N * n)]
+  have Hn := (ModularGroup_T_pow_mem_Gamma N (N * n) (by simp))
+  simp only [zpow_natCast, Int.natAbs_ofNat] at Hn
+  convert (SlashInvariantForm.slash_action_eqn' k (Gamma N) f ⟨((ModularGroup.T ^ (N * n))), Hn⟩ z)
+  unfold SpecialLinearGroup.coeToGL
+  simp only [Fin.isValue, ModularGroup.coe_T_zpow (N * n), of_apply, cons_val', cons_val_zero,
+    empty_val', cons_val_fin_one, cons_val_one, head_fin_const, Int.cast_zero, zero_mul, head_cons,
+    Int.cast_one, zero_add, one_zpow, one_mul]
+
+theorem T_zpow_width_invariant (N : ℕ) (k n : ℤ) (f : SlashInvariantForm (Gamma N) k) (z : ℍ) :
+    f (((ModularGroup.T ^ (N * n))) • z) = f z := by
+  rw [modular_T_zpow_smul z (N * n)]
+  simpa only [Int.cast_mul, Int.cast_natCast] using vAdd_width_periodic N k n f z
+
+end SlashInvariantForm