Bounds for modular forms

All of the lemmas formerly defined here (truncatedFundamentalDomain, the family of exists_bound_* lemmas, ModularFormClass.exists_bound, CuspFormClass.exists_bound, qExpansion_isBigO, …) have been upstreamed into Mathlib.NumberTheory.ModularForms.Bounds, phrased there for an arithmetic Γ : Subgroup (GL (Fin 2) ℝ). This file is now a re-export to keep the historical import path working.