Holomorphic logarithms of ideal L-series

The exponential form of an Euler product determines a logarithm only modulo 2πi ℤ. It does not choose a branch: a branch is a single holomorphic function on a region, and choosing one needs the region to be simply connected as well as zero-free.

This file makes that choice for the norm-regrouped L-series of a general TauCeti.IdealArithmeticFunction on a zero-free region of absolute convergence, hence in particular for the coefficient function underlying TauCeti.EulerProductData. It also specializes the result to a completely multiplicative ideal weight, whose Euler product supplies nonvanishing automatically. The derivative of the chosen logarithm is the logarithmic derivative of the L-series — the same function for every choice of branch, since two branches differ by a locally constant multiple of 2πi.

Main results

• TauCeti.IdealArithmeticFunction.exists_differentiableOn_exp_eq_LSeries: a holomorphic logarithm for a norm-regrouped ideal coefficient function on a simply connected zero-free region of absolute convergence.
• TauCeti.MultiplicativeIdealWeight.exists_differentiableOn_exp_eq_LSeries: the branch, together with the identification of its derivative, for a completely multiplicative ideal weight.

theorem TauCeti.IdealArithmeticFunction.exists_differentiableOn_exp_eq_LSeries {K : Type u_1} [Field K] [NumberField K] (f : IdealArithmeticFunction K) {U : Set ℂ} (hUc : IsSimplyConnected U) (hUo : IsOpen U) (hconv : ∀ s ∈ U, Summable (idealTerm K f s)) (hzero : ∀ s ∈ U, LSeries (⇑((normCoeff K) f)) s ≠ 0) : ∃ (L : ℂ → ℂ), DifferentiableOn ℂ L U ∧ Set.EqOn (Complex.exp ∘ L) (LSeries ⇑((normCoeff K) f)) U ∧ ∀ s ∈ U, deriv L s = logDeriv (LSeries ⇑((normCoeff K) f)) s

A holomorphic logarithm after regrouping an ideal-indexed series by norm. Let U be a simply connected open set where the ideal-indexed series of f converges absolutely and its norm-regrouped L-series does not vanish. Then there is a holomorphic function L on U whose exponential is that L-series, and deriv L is its logarithmic derivative.

The zero-free hypothesis is necessary for a general coefficient function. For a completely multiplicative degree-one weight, the Euler product supplies it automatically.

theorem TauCeti.MultiplicativeIdealWeight.exists_differentiableOn_exp_eq_LSeries {K : Type u_1} [Field K] [NumberField K] (χ : MultiplicativeIdealWeight K) {U : Set ℂ} (hUc : IsSimplyConnected U) (hUo : IsOpen U) (hconv : ∀ s ∈ U, Summable (idealTerm K χ.toIdealArithmeticFunction s)) : ∃ (L : ℂ → ℂ), DifferentiableOn ℂ L U ∧ Set.EqOn (Complex.exp ∘ L) (LSeries ⇑((normCoeff K) χ.toIdealArithmeticFunction)) U ∧ ∀ s ∈ U, deriv L s = logDeriv (LSeries ⇑((normCoeff K) χ.toIdealArithmeticFunction)) s

A holomorphic logarithm of the L-series on a simply connected zero-free region. Let U be a simply connected open set at every point of which the ideal-indexed series converges absolutely. Then there is a holomorphic L on U with exp ∘ L the L-series, and deriv L is its logarithmic derivative.

Absolute convergence does two jobs: through the Euler product it makes the L-series zero-free on U, and through a point of U slightly to the left of each s it puts s strictly right of the abscissa of absolute convergence, which is what makes the L-series holomorphic there. Simple connectedness is what turns pointwise nonvanishing into a single branch.