theorem AnalyticNumberTheory.LargeSieve.coprimeLambdaPrefix_one_eq_psi (y : ℕ) : coprimeLambdaPrefix y 1 = ↑(Chebyshev.psi ↑y)

At modulus one the principal character prefix is literally the real Chebyshev ψ value at the integer endpoint.

theorem AnalyticNumberTheory.LargeSieve.norm_principalLambdaMainError_one_eq_psi_sub (y : ℕ) : ‖principalLambdaMainError y 1‖ = |Chebyshev.psi ↑y - ↑y|

Exact pointwise bridge from the production principal error at modulus one to the authoritative real-valued PNT error.

theorem AnalyticNumberTheory.LargeSieve.principalLambdaPrefixMaxError_one_eq_psi_prefixMax (N : ℕ) : principalLambdaPrefixMaxError N 1 = (Finset.image (fun (y : ℕ) => |Chebyshev.psi ↑y - ↑y|) (Finset.range (N + 1))).max' ⋯

Exact finite bridge, including the production prefix maximum.

Deterministic discrete-Abel versus true-li source

theorem AnalyticNumberTheory.LargeSieve.discreteAbelLiMain_eq_sum_reciprocalLogWeight (y : ℕ) : discreteAbelLiMain y = ∑ n ∈ Finset.range (y + 1), reciprocalLogWeight n

The Abel main term telescopes exactly to the reciprocal-log Riemann sum.

theorem AnalyticNumberTheory.LargeSieve.discreteAbelLiMain_sub_integral_bounds {y : ℕ} (hy : 2 ≤ y) : 1 / Real.log ↑y ≤ discreteAbelLiMain y - ∫ (t : ℝ) in 2..↑y, 1 / Real.log t ∧ discreteAbelLiMain y - ∫ (t : ℝ) in 2..↑y, 1 / Real.log t ≤ 1 / Real.log 2

The discrete reciprocal-log sum differs from the integral by a bounded endpoint correction. This is a genuine integral comparison, not a source assumption.

theorem AnalyticNumberTheory.LargeSieve.globalChebyshevToLiSourceError_le_two_div_log_two {y : ℕ} (hy : 2 ≤ y) : globalChebyshevToLiSourceError y ≤ 2 / Real.log 2

The genuine-li discrepancy is bounded by an absolute endpoint constant.

noncomputable def AnalyticNumberTheory.LargeSieve.globalLiDiscreteErrorBound : ℝ

A uniform deterministic bound valid also at the two artificial low endpoints of the prefix maximum.

Equations

• AnalyticNumberTheory.LargeSieve.globalLiDiscreteErrorBound = max (AnalyticNumberTheory.LargeSieve.globalChebyshevToLiSourceError 0) (max (AnalyticNumberTheory.LargeSieve.globalChebyshevToLiSourceError 1) (2 / Real.log 2))

theorem AnalyticNumberTheory.LargeSieve.globalChebyshevToLiSourceError_le_bound (y : ℕ) : globalChebyshevToLiSourceError y ≤ globalLiDiscreteErrorBound

theorem AnalyticNumberTheory.LargeSieve.globalChebyshevToLiSourcePrefixMaxError_le_bound (N : ℕ) : globalChebyshevToLiSourcePrefixMaxError N ≤ globalLiDiscreteErrorBound

theorem AnalyticNumberTheory.LargeSieve.discreteAbelAmplifier_le_two_div_log_two (y : ℕ) : discreteAbelAmplifier y ≤ 2 / Real.log 2

The total variation of the reciprocal-log Abel kernel is an absolute constant: after its jump at 2, the weight is nonnegative and decreasing.

theorem AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax_le_two_div_log_two (N : ℕ) : discreteAbelAmplifierPrefixMax N ≤ 2 / Real.log 2

Uniform logarithmic payment

theorem AnalyticNumberTheory.LargeSieve.principalLambdaPrefixMaxError_one_eventually_le (A : ℝ) (hA : 0 < A) : ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, principalLambdaPrefixMaxError N 1 ≤ K * ↑N / Real.log ↑N ^ A

MediumPNT, made uniform over the genuine production prefix maximum.

theorem AnalyticNumberTheory.LargeSieve.globalChebyshevToLiPrincipalPNTSource : GlobalChebyshevToLiPrincipalPNTSourceContract

Closed production source: the real MediumPNT theorem supplies the principal modulus-one prefix, while the Abel kernel and true-li discrepancy are discharged by the deterministic bounds above.