Closed elementary payload for Standard Bombieri--Vinogradov

This module packages the elementary lanes left by the low/high conductor split. The asymptotic payment is proved from Mathlib's Real.isLittleO_pow_log_id_atTop; no scalar asymptotic inequality is retained as a premise.

theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMeanOn_vaughanSmall_le_explicit (N v : ℕ) (S : Finset ℕ) (hS : ∀ q ∈ S, 0 < q) : apNormalizedPrimitiveMeanOn (vaughanSmallCoeff vaughanUnitIntegerCoeff v) N S ≤ ↑S.card * (↑v * Real.log ↑(v + 1))

The small Vaughan lane in AP normalization costs only the number of conductors, rather than a large-sieve square mean.

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanSmallMean_le_explicit (N Q C v : ℕ) : highConductorVaughanSmallMean N Q C v ≤ ↑Q * (↑v * Real.log ↑(v + 1))

In particular a conductor interval contained in [1,Q] costs at most Q v log(v+1).

noncomputable def AnalyticNumberTheory.LargeSieve.StandardBVPayload (N Q : ℕ) : ℝ

A convenient closed packet for exactly the elementary Standard-BV lanes.

Equations

• AnalyticNumberTheory.LargeSieve.StandardBVPayload N Q = AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax N * (AnalyticNumberTheory.LargeSieve.principalBadPhysical N Q + AnalyticNumberTheory.LargeSieve.primePowerPhysical N Q + 2 * AnalyticNumberTheory.LargeSieve.directConductorCorrectionMean AnalyticNumberTheory.LargeSieve.vonMangoldtIntegerCoeff N Q)

theorem AnalyticNumberTheory.LargeSieve.natLog2_cast_le_two_log {n : ℕ} (hn : 2 ≤ n) : ↑n.log2 ≤ 2 * Real.log ↑n

theorem AnalyticNumberTheory.LargeSieve.natSqrt_cast_le_realSqrt (n : ℕ) : ↑n.sqrt ≤ √↑n

theorem AnalyticNumberTheory.LargeSieve.Q_sqrt_log_payable (A k : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (Q : ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ (A + k) → ↑Q * (√↑N + 1) * Real.log ↑N ^ k ≤ 2 * ↑N / Real.log ↑N ^ A

The exact Q ≤ sqrt N / log^(A+k) N calculation. This is the reusable polynomial-versus-log payment lemma for every elementary lane below.

theorem AnalyticNumberTheory.LargeSieve.StandardBVPayload_le_explicit : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ Q ≤ N, StandardBVPayload N Q ≤ 90 * ↑Q * (√↑N + 1) * Real.log ↑N ^ 3

Abel, bad-principal, higher-prime-power, and conductor-change terms have a single explicit Q (sqrt N+1) log^3 N envelope throughout the BV-relevant range Q ≤ N.

theorem AnalyticNumberTheory.LargeSieve.StandardBVPayload_payable (A : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (Q : ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ (A + 3) → StandardBVPayload N Q ≤ 180 * ↑N / Real.log ↑N ^ A

For every requested logarithmic saving, choosing the modulus exponent three larger pays the entire closed elementary packet.