Elementary source closure for prime-AP partial summation

This module discharges the higher-prime-power term by a literal finite support count. It also records the minimal one-dimensional hypotheses needed for the global PNT and Chebyshev-to-li sources. No AP or Bombieri--Vinogradov conclusion is assumed in either source contract.

noncomputable def AnalyticNumberTheory.LargeSieve.higherPrimePowerSupport (N : ℕ) : Finset ℕ

Nonprime support of Λ through N.

Equations

• AnalyticNumberTheory.LargeSieve.higherPrimePowerSupport N = {n ∈ Finset.range (N + 1) | ¬Nat.Prime n ∧ ArithmeticFunction.vonMangoldt n ≠ 0}

def AnalyticNumberTheory.LargeSieve.higherPrimePowerEnvelope (N : ℕ) : Finset ℕ

A finite family containing every higher prime power through N: bases up through √N, and exponents up through log₂ N.

Equations

• AnalyticNumberTheory.LargeSieve.higherPrimePowerEnvelope N = Finset.image (fun (pk : ℕ × ℕ) => pk.1 ^ (pk.2 + 2)) ((Finset.range (N.sqrt + 1)).product (Finset.range (N.log2 + 1)))

theorem AnalyticNumberTheory.LargeSieve.higherPrimePowerSupport_subset_envelope (N : ℕ) : higherPrimePowerSupport N ⊆ higherPrimePowerEnvelope N

theorem AnalyticNumberTheory.LargeSieve.card_higherPrimePowerSupport_le (N : ℕ) : (higherPrimePowerSupport N).card ≤ (N.sqrt + 1) * (N.log2 + 1)

There are at most (√N+1)(log₂N+1) nonprime points in the support of Λ. This is the explicit k ≥ 2 ⇒ p ≤ √N count.

theorem AnalyticNumberTheory.LargeSieve.lambda_norm_le_log_of_le {n N : ℕ} (hn : n ≤ N) (hN : 2 ≤ N) : ‖lambdaNatCoeff n‖ ≤ Real.log ↑N

The von Mangoldt coefficient through N has norm at most log N.

theorem AnalyticNumberTheory.LargeSieve.norm_lambdaPrimePowerCorrection_le_explicit {y N q a : ℕ} (hy : y ≤ N) : ‖lambdaPrimePowerCorrection y q a‖ ≤ ↑(N.sqrt + 1) * (↑N.log2 + 1) * Real.log ↑N

Uniform explicit correction bound, independent of modulus and residue.

theorem AnalyticNumberTheory.LargeSieve.lambdaPrimePowerCorrectionPrefixMaxError_le_explicit (N q : ℕ) : lambdaPrimePowerCorrectionPrefixMaxError N q ≤ ↑(N.sqrt + 1) * (↑N.log2 + 1) * Real.log ↑N

Prefix/residue maximum inherits the same modulus-free explicit bound.

noncomputable def AnalyticNumberTheory.LargeSieve.primePowerCorrectionExplicitBound (N : ℕ) : ℝ

The explicit modulus-free majorant for the higher-prime-power correction.

Equations

• AnalyticNumberTheory.LargeSieve.primePowerCorrectionExplicitBound N = ↑(N.sqrt + 1) * (↑N.log2 + 1) * Real.log ↑N

theorem AnalyticNumberTheory.LargeSieve.sum_lambdaPrimePowerCorrectionPrefixMaxError_le (N Q : ℕ) : ∑ q ∈ Finset.Icc 1 Q, lambdaPrimePowerCorrectionPrefixMaxError N q ≤ ↑Q * primePowerCorrectionExplicitBound N

Summing the residue maximum over any initial modulus interval costs only its cardinality. In particular there is no hidden residue-class factor.

theorem AnalyticNumberTheory.LargeSieve.sum_lambdaPrimePowerCorrection_standardBVRange_le (N : ℕ) (B : ℝ) : ∑ q ∈ Finset.Icc 1 (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B), lambdaPrimePowerCorrectionPrefixMaxError N q ≤ ↑(MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B) * primePowerCorrectionExplicitBound N

Literal Standard-BV-range specialization of the preceding elementary estimate.

theorem AnalyticNumberTheory.LargeSieve.sum_lambdaPrimePowerCorrection_standardBVRange_payable {N : ℕ} {A B C : ℝ} (hpay : ↑(MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B) * primePowerCorrectionExplicitBound N ≤ C * ↑N / Real.log ↑N ^ A) : ∑ q ∈ Finset.Icc 1 (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B), lambdaPrimePowerCorrectionPrefixMaxError N q ≤ C * ↑N / Real.log ↑N ^ A

Once the elementary scalar majorant fits in an N/log^A N budget, the whole prime-power contribution on the genuine Standard-BV range fits in the same budget. This theorem performs the finite q,residue,prefix bookkeeping; its premise is purely one-dimensional.

noncomputable def AnalyticNumberTheory.LargeSieve.globalPartialSummationSource (N : ℕ) : ℝ

The two genuinely global source terms left by partial summation: the principal PNT prefix at modulus one, after Abel amplification, and the scalar discrete-main-to-genuine-li discrepancy.

Equations

• AnalyticNumberTheory.LargeSieve.globalPartialSummationSource N = AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax N * AnalyticNumberTheory.LargeSieve.principalLambdaPrefixMaxError N 1 + AnalyticNumberTheory.LargeSieve.globalChebyshevToLiSourcePrefixMaxError N

def AnalyticNumberTheory.LargeSieve.GlobalChebyshevToLiPrincipalPNTSourceContract : Prop

Minimal source contract. It is a statement about one scalar sequence of N, with one common eventual threshold. It mentions neither residue classes, AP errors, characters, modulus ranges, nor a BV conclusion.

Equations

• AnalyticNumberTheory.LargeSieve.GlobalChebyshevToLiPrincipalPNTSourceContract = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ N → AnalyticNumberTheory.LargeSieve.globalPartialSummationSource N ≤ C * ↑N / Real.log ↑N ^ A

theorem AnalyticNumberTheory.LargeSieve.globalPartialSummationSource_payable (hsource : GlobalChebyshevToLiPrincipalPNTSourceContract) (A : ℝ) : 0 < A → ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ N → discreteAbelAmplifierPrefixMax N * principalLambdaPrefixMaxError N 1 + globalChebyshevToLiSourcePrefixMaxError N ≤ C * ↑N / Real.log ↑N ^ A

The one-dimensional contract closes exactly the global source term in the partial-summation bridge, with no AP/BV assertion frozen into the hypothesis.