Conjugating Dirichlet series

Coefficientwise complex conjugation reflects a Dirichlet series across the real axis. This file records the termwise identity, its effect on absolute convergence and sums, and invariance of the absolute-convergence abscissa. These results apply to arbitrary complex coefficients, including local Euler factors. The value identity also holds at nonsummable inputs, where both series have Mathlib's totalized value zero.

The construction uses Mathlib's LSeries.term and the continuous-star infinite-sum API.

@[simp]

theorem TauCeti.LSeries.term_star (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : LSeries.term (star f) ((starRingEnd ℂ) s) n = star (LSeries.term f s n)

Conjugating the coefficients and the argument conjugates each Dirichlet-series term.

@[simp]

theorem TauCeti.LSeries.LSeriesSummable_star_iff (f : ℕ → ℂ) (s : ℂ) : LSeriesSummable (star f) ((starRingEnd ℂ) s) ↔ LSeriesSummable f s

Reflection preserves absolute convergence of a Dirichlet series.

@[simp]

theorem TauCeti.LSeries.LSeriesHasSum_star_iff (f : ℕ → ℂ) (s a : ℂ) : LSeriesHasSum (star f) ((starRingEnd ℂ) s) ((starRingEnd ℂ) a) ↔ LSeriesHasSum f s a

Conjugating coefficients and reflecting the argument conjugates a prescribed Dirichlet-series sum.

@[simp]

theorem TauCeti.LSeries.LSeries_star (f : ℕ → ℂ) (s : ℂ) : LSeries (star f) ((starRingEnd ℂ) s) = star (LSeries f s)

The totalized value of the conjugate Dirichlet series is the conjugate value. No convergence hypothesis is needed.

@[simp]

theorem TauCeti.LSeries.abscissaOfAbsConv_star (f : ℕ → ℂ) : LSeries.abscissaOfAbsConv (star f) = LSeries.abscissaOfAbsConv f

Coefficientwise conjugation does not change the abscissa of absolute convergence.