[Merged by Bors] - feat(NumberTheory/ModularForms/EisensteinSeries): Update gammaSet

[CBirkbeck]

We redefine gammaSet to include vectors with non-trivial gcd. This is useful for giving the q-expansions of Eisenstein series at level one. Which can be seen here #27606 (these equivalences are used in tsum_prod_eisSummand_eq_riemannZeta_eisensteinSeries in the QExpansions file).

---

[github-actions]

PR summary d60062a692

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs	1851	1853	+2 (+0.11%)
Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence	2004	2006	+2 (+0.10%)

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable	1
3 files Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence	2

---

Declarations diff

+ divIntMap
+ finGcdMap
+ finGcdMap_div
+ finGcdMap_smul
+ gammaSetDivGcdEquiv
+ gammaSetDivGcdSigmaEquiv
+ gammaSetDivGcdSigmaEquiv_symm_eq
+ gammaSet_div_gcd
+ gammaSet_div_gcd_to_gammaSet10_bijection
+ gammaSet_eq_gcd_mul_divIntMap
+ gammaSet_one_const
+ gammaSet_one_mem_iff
+ isCoprime_div_gcd_div_gcd_of_gcd_ne_zero
+ mem_gammaSet_one
+ vecMulSL_gcd

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

[MichaelStollBayreuth]

Can you say what you are planning to use gammaSetN for? This would help figuring out how to set up the API. E.g., would gammaSetN 1 = gammaSet 1 0 be useful? or M • gammaSetN N = gammaSetN (M * N)?

A general remark: please check the naming convention; not all names adhere to it.
Also, the N in gammaSetN is a bit problematic, as N is the name of the argument and has no intrinsic mathematical meaning.

[CBirkbeck]

Can you say what you are planning to use gammaSetN for? This would help figuring out how to set up the API. E.g., would gammaSetN 1 = gammaSet 1 0 be useful? or M • gammaSetN N = gammaSetN (M * N)?

Sorry I tagged this in #27606 but didnt mention it on the description here. This is for the q-expansions of Eisenstein series of level one. Our general definition is sums over coprime pairs of integers, but to get the usual q-expansions at level one, one needs to relate this to the sum over all pairs of integers and then take out a riemannZeta factor. In doing this it seemed best to make this definition. But at the moment it doesn't need any more API than what is here really, since its just the equivalences that are mainly needed for all the tsums later.

[MichaelStollBayreuth]

I didn't find any application of your gammaSetWithGcd in the linked PRs, so I find it hard to judge what exactly would be needed here. I'm still wary of the promotion of the set to a type.

From what you mention above, I assume that you want something like

lemma foo {f : (Fin 2 → ℕ) → ℂ} {k : ℕ} (hk : 2 ≤ k) (h : ∀ (m : ℕ) n, f n = m ^ k * f (m • n)) (a : ℂ) : 
    HasSum f (a * riemannZeta k) ↔ HasSum (fun n : {n : Fin 2 → ℕ // IsCoprime (n 0) (n 1)} ↦ f n) a := ...

This should be doable without setting up gammaSetWithGcd in the first place. I'll try to come up with something.

[CBirkbeck]

So it is used in this PR: #27606, specifically, the equivalence is used to prove

lemma tsum_prod_eisSummand_eq_riemannZeta_eisensteinSeries {k : ℕ} (hk : 3 ≤ k) (z : ℍ) :
    ∑' (x : Fin 2 → ℤ), eisSummand k x z = (riemannZeta (k)) * (eisensteinSeries 𝟙 k z) := by

which is on line 265 of the QExpansion file (sorry I dont know how to link directly to a file).

Edit: Also the names aren't updated in this draft PR yet. So it still uses gammaSetN

[loefflerd]

Hi Chris,

With this PR, as currently written, we have two separate defs for "pairs with GCD = 1 and congruence condition a mod N" and "pairs with GCD = N and no congruence condition". Might it be better to have a single, more general definition "pairs with GCD = r and congruence condition a mod N"? This will make it much easier to generalize the q-expansion computation later to cover Eisenstein series of arbitrary level. I'm not saying we should necessarily do the q-exp computation in general levels from the start (the perfect is the enemy of the good, etc), just that we should bear in mind that it might come later so we shouldn't actively conspire against it.

[CBirkbeck]

Ok so I make gammaSet's more general now. They come with a gcd condition which should be enough for future aplications as well.

[loefflerd]

This looks pretty good now, just a few minor things I spotted while reading it.

[loefflerd]

LGTM now, thanks!

maintainer merge

[github-actions]

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

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success