Reflection of continued Dirichlet L-functions

Complex conjugation interchanges the continued L-functions of a Dirichlet character and its inverse. We extend the Dirichlet-series identity to the punctured plane by analytic uniqueness, and across 1 for nonprincipal characters. Thus the result applies to the continued function, not the totalized Dirichlet series outside its convergence half-plane.

For quadratic characters this gives reflection of zeros across the real axis and reality at real arguments away from the possible principal-character pole at 1, including the interval to its left used in real-zero estimates. We also give the reflection identity for derivatives and their real-axis specialization.

The continuation is Mathlib's DirichletCharacter.LFunction; coefficientwise reflection uses TauCeti.LSeries.LSeries_star.

theorem DirichletCharacter.LFunction_inv_conj {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : s ≠ 1 ∨ χ ≠ 1) : LFunction χ⁻¹ ((starRingEnd ℂ) s) = (starRingEnd ℂ) (LFunction χ s)

Reflection interchanges a character and its inverse. At the possible pole 1 we require that the character be nonprincipal.

@[simp]

theorem DirichletCharacter.LFunction_inv_conj_eq_zero_iff {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ) : LFunction χ⁻¹ ((starRingEnd ℂ) s) = 0 ↔ LFunction χ s = 0

Reflection interchanges the zeros of the continued L-functions of inverse characters.

theorem DirichletCharacter.deriv_LFunction_inv_conj {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : s ≠ 1 ∨ χ ≠ 1) : deriv (LFunction χ⁻¹) ((starRingEnd ℂ) s) = (starRingEnd ℂ) (deriv (LFunction χ) s)

The derivatives of the continued L-functions of inverse characters satisfy the same reflection identity wherever the L-functions are holomorphic.

@[simp]

theorem DirichletCharacter.LFunction_conj_of_isQuadratic {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : MulChar.IsQuadratic χ) {s : ℂ} (hs : s ≠ 1 ∨ χ ≠ 1) : LFunction χ ((starRingEnd ℂ) s) = (starRingEnd ℂ) (LFunction χ s)

A quadratic character's continued L-function commutes with conjugation away from its possible pole at 1.

@[simp]

theorem DirichletCharacter.deriv_LFunction_conj_of_isQuadratic {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : MulChar.IsQuadratic χ) {s : ℂ} (hs : s ≠ 1 ∨ χ ≠ 1) : deriv (LFunction χ) ((starRingEnd ℂ) s) = (starRingEnd ℂ) (deriv (LFunction χ) s)

The derivative of a quadratic character's continued L-function commutes with conjugation wherever the L-function is holomorphic.

@[simp]

theorem DirichletCharacter.LFunction_im_eq_zero_of_isQuadratic {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : MulChar.IsQuadratic χ) (x : ℝ) (hx : x ≠ 1 ∨ χ ≠ 1) : (LFunction χ ↑x).im = 0

The continued L-function of a quadratic character is real at real arguments away from its possible pole at 1, not only in the half-plane of convergence.

@[simp]

theorem DirichletCharacter.deriv_LFunction_im_eq_zero_of_isQuadratic {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : MulChar.IsQuadratic χ) (x : ℝ) (hx : x ≠ 1 ∨ χ ≠ 1) : (deriv (LFunction χ) ↑x).im = 0

The derivative of a quadratic character's continued L-function is real at real arguments wherever the L-function is holomorphic.

@[simp]

theorem DirichletCharacter.LFunction_conj_eq_zero_iff_of_isQuadratic {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : MulChar.IsQuadratic χ) (s : ℂ) : LFunction χ ((starRingEnd ℂ) s) = 0 ↔ LFunction χ s = 0

The zeros of a quadratic L-function are invariant under reflection across the real axis.