Commit 2025-06-09 13:00 51f395a1

View on Github →

chore : Split summability results for Eisenstein series into own file (#25443) I am going to be adding some more summability results for Eisenstein series (for example for E2), so it makes sence for this to all be in a separate file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean

Created Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean

added theorem EisensteinSeries.auxbound1

added theorem EisensteinSeries.auxbound2

added theorem EisensteinSeries.div_max_sq_ge_one

added theorem EisensteinSeries.norm_eq_max_natAbs

added def EisensteinSeries.r1

added theorem EisensteinSeries.r1_aux_bound

added theorem EisensteinSeries.r1_eq

added theorem EisensteinSeries.r1_pos

added def EisensteinSeries.r

added theorem EisensteinSeries.r_lower_bound_on_verticalStrip

added theorem EisensteinSeries.r_mul_max_le

added theorem EisensteinSeries.r_pos

added theorem EisensteinSeries.summable_one_div_norm_rpow

added theorem EisensteinSeries.summand_bound

added theorem EisensteinSeries.summand_bound_of_mem_verticalStrip

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean

deleted theorem EisensteinSeries.auxbound1

deleted theorem EisensteinSeries.auxbound2

deleted theorem EisensteinSeries.div_max_sq_ge_one

deleted theorem EisensteinSeries.norm_eq_max_natAbs

deleted def EisensteinSeries.r1

deleted theorem EisensteinSeries.r1_aux_bound

deleted theorem EisensteinSeries.r1_eq

deleted theorem EisensteinSeries.r1_pos

deleted def EisensteinSeries.r

deleted theorem EisensteinSeries.r_lower_bound_on_verticalStrip

deleted theorem EisensteinSeries.r_mul_max_le

deleted theorem EisensteinSeries.r_pos

deleted theorem EisensteinSeries.summable_one_div_norm_rpow

deleted theorem EisensteinSeries.summand_bound

deleted theorem EisensteinSeries.summand_bound_of_mem_verticalStrip