Rosser lower sieves and Mertens normalization

Depth-zero boundary assembly, lower Rosser density inputs, and standard Bombieri--Vinogradov distribution bounds combine with explicit Mertens and singular-series normalization to give the base lower-sieve asymptotic.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_mul_upperRosserBoundaryChainsFixedDepthDensity_zero_le_log_interval {S : BoundingSieve} {K z Δ s : ℝ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hs : s = Real.log Δ / Real.log z) (hslo : 3 / 2 ≤ s) (hshi : s < 3) (hpow : 2 ≤ z ^ (s / 3)) : ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) 0 ≤ Real.log (z + 1) / Real.log (z ^ (s / 3)) * (1 + K / Real.log (z ^ (s / 3))) - 1

The complete depth-zero outer Rosser contribution is controlled by one dimension-one logarithmic interval. This is the base case for the recursive fixed-depth Darboux comparison.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_mul_upperRosserBoundaryChainsFixedDepthDensity_zero_le_integral_add {S : BoundingSieve} {K z Δ s η : ℝ} (hK : 0 ≤ K) (hη : 0 ≤ η) (hz : 2 ≤ z) (hΔ : 0 < Δ) (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hs : s = Real.log Δ / Real.log z) (hslo : 3 / 2 ≤ s) (hshi : s < 3) (hpow : 2 ≤ z ^ (s / 3)) (hlogRatio : Real.log (z + 1) / Real.log z ≤ 1 + η) (herror : K / (s / 3 * Real.log z) ≤ η) : ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) 0 ≤ (∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * LinearSieve.upperRosserBoundaryMass 0 s a) + 4 * η + 2 * η ^ 2

Quantitative depth-zero Darboux comparison. Once the two elementary logarithmic errors are at most η, the full outer cubic shell differs from its continuous boundary integral by at most 4η + 2η², uniformly in 3 / 2 ≤ s < 3.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_mul_upperRosserBoundaryChainsFixedDepthDensity_zero_eq_zero {S : BoundingSieve} {z Δ s : ℝ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hs : s = Real.log Δ / Real.log z) (hs3 : 3 ≤ s) : ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) 0 = 0

For s ≥ 3, the depth-zero outer cubic shell is empty: all sieving primes lie below z, while the Rosser level lies above z³.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_sum_mul_upperRosserBoundaryChainsFixedDepthDensity_zero_le_integral_add (K ρ : ℝ) (hK : 0 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s < 3 → ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) 0 ≤ (∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * LinearSieve.upperRosserBoundaryMass 0 s a) + ρ

Uniform cutoff form of the depth-zero Darboux comparison. This discharges the power-cutoff, endpoint-logarithm, and local-product errors simultaneously.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_sum_mul_upperRosserBoundaryChainsFixedDepthDensity_zero_le_integral_add_of_three_halves_le (K ρ : ℝ) (hK : 0 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) 0 ≤ (∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * LinearSieve.upperRosserBoundaryMass 0 s a) + ρ

Uniform depth-zero comparison on the whole upper-sieve range. Below 3 it is the quantitative logarithmic-interval estimate; from 3 onward both the discrete cubic shell and its continuous boundary integral vanish.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_sum_mul_upperRosserBoundaryChainsFixedDepthDensity_le_integral_add_of_three_halves_le (k : ℕ) (K ρ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 4 → ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k ≤ (∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * LinearSieve.upperRosserBoundaryMass k s a) + ρ

Uniform comparison of a complete outer Rosser contribution at an arbitrary fixed depth with its continuous boundary integral.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_sum_range_sum_mul_upperRosserBoundaryChainsFixedDepthDensity_le_upperRosserFiniteBoundaryFactor_sub_one_add (L : ℕ) (K ρ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 4 → ∑ k ∈ Finset.range L, ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k ≤ LinearSieve.upperRosserFiniteBoundaryFactor L s - 1 + ρ

A finite collection of complete outer Rosser depths is uniformly bounded by the corresponding finite continuous boundary factor. The cutoff is the maximum of the finitely many fixed-depth cutoffs, with the error split at each successor step; the empty range needs no cutoff beyond 2.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mainSum_upperRosserWeight_le_boundaryChains {S : BoundingSieve} {K z Δ s : ℝ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hs : s = Real.log Δ / Real.log z) (hslo : 3 / 2 ≤ s) : BoundingSieve.mainSum (LinearSieve.upperRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1)) ≤ (1 + ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * (Real.log (z + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)) * ∑ t ∈ {p ∈ S.prodPrimes.primeFactors | q < p}.powerset with (LinearSieve.UpperRosserBoundarySet (⌊Δ⌋₊ + 1) q) t, ∏ p ∈ t, S.nu p / (1 - S.nu p))) * ∏ p ∈ S.prodPrimes.primeFactors, (1 - S.nu p)

