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

@[reducible, inline]

noncomputable abbrev LSeries.logMul (f : ℕ → ℂ) (n : ℕ) : ℂ

The (point-wise) product of log : ℕ → ℂ with f.

theorem LSeries.hasDerivAt_term (f : ℕ → ℂ) (n : ℕ) (s : ℂ) : HasDerivAt (fun (z : ℂ) => term f z n) (-term (logMul f) s n) s

The derivative of the terms of an L-series.

theorem LSeries_hasDerivAt {f : ℕ → ℂ} {s : ℂ} (h : LSeries.abscissaOfAbsConv f < ↑s.re) : HasDerivAt (LSeries f) (-LSeries (LSeries.logMul f) s) s

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.

theorem LSeries_deriv {f : ℕ → ℂ} {s : ℂ} (h : LSeries.abscissaOfAbsConv f < ↑s.re) : deriv (LSeries f) s = -LSeries (LSeries.logMul f) s

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.

theorem LSeries_deriv_eqOn {f : ℕ → ℂ} : Set.EqOn (deriv (LSeries f)) (-LSeries (LSeries.logMul f)) {s : ℂ | LSeries.abscissaOfAbsConv f < ↑s.re}

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.

theorem LSeriesSummable_logMul_of_lt_re {f : ℕ → ℂ} {s : ℂ} (h : LSeries.abscissaOfAbsConv f < ↑s.re) : LSeriesSummable (LSeries.logMul f) s

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'.

@[simp]

theorem LSeries.abscissaOfAbsConv_logMul {f : ℕ → ℂ} : abscissaOfAbsConv (logMul f) = abscissaOfAbsConv f

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

@[simp]

theorem LSeries.absicssaOfAbsConv_logPowMul {f : ℕ → ℂ} {m : ℕ} : abscissaOfAbsConv (logMul^[m] f) = abscissaOfAbsConv f

The abscissa of absolute convergence of the point-wise product of a power of log and f is the same as that of f.

theorem LSeries_iteratedDeriv {f : ℕ → ℂ} (m : ℕ) {s : ℂ} (h : LSeries.abscissaOfAbsConv f < ↑s.re) : iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (LSeries.logMul^[m] f) s

If re s is greater than the abscissa of absolute convergence of f, then the mth derivative of this L-series is (-1)^m times the L-series of log^m * f.

The L-series is holomorphic

theorem LSeries_differentiableOn (f : ℕ → ℂ) : DifferentiableOn ℂ (LSeries f) {s : ℂ | LSeries.abscissaOfAbsConv f < ↑s.re}

The L-series of f is complex differentiable in its open half-plane of absolute convergence.

theorem LSeries_analyticOnNhd (f : ℕ → ℂ) : AnalyticOnNhd ℂ (LSeries f) {s : ℂ | LSeries.abscissaOfAbsConv f < ↑s.re}

The L-series of f is holomorphic on its open half-plane of absolute convergence.

theorem LSeries_analyticOn (f : ℕ → ℂ) : AnalyticOn ℂ (LSeries f) {s : ℂ | LSeries.abscissaOfAbsConv f < ↑s.re}