Mellin continuation of a nonprincipal character pair

This modern analytic argument identifies the Mellin integral of the actual convolution of two nonprincipal characters with the product of their L-functions on Re s > 1/2. No primitivity or quadraticity is needed. In particular the value at one is the actual L-value product, not a formal or absolutely convergent harmonic series.

noncomputable def DirichletCharacter.characterPairSummatory {q : ℕ} (ψ η : DirichletCharacter ℂ q) (t : ℝ) : ℂ

The actual pair summatory function at a real endpoint.

Equations

• ψ.characterPairSummatory η t = ∑ n ∈ Finset.Icc 1 ⌊t⌋₊, ((toArithmeticFunction fun (x : ℕ) => ψ ↑x) * toArithmeticFunction fun (x : ℕ) => η ↑x) n

noncomputable def DirichletCharacter.characterPairKernel {q : ℕ} (ψ η : DirichletCharacter ℂ q) (s : ℂ) (t : ℝ) : ℂ

The kernel whose integral continues the pair Dirichlet series.

Equations

• ψ.characterPairKernel η s t = ψ.characterPairSummatory η t * ↑t ^ (-(s + 1))

noncomputable def DirichletCharacter.characterPairIntegral {q : ℕ} (ψ η : DirichletCharacter ℂ q) (s : ℂ) : ℂ

The genuinely convergent integral used for the continuation.

Equations

• ψ.characterPairIntegral η s = ∫ (t : ℝ) in Set.Ioi 1, ψ.characterPairKernel η s t

noncomputable def DirichletCharacter.characterPairCutoff {q : ℕ} (ψ η : DirichletCharacter ℂ q) : ℝ → ℂ

Cutoff of the actual summatory function for the Mellin transform.

Equations

• ψ.characterPairCutoff η = (Set.Ioi 1).indicator (ψ.characterPairSummatory η)

theorem DirichletCharacter.measurable_characterPairSummatory {q : ℕ} (ψ η : DirichletCharacter ℂ q) : Measurable (ψ.characterPairSummatory η)

theorem DirichletCharacter.measurable_characterPairCutoff {q : ℕ} (ψ η : DirichletCharacter ℂ q) : Measurable (ψ.characterPairCutoff η)

theorem DirichletCharacter.norm_characterPairCutoff_le {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) (t : ℝ) : ‖ψ.characterPairCutoff η t‖ ≤ 3 * ↑q * √t

theorem DirichletCharacter.locallyIntegrable_characterPairCutoff {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) : MeasureTheory.LocallyIntegrable (ψ.characterPairCutoff η) MeasureTheory.volume

theorem DirichletCharacter.characterPairCutoff_isBigO_atTop {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) : ψ.characterPairCutoff η =O[Filter.atTop] fun (t : ℝ) => t ^ (1 / 2)

theorem DirichletCharacter.characterPairCutoff_isBigO_zero {q : ℕ} (ψ η : DirichletCharacter ℂ q) (b : ℝ) : ψ.characterPairCutoff η =O[nhdsWithin 0 (Set.Ioi 0)] fun (t : ℝ) => t ^ b

theorem DirichletCharacter.mellin_characterPairCutoff {q : ℕ} (ψ η : DirichletCharacter ℂ q) (s : ℂ) : mellin (ψ.characterPairCutoff η) (-s) = ψ.characterPairIntegral η s

theorem DirichletCharacter.mellinConvergent_characterPairCutoff {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) {s : ℂ} (hs : 1 / 2 < s.re) : MellinConvergent (ψ.characterPairCutoff η) (-s)

theorem DirichletCharacter.integrableOn_characterPairKernel {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) {s : ℂ} (hs : 1 / 2 < s.re) : MeasureTheory.IntegrableOn (ψ.characterPairKernel η s) (Set.Ioi 1) MeasureTheory.volume

Absolute integrability of the summatory kernel, not of the harmonic series.

theorem DirichletCharacter.differentiableAt_characterPairIntegral {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) {s : ℂ} (hs : 1 / 2 < s.re) : DifferentiableAt ℂ (ψ.characterPairIntegral η) s

theorem DirichletCharacter.LFunction_mul_eq_characterPairIntegral_of_one_lt_re {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) {s : ℂ} (hs : 1 < s.re) : LFunction ψ s * LFunction η s = s * ψ.characterPairIntegral η s

Identification on the absolute-convergence half-plane.

theorem DirichletCharacter.LFunction_mul_eq_characterPairIntegral {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) {s : ℂ} (hs : 1 / 2 < s.re) : LFunction ψ s * LFunction η s = s * ψ.characterPairIntegral η s

The actual product identity throughout Re s > 1/2, obtained by analytic continuation of the convergent Mellin integral.

theorem DirichletCharacter.LFunction_one_mul_eq_characterPairIntegral {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) : LFunction ψ 1 * LFunction η 1 = ψ.characterPairIntegral η 1

At one, the Mellin integral is exactly the genuine product of L-values.