Ok I think its ready for another review :)

I've edited it a bit myself and made some adjustments which I think make it cleaner. Is it OK with you if I push my version to your branch? You can always revert it again if you prefer your version.

I've edited it a bit myself and made some adjustments which I think make it cleaner. Is it OK with you if I push my version to your branch? You can always revert it again if you prefer your version.

Yes certainly, thank you!

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.

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?

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

Modulo Johan's comment LGTM, thanks!

bors d+

✌️ 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.

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style