Zero contributions in the four-factor quadratic argument

This file supplies the algebraic/analytic bearing between a completed-function explicit formula and the positive four-factor logarithmic derivative. Infinite zero families are represented by genuine summable kernels. The finite rectangle formulation is also exposed, so a later Hadamard-product theorem can enter through finite rectangles without any opaque “source” predicate.

noncomputable def AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.zeroKernel (σ : ℝ) (ρ : ℂ) : ℝ

The real contribution of a zero ρ to a logarithmic derivative at a real point σ.

Equations

• AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.zeroKernel σ ρ = (↑σ - ρ)⁻¹.re

noncomputable def AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.finiteZeroContribution {ι : Type u_1} (zeros : ι → ℂ) (S : Finset ι) (σ : ℝ) : ℝ

A finite-rectangle zero contribution. Multiplicity is represented by the indexing type, so repeated zeros are retained.

Equations

• AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.finiteZeroContribution zeros S σ = ∑ ρ ∈ S, AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.zeroKernel σ (zeros ρ)

noncomputable def AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.zeroContribution {ι : Type u_1} (zeros : ι → ℂ) (σ : ℝ) : ℝ

The global zero contribution, indexed with multiplicity. Identifying it with a convergent sum requires Summable; nonnegativity holds without it.

Equations

• AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.zeroContribution zeros σ = ∑' (ρ : ι), AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.zeroKernel σ (zeros ρ)

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.zeroKernel_ofReal {σ β : ℝ} (h : β < σ) : zeroKernel σ ↑β = 1 / (σ - β)

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.zeroKernel_nonneg {σ : ℝ} {ρ : ℂ} (hρ : ρ.re ≤ σ) : 0 ≤ zeroKernel σ ρ

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.zeroContribution_nonneg {ι : Type u_1} (zeros : ι → ℂ) (σ : ℝ) (hstrip : ∀ (ρ : ι), (zeros ρ).re ≤ σ) : 0 ≤ zeroContribution zeros σ

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.hasSum_finiteZeroContribution {ι : Type u_1} (zeros : ι → ℂ) (σ : ℝ) (hsum : Summable fun (ρ : ι) => zeroKernel σ (zeros ρ)) : HasSum (fun (ρ : ι) => zeroKernel σ (zeros ρ)) (zeroContribution zeros σ)

Genuine convergence of finite zero rectangles to the zero contribution. This is HasSum, hence a limit over the directed system of finite subsets.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.completed_explicitFormula_fixedRealStrip {ι : Type u_1} (completed : ℂ → ℂ) (zeros : ι → ℂ) (A : ℝ → ℝ) (a b : ℝ) (hentire : Differentiable ℂ completed) (hsum : ∀ σ ∈ Set.Icc a b, Summable fun (ρ : ι) => zeroKernel σ (zeros ρ)) (hformula : ∀ σ ∈ Set.Icc a b, completed ↑σ ≠ 0 → (deriv completed ↑σ / completed ↑σ).re = A σ + zeroContribution zeros σ) : Differentiable ℂ completed ∧ (∀ σ ∈ Set.Icc a b, completed ↑σ ≠ 0 → (deriv completed ↑σ / completed ↑σ).re = A σ + zeroContribution zeros σ) ∧ ∀ σ ∈ Set.Icc a b, HasSum (fun (ρ : ι) => zeroKernel σ (zeros ρ)) (zeroContribution zeros σ)

Fixed-real-strip completed-function explicit formula, in both the genuine summable-zero and finite-rectangle-limit forms. The equality is the exact Hadamard/log-derivative input; unlike a source predicate, it is visible in the theorem's type. Entireness of the primitive nonprincipal completed quadratic function is discharged from the production API.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.primitiveQuadratic_completed_entire {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ.IsPrimitive) (hquad : χ ^ 2 = 1) (hne : χ ≠ 1) : Differentiable ℂ (DirichletCharacter.completedLFunction χ) ∧ ∀ (s : ℂ), DirichletCharacter.completedLFunction χ (1 - s) = ↑q ^ (s - 1 / 2) * χ.rootNumber * DirichletCharacter.completedLFunction χ s

Primitive quadratic specialization of the entireness part needed by the fixed-strip explicit formula.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.negLogDerivative_eq_arch_sub_zeroContribution {ι : Type u_1} (L completed : ℂ → ℂ) (zeros : ι → ℂ) (arch : ℝ → ℝ) (σ : ℝ) (hL : L ↑σ ≠ 0) (hcompleted : completed ↑σ ≠ 0) (hsum : Summable fun (ρ : ι) => zeroKernel σ (zeros ρ)) (hcompletedFormula : (deriv completed ↑σ / completed ↑σ).re = arch σ + zeroContribution zeros σ) (hgammaBridge : (-deriv L ↑σ / L ↑σ).re = 2 * arch σ - (deriv completed ↑σ / completed ↑σ).re) : (-deriv L ↑σ / L ↑σ).re = arch σ - zeroContribution zeros σ

Conversion of a completed-function zero formula into an uncompleted negative-log-derivative formula. arch is the explicit conductor/gamma term; the bridge equality is normally obtained by differentiating Λ(s,χ)=gammaFactor(s,χ)L(s,χ).

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.two_real_zeros_repel_of_fourFactor_nonneg {σ β₁ β₂ pole arch remainder total : ℝ} (hrem : 0 ≤ remainder) (hformula : total = pole + arch - 1 / (σ - β₁) - 1 / (σ - β₂) - remainder) (htotal : 0 ≤ total) : 1 / (σ - β₁) + 1 / (σ - β₂) ≤ pole + arch

Isolation of two designated real zeros from the nonnegative four-factor logarithmic derivative. All remaining zero terms have the correct sign and are discarded only through the explicit hypothesis 0 ≤ remainder.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.second_zero_separation {σ β₁ β₂ B : ℝ} (hβ₂ : β₂ < σ) (hsum : 1 / (σ - β₁) + 1 / (σ - β₂) ≤ B) (hbudget : 0 < B - 1 / (σ - β₁)) : 1 / (B - 1 / (σ - β₁)) ≤ σ - β₂

Quantitative one-sided Deuring--Heilbronn separation after isolating a near-one zero β₁.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.twoFactor_value_lower_of_integrated_fourFactor {L₁ L₂ Lpair lower upper : ℝ} (hL₁ : 0 ≤ L₁) (hL₂ : 0 ≤ L₂) (hlower : lower ≤ L₁ * L₂ * Lpair) (hpair : Lpair ≤ upper) (hupper : 0 < upper) : lower / upper ≤ L₁ * L₂

Final algebraic value-at-one lower-bound step after integration. It is stated for the three non-zeta factors: once the integrated explicit formula supplies lower ≤ L(1,χ₁)L(1,χ₂)L(1,χ₁χ₂), an upper bound for the pair factor produces the desired two-factor lower bound.