Elementary scalar payments for Standard Bombieri--Vinogradov

This module closes the lanes which require no distributional input. The only analytic inputs left to a final Standard-BV consumer are the low-conductor Siegel--Walfisz estimate and the high-conductor Type-I/II hybrid estimate.

theorem AnalyticNumberTheory.LargeSieve.reciprocalLogWeight_nonneg (n : ℕ) : 0 ≤ reciprocalLogWeight n

theorem AnalyticNumberTheory.LargeSieve.reciprocalLogWeight_antitone_of_two_le {m n : ℕ} (hm : 2 ≤ m) (hmn : m ≤ n) : reciprocalLogWeight n ≤ reciprocalLogWeight m

theorem AnalyticNumberTheory.LargeSieve.discreteAbelAmplifier_eq_two_inv_log_two {y : ℕ} (hy : 2 ≤ y) : discreteAbelAmplifier y = 2 * (Real.log 2)⁻¹

The total variation of the reciprocal-log Abel kernel is exactly its jump at two, counted twice. In particular the prefix maximum is uniformly bounded; there is no logarithmic growth to pay.

theorem AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax_le_two_inv_log_two (N : ℕ) : discreteAbelAmplifierPrefixMax N ≤ 2 * (Real.log 2)⁻¹

Uniform explicit bound for the prefix-maximal Abel amplifier.

theorem AnalyticNumberTheory.LargeSieve.principalBadPhysical_le_explicit (N Q : ℕ) : principalBadPhysical N Q ≤ ↑Q * ↑Q.log2 * (↑N.log2 + 1) * Real.log ↑N

The principal bad-prime lane is already a Q times polylogarithm.

theorem AnalyticNumberTheory.LargeSieve.primePowerPhysical_le_explicit (N Q : ℕ) : primePowerPhysical N Q ≤ ↑Q * primePowerCorrectionExplicitBound N

The higher-prime-power lane is Q (√N+1) log₂(N) log N.

theorem AnalyticNumberTheory.LargeSieve.vonMangoldt_conductorErrorAmplitude_le {q : ℕ} (hq : 0 < q) (χ : DirichletCharacter ℂ q) (N : ℕ) : conductorErrorAmplitude χ vonMangoldtIntegerCoeff N ≤ 2 * ↑q.log2 * (↑N.log2 + 1) * Real.log ↑N

Each direct conductor-change amplitude for Λ is polylogarithmic.

theorem AnalyticNumberTheory.LargeSieve.directConductorCorrectionMean_vonMangoldt_le (N Q : ℕ) : directConductorCorrectionMean vonMangoldtIntegerCoeff N Q ≤ ↑Q * (2 * ↑Q.log2 * (↑N.log2 + 1) * Real.log ↑N)

The full unsquared conductor correction is only Q times a polylogarithm (and therefore also a polylogarithm times Q²).

theorem AnalyticNumberTheory.LargeSieve.vaughanSmall_primitivePrefixAmplitude_le (N q v : ℕ) (χ : PrimitiveCharacter q) : primitivePrefixAmplitude (vaughanSmallCoeff vaughanUnitIntegerCoeff v) N q χ ≤ ↑v * Real.log ↑(v + 1)

Every primitive-character small Vaughan prefix is bounded directly by its support length v; no large-sieve input is needed.