Twisting the coefficients of a Dirichlet series by a power of the index

Multiplying the n-th coefficient of a Dirichlet series by n ^ (-z) translates the series by z: the n-th term becomes f n * n ^ (-z) / n ^ s = f n / n ^ (s + z), so the twisted series at s is the original one at s + z. The identity is termwise, hence needs no convergence hypothesis; at a point where neither series converges both sides are Mathlib's junk value 0.

The purely imaginary parameters z = -u * I are the ones a Hecke character twisted by N(I) ^ (i u) produces. They translate the series in the imaginary (vertical) direction, so a pole of the original series at s = 1 becomes a pole of the twisted one at s = 1 + i u.

Main results

• TauCeti.LSeries.term_mul_natCast_cpow_neg and TauCeti.LSeries.LSeries_mul_natCast_cpow_neg: the term and the value of the twisted series at s are those of the original series at s + z.

theorem TauCeti.LSeries.term_mul_natCast_cpow_neg (f : ℕ → ℂ) (z s : ℂ) (n : ℕ) : LSeries.term (fun (n : ℕ) => f n * ↑n ^ (-z)) s n = LSeries.term f (s + z) n

Twisting the n-th coefficient of a Dirichlet series by n ^ (-z) translates its n-th term by z.

theorem TauCeti.LSeries.LSeries_mul_natCast_cpow_neg (f : ℕ → ℂ) (z s : ℂ) : LSeries (fun (n : ℕ) => f n * ↑n ^ (-z)) s = LSeries f (s + z)

Twisting a Dirichlet series by a power of the index translates it. The series of the coefficients f n * n ^ (-z) at s is the series of f at s + z.