Finite upper-sieve bound obtained from the Rosser path expansion and the dimension-one local-product hypothesis. The sole remaining analytic quantity is the selected cubic-boundary chain sum displayed on the right.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mainSum_upperRosserWeight_le_boundaryChains_by_depth {S : BoundingSieve} {K z Δ s : ℝ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hs : s = Real.log Δ / Real.log z) (hslo : 3 / 2 ≤ s) : BoundingSieve.mainSum (LinearSieve.upperRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1)) ≤ (1 + ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * (Real.log (z + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)) * ∑ k ∈ Finset.range ({p ∈ S.prodPrimes.primeFactors | q < p}.card + 1), LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k)) * ∏ p ∈ S.prodPrimes.primeFactors, (1 - S.nu p)

The finite upper-sieve bound with the selected boundary mass indexed directly by Buchstab pair depth. This is the exact discrete expression to split into a fixed-depth approximation and a large-depth tail.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_jurkatRichertSource_dimensionOneLocalProductBound : ∃ (K : ℝ), 1 < K ∧ ∀ (N : ℕ), HasDimensionOneLocalProductBound (jurkatRichertSourceBoundingSieve N) K

The literal source sieve inherits the real-endpoint dimension-one estimate from the Goldbach local-factor interval bound.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSieveRatio_eq {N : ℕ} {ε : ℝ} (hN : 1 < N) : Real.log (↑N ^ (1 / 2 - ε)) / Real.log (↑N ^ (1 / 10)) = 5 - 10 * ε

Before the integer cutoff is taken, Chen's level and sifting powers have the exact logarithmic ratio 5 - 10ε.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.dimensionOneLowerLinearSieveFactor (s : ℝ) : ℝ

The standard dimension-one lower linear-sieve factor on 4 ≤ s ≤ 6. It is the solution of (s f(s))' = F(s - 1) obtained from the preceding upper-sieve branch.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.dimensionOneLowerLinearSieveFactor s = 2 * Real.exp Real.eulerMascheroniConstant / s * (Real.log (s - 1) + ∫ (u : ℝ) in 3..s - 1, MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral u / u)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.dimensionOneLowerLinearSieveFactor_five : dimensionOneLowerLinearSieveFactor 5 = jurkatRichertBaseSieveFactor jurkatRichertJ

The generic lower factor at ratio five is exactly Chen's equation (26) factor.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.dimensionOneLowerLinearSieveFactor_continuousAt_five : ContinuousAt dimensionOneLowerLinearSieveFactor 5

The standard lower linear-sieve factor is continuous at the ratio used in Chen's base sieve.

def MathlibNt.SieveTheory.SwitchingPrinciple.DimensionOneLowerRosserDensityFundamentalLemma : Prop

The generic dimension-one lower fundamental lemma for the explicit Rosser coefficient. For an arbitrary finite bounding sieve whose primes lie below z, real level Δ, and ratio s = log Δ / log z near five, the density sum is at least (f(s) - ρ) V(S).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.DimensionOneLowerRosserDensityFundamentalLemma = ∀ (K ρ : ℝ), 1 < K → 0 < ρ → ∃ (z₀ : ℝ), ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 2 ≤ z → 0 < Δ → MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 4 ≤ s → s ≤ 6 → (MathlibNt.SieveTheory.SwitchingPrinciple.dimensionOneLowerLinearSieveFactor s - ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S ≤ BoundingSieve.mainSum (MathlibNt.SieveTheory.LinearSieve.lowerRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1))

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseLowerRosserDensityFundamentalLemma : Prop

