feat (NumberTheory/ZetaFunctions): Hurwitz zeta function

[loefflerd]

This is a draft PR which will be split into many chunks for final submission

• Abstract functional-equation argument for Mellin transforms
• Refactor Riemann zeta using this
• Hurwitz zeta functions

See #12035 for an issue page tracking progress on getting this into mathlib.

---

• [x] depends on: #11069
• [x] depends on: #11176
• [x] depends on: #11150
• [x] depends on: #11190

[github-actions[bot]]

PR summary b43966756c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
3 files Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.Fourier.ZMod	1
Mathlib.NumberTheory.LSeries.DirichletContinuation2	2052
Mathlib.NumberTheory.LSeries.ZModFE	2184
Mathlib.NumberTheory.LSeries.DirichletFuncEq	2188

---

Declarations diff

+ Even.iff_coe + Even.not_odd + LFunction + LFunction_eq_LSeries + LFunction_mod_one + LFunction_neg_two_mul_nat_add_one + LFunction_neg_two_mul_nat_sub_one + Nat.residueClassesEquiv + Nat.sumByResidueClasses + Odd.iff_coe + Odd.not_even + completedDualLFunction_mod_one + completedLFunction_eq + completedLFunction_mod_one + completedLFunction_one_sub + completedLFunction_one_sub_eq + completedLFunction₀ + dft_even + dft_odd + differentiableAt_LFunction + differentiableAt_completedDualLFunction + differentiable_LFunction + differentiable_completedDualLFunction + differentiable_completedLFunction₀ + dualLFunction_eq_LSeries_dft + dualLFunction_eq_LSeries_gaussSum + dualLFunction_mod_one + gammaFactor_def + gammaFactor_dft + gammaFactor_inv + gaussSum_mod_one + map_zero' + not_even_and_odd + rootNumber ++ Even.LFunction_neg_two_mul_nat_add_one ++ LFunction_def_signed ++ Odd.LFunction_neg_two_mul_nat_sub_one ++ completedDualLFunction ++ completedDualLFunction_eq ++ completedLFunction_modOne_eq ++ completedLFunction_one_sub_eq_dual ++ differentiable_dualLFunction ++ dualLFunction ++ dualLFunction_def_signed ++ dualLFunction_eq ++ dualLFunction_eq_completed_div_gammaFactor +++ LFunction_eq_completed_div_gammaFactor +++ completedLFunction +++ differentiableAt_completedLFunction +++ differentiable_completedLFunction +++ gammaFactor

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.

[loefflerd]

I am closing this PR, since it is superseded by #16967.