Commit 2025-06-26 13:35 f541cd9e

View on Github →

feat: Add more Summability results needed for Eisenstein series. (#26005) This PR continues the work from #25393. Original PR: https://github.com/leanprover-community/mathlib4/pull/25393

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Defs.lean

added theorem Asymptotics.IsBigO.comp_neg_int

Modified Mathlib/Analysis/Complex/Asymptotics.lean

added theorem Int.cast_complex_isTheta_cast_real

Modified Mathlib/Analysis/Normed/Group/Bounded.lean

added theorem tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding'

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

added theorem EisensteinSeries.abs_le_left_of_norm

added theorem EisensteinSeries.abs_le_right_of_norm

added theorem EisensteinSeries.linear_inv_isBigO_left

added theorem EisensteinSeries.linear_inv_isBigO_right

added theorem EisensteinSeries.linear_isTheta_left

added theorem EisensteinSeries.linear_isTheta_right

added theorem EisensteinSeries.linear_left_summable

added theorem EisensteinSeries.linear_right_summable

added theorem EisensteinSeries.norm_symm

added theorem EisensteinSeries.summable_inv_of_isBigO_rpow_inv

added theorem EisensteinSeries.summable_linear_sub_mul_linear_add

Modified scripts/migrate_to_fork.py