Compatibility form of the lower density lemma specialized to Chen's source family. It is derived below from the generic dimension-one theorem.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseLowerRosserDensityFundamentalLemma = ∀ (K : ℝ), 1 < K → (∀ᶠ (N : ℕ) in Filter.atTop, MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceBoundingSieve N) K) → ∀ (δ : ℝ), 0 < δ → ∃ (ε : ℝ), 0 < ε ∧ ε < 2 / 5 ∧ ∀ᶠ (N : ℕ) in Filter.atTop, (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseSieveFactor MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertJ - δ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceBoundingSieve N) ≤ BoundingSieve.mainSum (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseLowerRosserWeight N ε)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertBaseLowerRosserDensityFundamentalLemma_of_generic (hfund : DimensionOneLowerRosserDensityFundamentalLemma) : ChenJurkatRichertBaseLowerRosserDensityFundamentalLemma

The generic dimension-one lower fundamental lemma specializes to Chen's source family. Continuity at ratio five absorbs the displacement s = 5 - 10ε, while the source local-product and prime-cutoff facts supply the generic hypotheses.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseLowerRosserStandardInput : Prop

The remaining standard source input is precisely the density-sum fundamental lemma, since the local-product condition is now proved above.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseLowerRosserStandardInput = MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseLowerRosserDensityFundamentalLemma

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseLowerSieveFundamentalLemma : Prop

The source-faithful lower-sieve fundamental lemma at D = N^(1/2-ε). It retains the exact finite Goldbach remainder rather than folding distribution or Mertens normalization into the conclusion.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseLowerSieveFundamentalLemma = ∀ (δ : ℝ), 0 < δ → ∃ (ε : ℝ), 0 < ε ∧ ε < 1 / 2 ∧ ∀ᶠ (N : ℕ) in Filter.atTop, Even N → (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseSieveFactor MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertJ - δ) * ((MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceBoundingSieve N).totalMass * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceBoundingSieve N)) - MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceRemainderSum N ε ≤ BoundingSieve.siftedSum

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseLowerRosserWeight_certificate {N : ℕ} {ε : ℝ} (hN : 1 ≤ N) (hε : ε < 2 / 5) : LinearSieve.IsLowerRosserCertificate (jurkatRichertSourceSiftingProduct N) (jurkatRichertSourceLowerLevel N ε)

The source Rosser coefficient is a finite lower-Möbius weight at its stated level. This is the combinatorial half of the fundamental lemma.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseLowerRosserError_le (N : ℕ) (ε : ℝ) : LinearSieve.lowerErrSum (jurkatRichertSourceBoundingSieve N) (jurkatRichertSourceLowerLevel N ε) (jurkatRichertBaseLowerRosserWeight N ε) ≤ jurkatRichertSourceRemainderSum N ε

The Rosser error term is bounded by exactly the level-restricted Goldbach remainder appearing in the source statement.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertBaseLowerSieveFundamentalLemma_of_density (hinput : ChenJurkatRichertBaseLowerRosserStandardInput) : ChenJurkatRichertBaseLowerSieveFundamentalLemma

The standard density-sum fundamental lemma, together with the fully finite Rosser expansion above, proves Chen's base lower-sieve statement.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseGoldbachDistribution : Prop

The Goldbach AP distribution input required by the base lower sieve: the exact squarefree remainder sum through N^(1/2-ε) is negligible on the 𝔖(N) N / log² N scale.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseGoldbachDistribution = ∀ (ε : ℝ), 0 < ε → ε < 1 / 2 → ∀ (δ : ℝ), 0 < δ → ∀ᶠ (N : ℕ) in Filter.atTop, Even N → MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceRemainderSum N ε ≤ δ * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertBaseGoldbachDistribution_of_standardBV (hBV : BombieriVinogradov.StandardBombieriVinogradov) : ChenJurkatRichertBaseGoldbachDistribution

The standard Bombieri--Vinogradov literature interface supplies precisely the base Goldbach distribution estimate needed by the source lower sieve. The proof retains the finite source support, reduces its moduli to canonical reduced residues, and absorbs the exceptional cutoff-prime fibres by their unconditional power-saving endpoint bound.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseMertensNormalization : Prop

