Commit 2025-12-15 10:15 37c079e4

View on Github →

feat(NumberTheory/EisensteinSeries/E2): Define the Eisenstein series E2 (#32584) We define the Eisenstein series E2 and prove some basic results which will be needed in #32585 to prove how it transforms under the slash action of SL2.

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Defs.lean

added def EisensteinSeries.D2

added theorem EisensteinSeries.D2_S

added theorem EisensteinSeries.D2_T

added theorem EisensteinSeries.D2_inv

added theorem EisensteinSeries.D2_mul

added theorem EisensteinSeries.D2_one

added def EisensteinSeries.E2

added def EisensteinSeries.G2

added def EisensteinSeries.e2Summand

added theorem EisensteinSeries.e2Summand_even

added theorem EisensteinSeries.e2Summand_summable

added theorem EisensteinSeries.e2Summand_zero_eq_two_riemannZeta_two

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

added theorem EisensteinSeries.G2_eq_tsum_cexp

added theorem EisensteinSeries.G2_eq_tsum_symmetricIco

added theorem EisensteinSeries.hasSum_e2Summand_symmetricIcc

added theorem EisensteinSeries.hasSum_e2Summand_symmetricIco

added theorem EisensteinSeries.summable_e2Summand_symmetricIcc

added theorem EisensteinSeries.summable_e2Summand_symmetricIco

added theorem EisensteinSeries.tendsto_e2Summand_atTop_nhds_zero

Modified Mathlib/Topology/Algebra/InfiniteSum/ConditionalInt.lean

added theorem HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc

added theorem Summable.tendsto_zero_of_even_summable_symmetricIcc

deleted theorem SummationFilter.HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc

added theorem SummationFilter.multipliable_symmetricIco_of_multipliable_symmetricIcc

deleted theorem SummationFilter.multipliable_symmetricIco_of_multiplible_symmetricIcc