Mellin continuation of the genuine two-character convolution

This modern argument continues the actual four-factor product by the Mellin transform of its proved summatory error. Only the first character must be quadratic; neither character must be primitive. This is not a source transcription of Bombieri's argument.

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterSummatory {q : ℕ} (χ ψ : DirichletCharacter ℂ q) (N : ℕ) : ℂ

The actual complex summatory function.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterSummatory χ ψ N = ∑ n ∈ Finset.Icc 1 N, (χ.twoCharacterConvolution ψ) n

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterError {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (t : ℝ) : ℂ

The actual summatory error with its actual residue.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterError χ ψ t = AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterSummatory χ ψ ⌊t⌋₊ - ↑t * χ.twoCharacterResidue ψ

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterErrorKernel {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (s : ℂ) (t : ℝ) : ℂ

The Mellin kernel of the summatory error.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterErrorKernel χ ψ s t = AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterError χ ψ t * ↑t ^ (-(s + 1))

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterErrorIntegral {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (s : ℂ) : ℂ

The genuine error integral, initially convergent for Re s > 3/4.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterErrorIntegral χ ψ s = ∫ (t : ℝ) in Set.Ioi 1, AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterErrorKernel χ ψ s t

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterCutoffError {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) : ℝ → ℂ

The cutoff needed to use the Mellin transform on the positive half-line.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterCutoffError χ ψ = (Set.Ioi 1).indicator (AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterError χ ψ)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.norm_twoCharacterError_le {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) {t : ℝ} (ht : 1 ≤ t) : ‖twoCharacterError χ ψ t‖ ≤ 308 * ↑q ^ 3 * t ^ (3 / 4)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.measurable_twoCharacterError {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) : Measurable (twoCharacterError χ ψ)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.measurable_twoCharacterCutoffError {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) : Measurable (twoCharacterCutoffError χ ψ)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.norm_twoCharacterCutoffError_le {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) (t : ℝ) : ‖twoCharacterCutoffError χ ψ t‖ ≤ 308 * ↑q ^ 3 * |t| ^ (3 / 4)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.locallyIntegrable_twoCharacterCutoffError {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) : MeasureTheory.LocallyIntegrable (twoCharacterCutoffError χ ψ) MeasureTheory.volume

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterCutoffError_isBigO_atTop {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) : twoCharacterCutoffError χ ψ =O[Filter.atTop] fun (t : ℝ) => t ^ (3 / 4)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterCutoffError_isBigO_zero {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (b : ℝ) : twoCharacterCutoffError χ ψ =O[nhdsWithin 0 (Set.Ioi 0)] fun (t : ℝ) => t ^ b

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.mellin_twoCharacterCutoffError {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (s : ℂ) : mellin (twoCharacterCutoffError χ ψ) (-s) = twoCharacterErrorIntegral χ ψ s

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.integrableOn_twoCharacterErrorKernel {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) {s : ℂ} (hs : 3 / 4 < s.re) : MeasureTheory.IntegrableOn (twoCharacterErrorKernel χ ψ s) (Set.Ioi 1) MeasureTheory.volume

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.differentiableAt_twoCharacterErrorIntegral {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) {s : ℂ} (hs : 3 / 4 < s.re) : DifferentiableAt ℂ (twoCharacterErrorIntegral χ ψ) s

Holomorphy is proved from the actual O(t^(3/4)) error.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterSummatory_isBigO {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) : twoCharacterSummatory χ ψ =O[Filter.atTop] fun (n : ℕ) => ↑n ^ 1

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacter_product_eq_errorIntegral_of_one_lt_re {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) {s : ℂ} (hs : 1 < s.re) : riemannZeta s * DirichletCharacter.LFunction χ s * DirichletCharacter.LFunction ψ s * DirichletCharacter.LFunction (χ * ψ) s = χ.twoCharacterResidue ψ * s / (s - 1) + s * twoCharacterErrorIntegral χ ψ s

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacter_regularized_product_eq_errorIntegral {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) {s : ℂ} (hs : 3 / 4 < s.re) : riemannZeta₁ s * DirichletCharacter.LFunction χ s * DirichletCharacter.LFunction ψ s * DirichletCharacter.LFunction (χ * ψ) s = χ.twoCharacterResidue ψ * s + (s - 1) * s * twoCharacterErrorIntegral χ ψ s

Identity-theorem continuation of the pole-cleared actual product.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacter_product_eq_errorIntegral {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) {s : ℂ} (hs : 3 / 4 < s.re) (hs1 : s ≠ 1) : riemannZeta s * DirichletCharacter.LFunction χ s * DirichletCharacter.LFunction ψ s * DirichletCharacter.LFunction (χ * ψ) s = χ.twoCharacterResidue ψ * s / (s - 1) + s * twoCharacterErrorIntegral χ ψ s

The continued constant is the actual zeta/three-L-function product.