[Merged by Bors] - Eisenstein series uniform convergence

[CBirkbeck]

We show that the sum defining an Eisenstein Series converges locally uniformly. This is the basis for later proving that they are holomorphic (see #11013 ) and bounded at infinity (see #12456), which combine to show they are modular forms (see #12604).

---

• depends on: [Merged by Bors] - feat: Boxes in locally finite ordered rings #10506
• depends on: [Merged by Bors] - Composing non_zero function with injective fun is non_zero #11244
• depends on: [Merged by Bors] - feat(Complex/UpperHalfPlane): add vertical strips #12443
• depends on : [Merged by Bors] - feat(Order/Interval/Finset/Box): add lemma #12444
• depends on: [Merged by Bors] - feat(Topology/Algebra/InfiniteSum/Real): Add partition lemma #12446
  

[loefflerd]

The main changes I made were:

• rather than writing max (x 0).natAbs ... each time, I used the handy fact that Fin 2 → ℤ has a pre-defined norm and it's the sup-norm, so we can just write ‖x‖.
• You had various lemmas involving Finset.box that depended on z; but I think it's better to gather together all the references to Finset.box into the proof of the single lemma

  lemma summable_one_div_norm_rpow {k : ℝ} (hk : 2 < k) :
      Summable fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k) := by

  which is hopefully interesting outside the context of this particular PR.
• I added an outline of the argument at the start of the file.

[CBirkbeck]

I didn't know we had this norm on tuples, which I think really makes it much cleaner, so thank you! and thanks for the extra doc strings, I usually only add then to defs, but I this is a good idea going forward. The only thing I changed (other than some short golf) was the name norm_def to norm_eq_max_natAbs as its maybe more standard?

[loefflerd]

Great – let's get this in!

Note to maintainers: the code is now kind of a joint effort, but Chris has carefully read the bits that I wrote, and vice versa, so I think we can count it all as being "reviewed".

maintainer merge

[github-actions]

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

[riccardobrasca]

Modulo Johan's comment LGTM, thanks!

bors d+

[mathlib-bors]

✌️ CBirkbeck can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[CBirkbeck]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style