Naturally ordered conditional Dirichlet L-series

For a nonprincipal Dirichlet character, the ordinary partial sums of χ(n)n⁻ˢ converge when re s > 0. We retain the natural order (rather than using an unordered tsum), prove an explicit Abel tail, establish compact-local uniform convergence, and identify the resulting holomorphic function with χ.LFunction.

theorem DirichletLConditionalValueSeries.character_nat_zero_of_ne_one {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) : χ ↑0 = 0

A nonprincipal Dirichlet character vanishes at the natural argument zero.

theorem DirichletLConditionalValueSeries.cpowWeight_nat_eq (s : ℂ) (k : ℕ) : DirichletLAbelWeightVariation.cpowWeight s ↑k = ↑k ^ (-s)

On natural arguments, cpowWeight is the usual complex Dirichlet weight.

theorem DirichletLConditionalValueSeries.norm_sum_Ico_cpowWeight_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.cpowWeight s ↑k * χ ↑k‖ ≤ ↑q * (‖DirichletLAbelWeightVariation.cpowWeight s ↑(n - 1)‖ + ‖DirichletLAbelWeightVariation.cpowWeight s ↑m‖ + ‖s‖ / s.re * ↑m ^ (-s.re))

Explicit finite Abel tail for the value series.

theorem DirichletLConditionalValueSeries.tendsto_norm_cpowWeight_nat_atTop (s : ℂ) (hs : 0 < s.re) : Filter.Tendsto (fun (n : ℕ) => ‖DirichletLAbelWeightVariation.cpowWeight s ↑n‖) Filter.atTop (nhds 0)

The endpoint value weight tends to zero in re s > 0.

theorem DirichletLConditionalValueSeries.tendsto_cpowVariationBudget_nat_atTop (s : ℂ) (hs : 0 < s.re) : Filter.Tendsto (fun (n : ℕ) => ‖s‖ / s.re * ↑n ^ (-s.re)) Filter.atTop (nhds 0)

The explicit variation part of the tail tends to zero.

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

Natural-order partial sums form a Cauchy sequence throughout re s > 0.

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

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

Canonical value of the conditional series, defined by its natural partial sums.

Equations

• DirichletLConditionalValueSeries.orderedValueSeries χ hχ s hs = Classical.choose ⋯

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

theorem DirichletLConditionalValueSeries.norm_orderedValueSeries_sub_sum_range_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 0 < s.re) {m : ℕ} (hm : 1 ≤ m) : ‖orderedValueSeries χ hχ s hs - ∑ k ∈ Finset.range m, DirichletLAbelWeightVariation.cpowWeight s ↑k * χ ↑k‖ ≤ ↑q * (↑m ^ (-s.re) + ‖s‖ / s.re * ↑m ^ (-s.re))

Explicit tail for the canonical natural-order value.

def DirichletLConditionalValueSeries.rightHalfPlane : Set ℂ

The open half-plane on which the natural-order value series converges.

Equations

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

noncomputable def DirichletLConditionalValueSeries.valuePartialSum {q : ℕ} (χ : DirichletCharacter ℂ q) (N : ℕ) (s : ℂ) : ℂ

Equations

• DirichletLConditionalValueSeries.valuePartialSum χ N s = ∑ n ∈ Finset.range N, DirichletLAbelWeightVariation.cpowWeight s ↑n * χ ↑n

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

Equations

• DirichletLConditionalValueSeries.orderedValueFunction χ hχ s = if hs : 0 < s.re then DirichletLConditionalValueSeries.orderedValueSeries χ hχ s hs else 0

theorem DirichletLConditionalValueSeries.orderedValueSeries_proof_irrel {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs ht : 0 < s.re) : orderedValueSeries χ hχ s hs = orderedValueSeries χ hχ s ht

theorem DirichletLConditionalValueSeries.orderedValueFunction_eq {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 0 < s.re) : orderedValueFunction χ hχ s = orderedValueSeries χ hχ s hs

noncomputable def DirichletLConditionalValueSeries.compactValueTailMajorant (q : ℕ) (δ M : ℝ) (m : ℕ) : ℝ

Compact-window majorant requested by the Abel estimate.

Equations

• DirichletLConditionalValueSeries.compactValueTailMajorant q δ M m = ↑q * ↑m ^ (-δ) * (1 + M / δ)

theorem DirichletLConditionalValueSeries.tendstoLocallyUniformlyOn_valuePartialSum {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) : TendstoLocallyUniformlyOn (valuePartialSum χ) (orderedValueFunction χ hχ) Filter.atTop rightHalfPlane

Natural partial sums converge locally uniformly on re s > 0.

theorem DirichletLConditionalValueSeries.differentiableOn_orderedValueFunction {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) : DifferentiableOn ℂ (orderedValueFunction χ hχ) rightHalfPlane

The canonical natural-order value is holomorphic on the right half-plane.

theorem DirichletLConditionalValueSeries.orderedValueSeries_eq_LFunction {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 1 < s.re) : orderedValueSeries χ hχ s ⋯ = DirichletCharacter.LFunction χ s

In re s > 1, the ordered value is the ordinary L-series value.

theorem DirichletLConditionalValueSeries.orderedValueSeries_eq_LFunction_of_re_pos {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 0 < s.re) : orderedValueSeries χ hχ s hs = DirichletCharacter.LFunction χ s

Identity-theorem continuation: the ordered conditional value is χ.LFunction throughout the full half-plane re s > 0.