# Differentiability and derivatives of L-series #

## Main results #

We show that the

`LSeries`

of`f`

is differentiable at`s`

when`re s`

is greater than the abscissa of absolute convergence of`f`

(`LSeries.hasDerivAt`

) and that its derivative there is the negative of the`LSeries`

of the point-wise product`log * f`

(`LSeries.deriv`

).We prove similar results for iterated derivatives (

`LSeries.iteratedDeriv`

).We use this to show that

`LSeries f`

is holomorphic on the right half-plane of absolute convergence (`LSeries.analyticOnNhd`

).

## Implementation notes #

We introduce `LSeries.logMul`

as an abbreviation for the point-wise product `log * f`

, to avoid
the problem that this expression does not type-check.

### The derivative of an L-series #

The (point-wise) product of `log : ℕ → ℂ`

with `f`

.

## Equations

- LSeries.logMul f n = Complex.log ↑n * f n

## Instances For

The derivative of the terms of an L-series.

If `re s`

is greater than the abscissa of absolute convergence of `f`

, then the L-series
of `f`

is differentiable with derivative the negative of the L-series of the point-wise
product of `log`

with `f`

.

If `re s`

is greater than the abscissa of absolute convergence of `f`

, then
the derivative of this L-series at `s`

is the negative of the L-series of `log * f`

.

The derivative of the L-series of `f`

agrees with the negative of the L-series of
`log * f`

on the right half-plane of absolute convergence.

If the L-series of `f`

is summable at `s`

and `re s < re s'`

, then the L-series of the
point-wise product of `log`

with `f`

is summable at `s'`

.

The abscissa of absolute convergence of the point-wise product of `log`

and `f`

is the same as that of `f`

.

### Higher derivatives of L-series #

The abscissa of absolute convergence of the point-wise product of a power of `log`

and `f`

is the same as that of `f`

.

If `re s`

is greater than the abscissa of absolute convergence of `f`

, then
the `m`

th derivative of this L-series is `(-1)^m`

times the L-series of `log^m * f`

.

### The L-series is holomorphic #

The L-series of `f`

is complex differentiable in its open half-plane of absolute
convergence.

The L-series of `f`

is holomorphic on its open half-plane of absolute convergence.