Theorems · Theorem · number theory

DirichletCharacter.differentiableAt_completedLFunction

∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ),
  s ≠ 0 ∨ N ≠ 1 → s ≠ 1 ∨ χ ≠ 1 → DifferentiableAt ℂ (DirichletCharacter.completedLFunction χ) s

The completed L-function of a Dirichlet character is differentiable, with the following exceptions: at s = 1 if χ is the trivial character (to any modulus); and at s = 0 if the modulus is 1. This result is best possible. Note both χ and s are explicit arguments: we will always be able to infer one or other of them from the hypotheses, but it's not clear which!

Defined in

Mathlib.NumberTheory.LSeries.DirichletContinuation

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZero