Conditional convergence of the derivative Dirichlet series

This module combines the exact finite Abel identity, the modulus bound for character prefix sums, and the total-variation estimate for the logarithmic cpow weight.

theorem DirichletLConditionalDerivativeSeries.logCpowWeight_nat_eq (s : ℂ) {k : ℕ} (hk : 1 ≤ k) : DirichletLAbelWeightVariation.logCpowWeight s ↑k = -Complex.log ↑k * ↑k ^ (-s)

On positive natural numbers, the real-logarithm definition of logCpowWeight is exactly the complex-logarithm weight occurring in finite Abel summation.

theorem DirichletLConditionalDerivativeSeries.logCpowWeight_abel_Ico {q : ℕ} (χ : DirichletCharacter ℂ q) (s : ℂ) {m n : ℕ} (_hm : 1 ≤ m) (hmn : m < n) : ∑ k ∈ Finset.Ico m n, DirichletLAbelWeightVariation.logCpowWeight s ↑k * χ ↑k = DirichletLAbelWeightVariation.logCpowWeight s ↑(n - 1) * ∑ k ∈ Finset.range n, χ ↑k - DirichletLAbelWeightVariation.logCpowWeight s ↑m * ∑ k ∈ Finset.range m, χ ↑k - ∑ k ∈ Finset.Ico m (n - 1), (DirichletLAbelWeightVariation.logCpowWeight s ↑(k + 1) - DirichletLAbelWeightVariation.logCpowWeight s ↑k) * ∑ j ∈ Finset.range (k + 1), χ ↑j

Exact finite Abel identity, stated with logCpowWeight.

theorem DirichletLConditionalDerivativeSeries.norm_sum_Ico_logCpowWeight_character_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 0 < s.re) {m n : ℕ} (hm : 1 ≤ m) (hmn : m < n) : ‖∑ k ∈ Finset.Ico m n, DirichletLAbelWeightVariation.logCpowWeight s ↑k * χ ↑k‖ ≤ ↑q * (‖DirichletLAbelWeightVariation.logCpowWeight s ↑(n - 1)‖ + ‖DirichletLAbelWeightVariation.logCpowWeight s ↑m‖ + DirichletLAbelWeightVariation.logVariationBudget s ↑m)

Uniform finite-tail estimate for the logarithmic derivative weight.

theorem DirichletLConditionalDerivativeSeries.tendsto_norm_logCpowWeight_nat_atTop (s : ℂ) (hs : 0 < s.re) : Filter.Tendsto (fun (n : ℕ) => ‖DirichletLAbelWeightVariation.logCpowWeight s ↑n‖) Filter.atTop (nhds 0)

The endpoint logarithmic cpow weight tends to zero throughout re s > 0.

theorem DirichletLConditionalDerivativeSeries.tendsto_logVariationBudget_nat_atTop (s : ℂ) (hs : 0 < s.re) : Filter.Tendsto (fun (n : ℕ) => DirichletLAbelWeightVariation.logVariationBudget s ↑n) Filter.atTop (nhds 0)

The explicit variation budget also vanishes at infinity.

theorem DirichletLConditionalDerivativeSeries.cauchySeq_sum_range_logCpowWeight_character {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 0 < s.re) : CauchySeq fun (n : ℕ) => ∑ k ∈ Finset.range n, DirichletLAbelWeightVariation.logCpowWeight s ↑k * χ ↑k

The ordinary ordered partial sums form a Cauchy sequence. This is the correct notion of conditional convergence for a series indexed in its natural order.

theorem DirichletLConditionalDerivativeSeries.exists_tendsto_sum_range_logCpowWeight_character {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 0 < s.re) : ∃ (L : ℂ), Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, DirichletLAbelWeightVariation.logCpowWeight s ↑k * χ ↑k) Filter.atTop (nhds L)

Existence of the naturally ordered conditional sum.

noncomputable def DirichletLConditionalDerivativeSeries.orderedLogDerivativeSeries {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 0 < s.re) : ℂ

The canonical value of the conditionally convergent logarithmic derivative series, defined by taking its partial sums in the natural order. The convergence hypotheses are arguments of the definition so that no unordered tsum is used in the conditional range.

Equations

• DirichletLConditionalDerivativeSeries.orderedLogDerivativeSeries χ hχ s hs = Classical.choose ⋯

theorem DirichletLConditionalDerivativeSeries.tendsto_sum_range_orderedLogDerivativeSeries {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 0 < s.re) : Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, DirichletLAbelWeightVariation.logCpowWeight s ↑k * χ ↑k) Filter.atTop (nhds (orderedLogDerivativeSeries χ hχ s hs))

The naturally ordered partial sums converge to orderedLogDerivativeSeries.

theorem DirichletLConditionalDerivativeSeries.norm_orderedLogDerivativeSeries_sub_sum_range_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 0 < s.re) {m : ℕ} (hm : 1 ≤ m) : ‖orderedLogDerivativeSeries χ hχ s hs - ∑ k ∈ Finset.range m, DirichletLAbelWeightVariation.logCpowWeight s ↑k * χ ↑k‖ ≤ ↑q * (‖DirichletLAbelWeightVariation.logCpowWeight s ↑m‖ + DirichletLAbelWeightVariation.logVariationBudget s ↑m)

Explicit tail bound for the canonical naturally ordered sum.

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

In the half-plane of absolute convergence, the canonical naturally ordered sum is the derivative of the analytically continued Dirichlet L-function.