feat: define the Eisenstein Series E2

[CBirkbeck]

This PR continues the work from #24822.

Original PR: #24822

• depends on : Eisenstein q exp identity #27606
• depends on: Ixx summation filters #30380

[CBirkbeck]

Comments from Original PR #24822

This section contains 1 comment(s) from the original PR, excluding bot comments.

---

@github-actions (2025-05-12 20:43 UTC):

PR summary e7617962a5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2 (new file)	2495

---

Declarations diff

+ Asymptotics.IsBigO.map
+ Asymptotics.IsBigO.nat_of_int
+ D2
+ E2
+ Eis_isBigO
+ G2
+ G2_summable_aux
+ abs_le_left_of_norm
+ abs_le_right_of_norm
+ e2Summand
+ e2Summand_summable
+ le_left_of_norm
+ le_right_of_norm
+ linear_bigO
+ linear_bigO2
+ linear_bigO_pow
+ norm_symm
+ pnat_div_upper
+ summable_hammerTime

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[github-actions]

PR summary 61e5c4c0d3

Import changes exceeding 2%

%	File
+11.27%	Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
+5.13%	Mathlib.NumberTheory.TsumDivsorsAntidiagonal
+19.15%	Mathlib.Order.Filter.AtTopBot.Finset

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.Filter.AtTopBot.Finset	590	703	+113 (+19.15%)
Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion	2520	2804	+284 (+11.27%)
Mathlib.NumberTheory.TsumDivsorsAntidiagonal	1597	1679	+82 (+5.13%)

Import changes for all files

Files	Import difference
8 files Mathlib.RingTheory.MvPowerSeries.Evaluation Mathlib.RingTheory.MvPowerSeries.LinearTopology Mathlib.RingTheory.MvPowerSeries.PiTopology Mathlib.RingTheory.MvPowerSeries.Substitution Mathlib.RingTheory.PowerSeries.Evaluation Mathlib.RingTheory.PowerSeries.PiTopology Mathlib.RingTheory.PowerSeries.Substitution Mathlib.Topology.Algebra.InfiniteSum.Module	1
6 files Mathlib.Topology.Algebra.InfiniteSum.Constructions Mathlib.Topology.Algebra.InfiniteSum.NatInt Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.Topology.Algebra.InfiniteSum.Order Mathlib.Topology.Algebra.InfiniteSum.Ring Mathlib.Topology.Algebra.InfiniteSum.UniformOn	2
Mathlib.NumberTheory.TsumDivsorsAntidiagonal	82
Mathlib.Order.Filter.AtTopBot.Finset	113
Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion	284
Mathlib.NumberTheory.IntervalSums (new file)	999
Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (new file)	2617
Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (new file)	2807
Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (new file)	2809

---

Declarations diff

+ D2
+ D2_S
+ D2_T
+ D2_inv
+ D2_mul
+ D2_one
+ E2
+ E2_slash_action
+ EisensteinSeries.q_expansion_bernoulli
+ EisensteinSeries.q_expansion_riemannZeta
+ Filter.tendsto_of_div_tendsto_one
+ Finset.Icc_succ_succ
+ Finset.Ico_succ_succ
+ Finset.prod_Icc_eq_prod_Ico_succ
+ Finset.prod_Icc_mul_endpoints
+ Finset.prod_Icc_of_even_eq_range
+ Finset.tendsto_Ico_atTop_atTop
+ Finset.tendsto_Ioc_atTop_atTop
+ G2
+ G2Term
+ G2_Ico_cauchySeq
+ G2_S_transform
+ G2_T_transform
+ G2_cauchySeq
+ G2_eq_tsum_G2Term
+ G2_eq_tsum_IcoFilter
+ G2_q_exp
+ G2_slash_action
+ HasProd_IcoFilter_iff
+ IcoFilter
+ IocFilter
+ Summable_IccFilter_G2_Ico
+ Summable_symCondInt_G2
+ aux_isBigO_linear
+ e2Summand
+ e2Summand_even
+ e2Summand_summable
+ e2Summand_zero_eq_two_riemannZeta_two
+ eisSummand_of_gammaSet_eq_divIntMap
+ instance : (IcoFilter G).NeBot
+ instance : (IcoFilter ℤ).LeAtTop
+ instance : (IocFilter G).NeBot
+ instance : (IocFilter ℤ).LeAtTop
+ instance : (symmetricConditional G).LeAtTop
+ instance : (symmetricConditional G).NeBot
+ int_div_upperHalfPlane_mem_integerComplement
+ isBigO_linear_add_const_vec
+ isLittleO_const_vec
+ linear_inv_isBigO_right'
+ linear_isTheta_right'
+ multipliable_IcoFilter_of_multiplible_symmetricConditional
+ multipliable_pnat_iff_multipliable_nat
+ pnat_div_upperHalfPlane_im_pos
+ slash_S_apply
+ summable_inv_of_isBigO_rpow_norm_inv
+ summable_linear_add_mul_linear_add
+ summable_linear_mul_linear
+ summable_one_div_linear_sub_one_div_linear
+ summable_prod_eisSummand
+ swap
+ swap_apply
+ swap_equiv
+ swap_involutive
+ symCondInt
+ symmetricConditional
+ symmetricConditional_eq_map_Icc
+ symmetricConditional_eq_map_Icc_nat
+ symmetricConditional_eq_map_Ioo
+ symmetricConditional_le_Conditional
+ tendsto_zero_geometric_tsum_pnat
+ tendsto_zero_inv_linear
+ tendsto_zero_inv_linear_sub
+ tprod_eq_of_le
+ tprod_eq_of_multipliable_unconditional
+ tprod_int_eq_zero_mul_tprod_pnat
+ tprod_symmetricConditional_eq_tprod_IcoFilter
+ tsum_IcoFilter_eq_zero
+ tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries
+ tsum_eisSummand_eq_tsum_sigma_cexp
+ vec_add_const_isTheta

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).