Boundedness of Eisenstein series

All of the lemmas formerly defined here have been upstreamed into Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty; this file is now a re-export.