Reduction of every principal character to the global PNT source

The principal character at level q deletes exactly the von Mangoldt mass on prime powers p^k with p ∣ q. This module makes that deletion literal, bounds it by ω(q) (log₂ N + 1) log N, sums the correction over q ≤ Q, and feeds the modulus-one source contract into the prime-AP partial-summation bridge.

noncomputable def AnalyticNumberTheory.LargeSieve.principalBadLambdaSupport (q N : ℕ) : Finset ℕ

The non-coprime von Mangoldt support through N.

Equations

• AnalyticNumberTheory.LargeSieve.principalBadLambdaSupport q N = {n ∈ Finset.range (N + 1) | ArithmeticFunction.vonMangoldt n ≠ 0 ∧ ¬n.Coprime q}

def AnalyticNumberTheory.LargeSieve.principalBadPrimePowers (q N : ℕ) : Finset ℕ

The explicit prime-power envelope indexed by p ∣ q and the exponent.

Equations

• AnalyticNumberTheory.LargeSieve.principalBadPrimePowers q N = q.primeFactors.biUnion fun (p : ℕ) => Finset.image (fun (k : ℕ) => p ^ (k + 1)) (Finset.range (N.log2 + 1))

theorem AnalyticNumberTheory.LargeSieve.principalBadLambdaSupport_subset_primePowers {q : ℕ} (hq : 0 < q) (N : ℕ) : principalBadLambdaSupport q N ⊆ principalBadPrimePowers q N

Every non-coprime point supporting Λ is p^k for a prime divisor of q.

theorem AnalyticNumberTheory.LargeSieve.card_principalBadLambdaSupport_le {q : ℕ} (hq : 0 < q) (N : ℕ) : (principalBadLambdaSupport q N).card ≤ q.primeFactors.card * (N.log2 + 1)

There are at most ω(q)(log₂ N+1) bad prime powers through N.

noncomputable def AnalyticNumberTheory.LargeSieve.principalBadLambdaMass (y q : ℕ) : ℂ

The mass deleted from the principal character at modulus q.

Equations

• AnalyticNumberTheory.LargeSieve.principalBadLambdaMass y q = ∑ n ∈ Finset.range (y + 1), if n.Coprime q then 0 else AnalyticNumberTheory.LargeSieve.lambdaNatCoeff n

theorem AnalyticNumberTheory.LargeSieve.coprimeLambdaPrefix_one_eq_add_badMass (y q : ℕ) : coprimeLambdaPrefix y 1 = coprimeLambdaPrefix y q + principalBadLambdaMass y q

Literal partition of the global von Mangoldt prefix into coprime and bad mass.

theorem AnalyticNumberTheory.LargeSieve.norm_principalBadLambdaMass_le_omega {y N q : ℕ} (hq : 0 < q) (hy : y ≤ N) (hN : 2 ≤ N) : ‖principalBadLambdaMass y q‖ ≤ ↑q.primeFactors.card * (↑N.log2 + 1) * Real.log ↑N

Explicit ω(q) bound for the deleted mass.

theorem AnalyticNumberTheory.LargeSieve.norm_principalBadLambdaMass_le_log2 {y N q : ℕ} (hq : 0 < q) (hy : y ≤ N) (hN : 2 ≤ N) : ‖principalBadLambdaMass y q‖ ≤ ↑q.log2 * (↑N.log2 + 1) * Real.log ↑N

The same correction with the elementary ω(q) ≤ log₂ q substitution.

theorem AnalyticNumberTheory.LargeSieve.norm_principalLambdaMainError_le_global_add_bad {y N q : ℕ} (hq : 0 < q) (hy : y ≤ N) (hN : 2 ≤ N) : ‖principalLambdaMainError y q‖ ≤ ‖principalLambdaMainError y 1‖ + ↑q.log2 * (↑N.log2 + 1) * Real.log ↑N

Pointwise principal error at q is the global error plus bad prime powers.

theorem AnalyticNumberTheory.LargeSieve.principalLambdaPrefixMaxError_le_global_add_bad {N q : ℕ} (hq : 0 < q) (hN : 2 ≤ N) : principalLambdaPrefixMaxError N q ≤ principalLambdaPrefixMaxError N 1 + ↑q.log2 * (↑N.log2 + 1) * Real.log ↑N

Uniform principal reduction for every positive modulus.

theorem AnalyticNumberTheory.LargeSieve.sum_principalLambdaPrefixMaxError_le_global {N Q : ℕ} (hN : 2 ≤ N) : ∑ q ∈ Finset.Icc 1 Q, principalLambdaPrefixMaxError N q ≤ ↑Q * principalLambdaPrefixMaxError N 1 + ↑Q * (↑Q.log2 * (↑N.log2 + 1) * Real.log ↑N)

Summing all principal errors through Q costs one copy of the global error per modulus and an explicit Q log₂Q log₂N log N scalar.

theorem AnalyticNumberTheory.LargeSieve.sum_principal_badCorrection_BVRange_payable {N Q : ℕ} {A B C : ℝ} (_hN : 2 ≤ N) (hQ : ↑Q ≤ √↑N / Real.log ↑N ^ B) (hscalar : √↑N / Real.log ↑N ^ B * (↑Q.log2 * (↑N.log2 + 1) * Real.log ↑N) ≤ C * ↑N / Real.log ↑N ^ A) : ∑ q ∈ Finset.Icc 1 Q, ↑q.log2 * (↑N.log2 + 1) * Real.log ↑N ≤ C * ↑N / Real.log ↑N ^ A

In a Q ≤ √N/log^B N range, the complete bad-prime-power aggregate is paid once the displayed scalar (with Q eliminated) fits the target budget.

theorem AnalyticNumberTheory.LargeSieve.standardPrimeAPPrefixMaxError_le_global_principal_bridge {N q : ℕ} (hq : 0 < q) (hN : 2 ≤ N) : MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ discreteAbelAmplifierPrefixMax N * ((↑q.totient)⁻¹ * (principalLambdaPrefixMaxError N 1 + ↑q.log2 * (↑N.log2 + 1) * Real.log ↑N + ∑ χ ∈ nonprincipalCharacters q, lambdaCharacterPrefixMaxAmplitude N q χ) + lambdaPrimePowerCorrectionPrefixMaxError N q) + (↑q.totient)⁻¹ * globalChebyshevToLiSourcePrefixMaxError N

The all-modulus partial-summation bridge with the principal term reduced literally to the modulus-one PNT error plus bad prime powers.

theorem AnalyticNumberTheory.LargeSieve.globalSourceContract_to_all_moduli_primeAPBridge (hsource : GlobalChebyshevToLiPrincipalPNTSourceContract) (A : ℝ) : 0 < A → ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ N → ∀ (q : ℕ), 0 < q → MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ discreteAbelAmplifierPrefixMax N * ((↑q.totient)⁻¹ * (↑q.log2 * (↑N.log2 + 1) * Real.log ↑N + ∑ χ ∈ nonprincipalCharacters q, lambdaCharacterPrefixMaxAmplitude N q χ) + lambdaPrimePowerCorrectionPrefixMaxError N q) + (↑q.totient)⁻¹ * (C * ↑N / Real.log ↑N ^ A)

The global source contract now feeds the prime-AP bridge for every positive q; only the explicit bad-prime-power term and nonprincipal transforms remain.