Chen equation (25), in the one-sided form needed here: the source Goldbach main term has normalization 20 exp(-γ) 𝔖(N) N / log² N.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseMertensNormalization = ∀ (δ : ℝ), 0 < δ → ∀ᶠ (N : ℕ) in Filter.atTop, Even N → (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertMertensFactor - δ) * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 ≤ (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceBoundingSieve N).totalMass * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceBoundingSieve N)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.tendsto_log_jurkatRichertSourceZ_sub_one_div_log : Filter.Tendsto (fun (N : ℕ) => Real.log ↑(jurkatRichertSourceZ N - 1) / Real.log ↑N) Filter.atTop (nhds (1 / 10))

The literal source cutoff has logarithmic scale 1/10.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.eventually_two_mul_liuSingularSeries_le_source_truncated (η : ℝ) (hη : 0 < η) : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → 2 * SingularSeries.liuSingularSeries N ≤ (1 + η) * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (jurkatRichertSourceZ N - 1)

Uniform varying-N comparison at Chen's literal source cutoff.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.eventually_jurkatRichertSourceGoldbachSieveProduct_lower (ε : ℝ) (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → (10 * Real.exp (-Real.eulerMascheroniConstant) - ε) * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (jurkatRichertSourceZ N - 1) / Real.log ↑N ≤ MertensTheorem.goldbachSieveProduct N (jurkatRichertSourceZ N)

Mertens' product theorem at the literal source cutoff, uniformly in N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertBaseMertensNormalization : ChenJurkatRichertBaseMertensNormalization

Chen's equation (25) follows from the exact Goldbach product identity, Mertens' product theorem, and the uniform source-cutoff singular-series bridge.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.eventually_jurkatRichertSourceGoldbachSieveProduct_upper (η : ℝ) (hη : 0 < η) : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → MertensTheorem.goldbachSieveProduct N (jurkatRichertSourceZ N) ≤ (20 * Real.exp (-Real.eulerMascheroniConstant) + η) * SingularSeries.liuSingularSeries N / Real.log ↑N

Mertens' product theorem at the literal source cutoff, with Liu's genuine normalization and an upper error uniform in the even integer N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.eventually_liuLogarithmicIntegral_le (η : ℝ) (hη : 0 < η) : ∀ᶠ (N : ℕ) in Filter.atTop, LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) ↑N ≤ (1 + η) * ↑N / Real.log ↑N

The genuine logarithmic integral has the sharp upper normalization needed when it is multiplied by the Mertens sieve product.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.eventually_jurkatRichertSourceCommonDensity_upper (η : ℝ) (hη : 0 < η) : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) ↑N * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (jurkatRichertSourceBoundingSieve N) ≤ (20 * Real.exp (-Real.eulerMascheroniConstant) + η) * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

The common mass in every conditioned source sieve has the sharp Liu-normalized upper asymptotic.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseLowerSieveAsymptotic : Prop

The base term in Chen's equation (26), using equation (25) for its Mertens normalization.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertBaseLowerSieveAsymptotic = ∀ (η : ℝ), 0 < η → ∀ᶠ (N : ℕ) in Filter.atTop, Even N → (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseMainCoefficient MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertJ - η) * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 ≤ ↑(MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceCandidates N).card

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertBaseLowerSieveAsymptotic_of_inputs (hlower : ChenJurkatRichertBaseLowerSieveFundamentalLemma) (hdistribution : ChenJurkatRichertBaseGoldbachDistribution) : ChenJurkatRichertBaseLowerSieveAsymptotic

The literal base asymptotic follows from the level-N^(1/2-ε) lower-sieve fundamental lemma and Goldbach AP distribution for its finite remainder. Equation (25)'s Mertens normalization is unconditional.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertBaseLowerSieveAsymptotic_of_literature_inputs (hLowerDensity : DimensionOneLowerRosserDensityFundamentalLemma) (hBV : BombieriVinogradov.StandardBombieriVinogradov) : ChenJurkatRichertBaseLowerSieveAsymptotic

The base asymptotic directly from its two literature inputs. The lower Rosser density fundamental lemma and standard Bombieri--Vinogradov are converted to the finite lower-sieve and Goldbach-distribution APIs above.