Theorems · Definition · number theory

DirichletCharacter.LFunction

{N : ℕ} → [NeZero N] → DirichletCharacter ℂ N → ℂ → ℂ

The unique meromorphic function ℂ → ℂ which agrees with ∑' n : ℕ, χ n / n ^ s wherever the latter is convergent. This is constructed as a linear combination of Hurwitz zeta functions. Note that this is not the same as LSeries χ: they agree in the convergence range, but LSeries χ s is defined to be 0 if re s ≤ 1.

Defined in

Mathlib.NumberTheory.LSeries.DirichletContinuation

Cited by

23 results in Mathlib

Foundations

Depth 305 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NeZero