Analytic continuation of the conditionally convergent derivative series

The natural partial sums converge locally uniformly on re s > 0. Thus their ordered limit is holomorphic there, and the identity theorem identifies it with the derivative of the Dirichlet L-function.

def DirichletLConditionalDerivativeAnalyticContinuation.rightHalfPlane : Set ℂ

The open right half-plane.

Equations

• DirichletLConditionalDerivativeAnalyticContinuation.rightHalfPlane = {s : ℂ | 0 < s.re}

noncomputable def DirichletLConditionalDerivativeAnalyticContinuation.derivativePartialSum {q : ℕ} (χ : DirichletCharacter ℂ q) (N : ℕ) (s : ℂ) : ℂ

Natural partial sums, regarded as entire functions.

Equations

• DirichletLConditionalDerivativeAnalyticContinuation.derivativePartialSum χ N s = ∑ n ∈ Finset.range N, DirichletLAbelWeightVariation.logCpowWeight s ↑n * χ ↑n

noncomputable def DirichletLConditionalDerivativeAnalyticContinuation.orderedDerivativeFunction {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) : ℂ

The ordered sum as a function on all of ℂ; outside the right half-plane its value is immaterial. The dependent proof argument is eliminated by this wrapper.

Equations

• DirichletLConditionalDerivativeAnalyticContinuation.orderedDerivativeFunction χ hχ s = if hs : 0 < s.re then DirichletLConditionalDerivativeSeries.orderedLogDerivativeSeries χ hχ s hs else 0

theorem DirichletLConditionalDerivativeAnalyticContinuation.orderedLogDerivativeSeries_proof_irrel {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs ht : 0 < s.re) : DirichletLConditionalDerivativeSeries.orderedLogDerivativeSeries χ hχ s hs = DirichletLConditionalDerivativeSeries.orderedLogDerivativeSeries χ hχ s ht

The value of the dependent ordered sum does not depend on the proof of 0 < re s. This explicit lemma prevents dependent proof arguments from leaking into the function-level analytic statements.

theorem DirichletLConditionalDerivativeAnalyticContinuation.orderedDerivativeFunction_eq {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 0 < s.re) : orderedDerivativeFunction χ hχ s = DirichletLConditionalDerivativeSeries.orderedLogDerivativeSeries χ hχ s hs

noncomputable def DirichletLConditionalDerivativeAnalyticContinuation.compactTailMajorant (q : ℕ) (δ M : ℝ) (n : ℕ) : ℝ

A compact-uniform scalar majorant for the explicit Abel tail.

Equations

• DirichletLConditionalDerivativeAnalyticContinuation.compactTailMajorant q δ M n = ↑q * (Real.log ↑n / ↑n ^ δ + (1 / δ + M / δ ^ 2) * ↑n ^ (-δ) + M / δ * (Real.log ↑n / ↑n ^ δ))

theorem DirichletLConditionalDerivativeAnalyticContinuation.tendstoLocallyUniformlyOn_derivativePartialSum {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) : TendstoLocallyUniformlyOn (derivativePartialSum χ) (orderedDerivativeFunction χ hχ) Filter.atTop rightHalfPlane

The natural partial sums converge locally uniformly throughout re s > 0.

theorem DirichletLConditionalDerivativeAnalyticContinuation.differentiableOn_orderedDerivativeFunction {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) : DifferentiableOn ℂ (orderedDerivativeFunction χ hχ) rightHalfPlane

The ordered conditional derivative series is holomorphic on the right half-plane.

theorem DirichletLConditionalDerivativeAnalyticContinuation.orderedLogDerivativeSeries_eq_deriv_LFunction_of_re_pos {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 0 < s.re) : DirichletLConditionalDerivativeSeries.orderedLogDerivativeSeries χ hχ s hs = deriv (DirichletCharacter.LFunction χ) s

Analytic continuation identifies the ordered conditionally convergent series with L' on the whole half-plane re s > 0.