The actual four-factor local zero-repulsion identity

This file combines three finite-disk factorizations, for χ₁, χ₂, and χ₁χ₂, with the actual conductor/gamma bridge and the Euler-product positivity of ζ L(χ₁) L(χ₂) L(χ₁χ₂). The only remainder is the sum of the three local nonvanishing factors' logarithmic derivatives.

structure AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.CharacterLocalDiskData {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (c : ℂ) (R : ℝ) : Type

An actual choice of the finite zero divisor and nonvanishing local factor for one symmetrically completed Dirichlet L-function.

• D : ℂ → ℤ
• S : Finset ℂ
• g : ℂ → ℂ
• D_nonneg (z : ℂ) : 0 ≤ self.D z
• mem_iff (z : ℂ) : z ∈ self.S ↔ z ∈ Metric.ball c R ∧ symmetricCompletedLFunction χ z = 0
• g_analytic : AnalyticOnNhd ℂ self.g (Metric.ball c R)
• g_ne_zero (z : ℂ) : z ∈ Metric.ball c R → self.g z ≠ 0
• formula (s : ℂ) : s ∈ Metric.ball c R → symmetricCompletedLFunction χ s ≠ 0 → logDeriv (symmetricCompletedLFunction χ) s = ∑ ρ ∈ self.S, ↑(self.D ρ).toNat / (s - ρ) + logDeriv self.g s

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.CharacterLocalDiskData.exists {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (c : ℂ) {R : ℝ} (hR : 0 < R) : Nonempty (CharacterLocalDiskData χ c R)

The local factorization theorem makes an actual disk datum; no formula is passed in abstractly.

noncomputable def AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.CharacterLocalDiskData.zeroSum {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} {c : ℂ} {R : ℝ} (d : CharacterLocalDiskData χ c R) (σ : ℝ) : ℝ

The real part of the finite zero sum, with its actual multiplicities.

Equations

• d.zeroSum σ = ∑ ρ ∈ d.S, ↑(d.D ρ).toNat * AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.zeroKernel σ ρ

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.CharacterLocalDiskData.zeroSum_nonneg {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} {c : ℂ} {R : ℝ} (d : CharacterLocalDiskData χ c R) {σ : ℝ} (hstrip : ∀ ρ ∈ d.S, ρ.re ≤ σ) : 0 ≤ d.zeroSum σ

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.CharacterLocalDiskData.zeroKernel_le_zeroSum {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} {c : ℂ} {R : ℝ} (d : CharacterLocalDiskData χ c R) {σ : ℝ} {β : ℂ} (hβ : β ∈ d.S) (hmult : 1 ≤ (d.D β).toNat) (hstrip : ∀ ρ ∈ d.S, ρ.re ≤ σ) : zeroKernel σ β ≤ d.zeroSum σ

noncomputable def AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.actualFourFactorLogDerivative {q₁ q₂ : ℕ} [NeZero q₁] [NeZero q₂] [NeZero (q₁ * q₂)] (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) (σ : ℝ) : ℝ

The actual four-factor negative logarithmic derivative, retaining the zeta factor in its standard L-series form.

Equations

• AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.actualFourFactorLogDerivative χ₁ χ₂ σ = (-deriv (LSeries fun (x : ℕ) => 1) ↑σ / LSeries (fun (x : ℕ) => 1) ↑σ).re + (-deriv (DirichletCharacter.LFunction χ₁) ↑σ / DirichletCharacter.LFunction χ₁ ↑σ).re + (-deriv (DirichletCharacter.LFunction χ₂) ↑σ / DirichletCharacter.LFunction χ₂ ↑σ).re + (-deriv (DirichletCharacter.LFunction (AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.pairCharacter χ₁ χ₂)) ↑σ / DirichletCharacter.LFunction (AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.pairCharacter χ₁ χ₂) ↑σ).re

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.actualFourFactor_localZeroIdentity {q₁ q₂ : ℕ} [NeZero q₁] [NeZero q₂] [NeZero (q₁ * q₂)] (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) (hχ₁ : χ₁ ≠ 1) (hχ₂ : χ₂ ≠ 1) (hpair : TatuzawaMultiplicativeTransfer.pairCharacter χ₁ χ₂ ≠ 1) {c : ℂ} {R : ℝ} (d₁ : CharacterLocalDiskData χ₁ c R) (d₂ : CharacterLocalDiskData χ₂ c R) (dp : CharacterLocalDiskData (TatuzawaMultiplicativeTransfer.pairCharacter χ₁ χ₂) c R) {σ : ℝ} (hσ : 1 < σ) (hσdisk : ↑σ ∈ Metric.ball c R) : actualFourFactorLogDerivative χ₁ χ₂ σ = (-deriv (LSeries fun (x : ℕ) => 1) ↑σ / LSeries (fun (x : ℕ) => 1) ↑σ).re + (conductorGammaTerm χ₁ ↑σ).re + (conductorGammaTerm χ₂ ↑σ).re + (conductorGammaTerm (TatuzawaMultiplicativeTransfer.pairCharacter χ₁ χ₂) ↑σ).re - d₁.zeroSum σ - d₂.zeroSum σ - dp.zeroSum σ - ((logDeriv d₁.g ↑σ).re + (logDeriv d₂.g ↑σ).re + (logDeriv dp.g ↑σ).re)

The exact identity obtained by putting all three actual local factorizations on one disk. Zeros outside the disk occur only through the three concrete g'/g terms.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.threeLocalRemainder_le_of_circleBounds (g₁ g₂ gp : ℂ → ℂ) (σ : ℂ) {r M₁ M₂ Mp m₁ m₂ mp : ℝ} (hr : 0 < r) (hM₁ : 0 ≤ M₁) (hM₂ : 0 ≤ M₂) (hMp : 0 ≤ Mp) (hm₁ : 0 < m₁) (hm₂ : 0 < m₂) (hmp : 0 < mp) (hg₁ : DiffContOnCl ℂ g₁ (Metric.ball σ r)) (hg₂ : DiffContOnCl ℂ g₂ (Metric.ball σ r)) (hgp : DiffContOnCl ℂ gp (Metric.ball σ r)) (hcircle₁ : ∀ z ∈ Metric.sphere σ r, ‖g₁ z‖ ≤ M₁) (hcircle₂ : ∀ z ∈ Metric.sphere σ r, ‖g₂ z‖ ≤ M₂) (hcirclep : ∀ z ∈ Metric.sphere σ r, ‖gp z‖ ≤ Mp) (hlower₁ : m₁ ≤ ‖g₁ σ‖) (hlower₂ : m₂ ≤ ‖g₂ σ‖) (hlowerp : mp ≤ ‖gp σ‖) : -((logDeriv g₁ σ).re + (logDeriv g₂ σ).re + (logDeriv gp σ).re) ≤ M₁ / r / m₁ + M₂ / r / m₂ + Mp / r / mp

The existing Cauchy bound pays the complete three-factor remainder from circle upper bounds and center lower bounds for the actual local factors.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.two_real_zeros_repel {q₁ q₂ : ℕ} [NeZero q₁] [NeZero q₂] [NeZero (q₁ * q₂)] (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) (hχ₁ : χ₁ ≠ 1) (hχ₂ : χ₂ ≠ 1) (hpair : TatuzawaMultiplicativeTransfer.pairCharacter χ₁ χ₂ ≠ 1) (hsq₁ : χ₁ ^ 2 = 1) (hsq₂ : χ₂ ^ 2 = 1) {c : ℂ} {R : ℝ} (d₁ : CharacterLocalDiskData χ₁ c R) (d₂ : CharacterLocalDiskData χ₂ c R) (dp : CharacterLocalDiskData (TatuzawaMultiplicativeTransfer.pairCharacter χ₁ χ₂) c R) {σ β₁ β₂ E : ℝ} (hσ : 1 < σ) (hσdisk : ↑σ ∈ Metric.ball c R) (hβ₁ : ↑β₁ ∈ d₁.S) (hβ₂ : ↑β₂ ∈ d₂.S) (hmult₁ : 1 ≤ (d₁.D ↑β₁).toNat) (hmult₂ : 1 ≤ (d₂.D ↑β₂).toNat) (hβ₁σ : β₁ < σ) (hβ₂σ : β₂ < σ) (hstrip₁ : ∀ ρ ∈ d₁.S, ρ.re ≤ σ) (hstrip₂ : ∀ ρ ∈ d₂.S, ρ.re ≤ σ) (hstripp : ∀ ρ ∈ dp.S, ρ.re ≤ σ) (hremainder : -((logDeriv d₁.g ↑σ).re + (logDeriv d₂.g ↑σ).re + (logDeriv dp.g ↑σ).re) ≤ E) : 1 / (σ - β₁) + 1 / (σ - β₂) ≤ (-deriv (LSeries fun (x : ℕ) => 1) ↑σ / LSeries (fun (x : ℕ) => 1) ↑σ).re + (conductorGammaTerm χ₁ ↑σ).re + (conductorGammaTerm χ₂ ↑σ).re + (conductorGammaTerm (TatuzawaMultiplicativeTransfer.pairCharacter χ₁ χ₂) ↑σ).re + E

Character-specific two-real-zero repulsion. Its hypotheses are only actual local disk data, the two selected disk zeros with multiplicity, the elementary right-of-zero strip condition, and a directly checkable bound for the three g'/g remainders; there is no abstract explicit-formula hypothesis.