Documentation

MathlibNt.AnalyticNumberTheory.DirichletL.DirichletLConditionalDerivativeSeries

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.

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

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

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

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

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

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

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

source
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
Instances For
    source
    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.

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

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