[Merged by Bors] - feat(NumberTheory/ModularForms): the Dedekind Eta function

[CBirkbeck]

We define the Dedekind eta function in preparation for later relating it to Eisenstein series and the modular form Delta.

---

• depends on: [Merged by Bors] - feat(Topology/Algebra/InfiniteSum): use NormMulClass #28756

[github-actions]

PR summary 2c4da570e3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.ModularForms.DedekindEta (new file)	2409

---

Declarations diff

+ Summable.summable_log_norm_one_add
+ contDiff_qParam
+ differentiableAt_eta_of_mem_upperHalfPlaneSet
+ differentiable_qParam
+ eta
+ eta_ne_zero
+ eta_q
+ eta_q_eq_cexp
+ eta_q_eq_pow
+ isOpen_upperHalfPlaneSet
+ logDeriv_one_sub_cexp
+ logDeriv_one_sub_mul_cexp_comp
+ multipliableLocallyUniformlyOn_eta
+ one_sub_eta_q_ne_zero
+ qParam_ne_zero
+ summable_eta_q
+ tprod_one_add_ne_zero_of_summable
+ tsum_logDeriv_eta_q
+ upperHalfPlaneSet

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]

Here are a few quick thoughts (have to go get lunch now).

[loefflerd]

OK, that's it from me. Let's hope the mini-PR I spun off gets merged soon. Probably best I don't use my maintainer-merge powers until that has happened, but I will do so once it has (if I don't, remind me!)

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Topology/Algebra/InfiniteSum): use NormMulClass #28756
  By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[loefflerd]

I found some more trivial fixes (mostly just formatting and golfs). Feel free to fix or ignore as you prefer.

maintainer delegate

[github-actions]

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

[loefflerd]

Maintainers: I confirm all my comments are dealt with, so my "maintainer delegate" recommendation can become a "maintainer merge".

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success