[Merged by Bors] - feat(NumberTheory/EisensteinSeries/E2): Define the Eisenstein series E2

[CBirkbeck]

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.

---

[github-actions]

PR summary 789a3095b5

Import changes exceeding 2%

%	File
+52.79%	Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt	735	1123	+388 (+52.79%)

Import changes for all files

Files	Import difference
Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt	388
Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (new file)	2460
Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (new file)	2590

---

Declarations diff

+ D2
+ D2_S
+ D2_T
+ D2_inv
+ D2_mul
+ D2_one
+ E2
+ G2
+ G2_eq_tsum_cexp
+ G2_eq_tsum_symmetricIco
+ _root_.HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc
+ _root_.Summable.tendsto_zero_of_even_summable_symmetricIcc
+ e2Summand
+ e2Summand_even
+ e2Summand_summable
+ e2Summand_zero_eq_two_riemannZeta_two
+ hasSum_e2Summand_symmetricIcc
+ hasSum_e2Summand_symmetricIco
+ multipliable_symmetricIco_of_multipliable_symmetricIcc
+ summable_e2Summand_symmetricIcc
+ summable_e2Summand_symmetricIco
+ tendsto_e2Summand_atTop_nhds_zero
- HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc
- multipliable_symmetricIco_of_multiplible_symmetricIcc

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).

[loefflerd]

First instalment, more later

[loefflerd]

Here's some (not definitive) feedback on the second file. Overall I feel like it's a bit roundabout, like we keep taking 2 steps forward and 1 step back (establishing that a sequence tends to some limit & then deducing that it's Cauchy, etc)

[loefflerd]

This might help:

lemma tendsto_zero_of_summable_symmetricIcc {F : Type*} [NormedAddCommGroup F] [NormSMulClass ℤ F]
    {f : ℤ → F} (hf : Summable f (symmetricIcc ℤ)) (hs : f.Even) :
    Tendsto f atTop (𝓝 0) := by
  rw [tendsto_zero_iff_norm_tendsto_zero]
  obtain ⟨L, hL⟩ := hf
  rw [HasSum, symmetricIcc_filter, tendsto_map'_iff, Function.comp_def] at hL
  have := hL.sub (hL.comp (tendsto_atTop_add_const_right _ (-1) tendsto_id))
  simp only [id_eq, Int.reduceNeg, Function.comp_apply, sub_self, ← sub_eq_add_neg] at this
  rw [tendsto_zero_iff_norm_tendsto_zero] at this
  refine (mul_zero (_ : ℝ) ▸ this.const_mul 2⁻¹).congr' ?_
  filter_upwards [eventually_ge_atTop 1] with x hx
  have : Finset.Icc (-x) x = {x} ∪ {-x} ∪ Icc (-(x - 1)) (x - 1) := by
    ext
    simp only [mem_Icc, union_singleton, insert_union, singleton_union, mem_insert]
    omega
  rw [this, Finset.sum_union, Finset.sum_union, Finset.sum_singleton, Finset.sum_singleton,
    hs x, add_sub_assoc, sub_self, add_zero, ← two_zsmul, norm_smul, Int.norm_eq_abs,
    Int.cast_two, abs_two, inv_mul_cancel_left₀ two_ne_zero] <;>
  · simp only [union_singleton, disjoint_iff_ne, mem_insert, mem_singleton, mem_Icc]
    omega

[loefflerd]

See https://pastebin.com/GJ30AWGE for a suggestion about how to edit the Summable.lean file. You'll need to rename HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc in Topology.Algebra.InfiniteSum.ConditionalInt to _root_.HasProd.xxx, and fix the typo in the lemma following.

[loefflerd]

Looks good now!

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by loefflerd.

[loefflerd]

(Maintainers: CB has implemented the changes I wanted so please consider my "maintainer delegate" to be upgraded to "maintainer merge")

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Build failed (retrying...):

• Post-Build Step

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step