Commit 2026-01-28 16:26 7cccd8a4

View on Github →

feat(NumberTheory/ModularForms/EisensteinSeries/E2/Transform): E2 under the action of SL2 (#32585) We show how E2 transforms under the slash action of SL2.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Interval.lean

added theorem Finset.prod_Ico_int_div

Modified Mathlib/Analysis/Complex/IntegerCompl.lean

deleted theorem Complex.UpperHalfPlane.coe_mem_integerComplement

deleted theorem Complex.UpperHalfPlane.int_div_mem_integerComplement

added theorem UpperHalfPlane.coe_mem_integerComplement

added theorem UpperHalfPlane.int_div_mem_integerComplement

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

deleted theorem Summable_cotTerm

added theorem summable_cotTerm

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

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

added theorem EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear

added theorem EisensteinSeries.summable_right_one_div_linear_sub_one_div_linear_succ

added theorem EisensteinSeries.tendsto_double_sum_S_act

added theorem EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq

added theorem EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero

added theorem EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act

added theorem EisensteinSeries.tsum_symmetricIco_tsum_sub_eq

added theorem EisensteinSeries.tsum_tsum_symmetricIco_sub_eq

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

added theorem EisensteinSeries.E2_slash_action

added theorem EisensteinSeries.G2Term_prod_summable

added theorem EisensteinSeries.G2Term_summable

added theorem EisensteinSeries.G2_S_action_eq_tsum_G2Term

added theorem EisensteinSeries.G2_S_transform

added theorem EisensteinSeries.G2_T_transform

added theorem EisensteinSeries.G2_eq_tsum_G2Term

added theorem EisensteinSeries.G2_slash_action

added theorem EisensteinSeries.aux_identity

added theorem EisensteinSeries.tsum_G2Term_eq_tsum'

added theorem EisensteinSeries.tsum_G2Term_eq_tsum

added def EisensteinSeries.δ

added theorem EisensteinSeries.δ_eq

added theorem EisensteinSeries.δ_eq_two

added theorem EisensteinSeries.δ_eventually_cofinite

Modified Mathlib/Order/Filter/AtTopBot/Archimedean.lean

added theorem PNat.tendsto_comp_val_iff