Commit 2024-03-04 09:02 ba66cf76

refactor(NumberTheory/LSeries/*): change type of argument to ℕ → ℂ, add LSeries.term + API etc. (#11111) See this thread on Zulip. The main point of this PR is to refactor LSeries and friends to use an argument f : ℕ → ℂ instead of f : ArithmeticFunction ℂ. Since I was at it anyway, I also did a few more things:

• Move the L-series stuff out of the ArithmeticFunction namespace. Use LSeries as a namespace for some of the declarations instead.
• Introduce LSeries.term f s n; this denotes the nth term in the L-series LSeries f s. This is defined to be zero for n = 0; otherwise it is the usual f n / n ^ s. Provide basic API for it.
• Re-write LSeries etc. in terms of LSeries.term. Attempt to isolate the meat of the proofs in suitable API lemmas for LSeries.term. Add some API (like congruence lemmas).
• Use s for the complex variable (in place of z or w; s and s' when two are required), following the notational convention in analytic number theory.
• Golf some proofs.
• Add some documentation (and modify existing docstrings to fit the changes).