Varying-prime sieves and cutoff corrections

Upper Rosser certificates and weighted Bombieri--Vinogradov remainders control the medium-prime aggregate. Nonreduced residues and cutoff fibers are bounded explicitly before comparison with the corrected weighted count.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQDensityModel (N : ℕ) (ε : ℝ) : ℝ

The explicit q-local density model before prime-q partial summation. It retains the exact 1 / (q - 1) mass and the varying upper-sieve factor.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQDensityModel N ε = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes N, (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditionedBoundingSieve N q).totalMass * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditionedBoundingSieve N q) * MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperSieveRatio N q ε)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQDensityModel_eq_common_mul (N : ℕ) (ε : ℝ) : jurkatRichertSourceVaryingQDensityModel N ε = LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) ↑N * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (jurkatRichertSourceBoundingSieve N) * ∑ q ∈ jurkatRichertSourceMediumPrimes N, jurkatRichertUpperLinearSieveFactor (jurkatRichertSourceUpperSieveRatio N q ε) / (↑q - 1)

The conditioned densities have one common Goldbach sieve mass. Only the exact local factor 1 / (q - 1) and the varying linear-sieve weight remain inside the prime sum.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQUpperRosserWeight (N q : ℕ) (ε : ℝ) (d : ℕ) : ℝ

The explicit upper Rosser coefficient at Chen's exact varying level floor (N^(1/2-ε) / q) + 1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQUpperRosserWeight N q ε d = MathlibNt.SieveTheory.LinearSieve.upperRosserWeight (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct N) (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperLevel N q ε) d

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQUpperRosserWeight_hasUpperLevelSupport (N q : ℕ) (ε : ℝ) : LinearSieve.HasUpperLevelSupport (jurkatRichertSourceSiftingProduct N) (jurkatRichertSourceUpperLevel N q ε) (jurkatRichertSourceVaryingQUpperRosserWeight N q ε)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_jurkatRichertSourceVaryingQUpperRosserWeight_le_one (N q d : ℕ) (ε : ℝ) : |jurkatRichertSourceVaryingQUpperRosserWeight N q ε d| ≤ 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_jurkatRichertSourceVaryingQUpperRosserWeight_le_threePow (N q d : ℕ) (ε : ℝ) : |jurkatRichertSourceVaryingQUpperRosserWeight N q ε d| ≤ 3 ^ d.primeFactors.card

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQUpperRosserWeight_certificate {N q : ℕ} {ε : ℝ} (hN : 1 < N) (hε : ε < 1 / 60) (hq : q ∈ jurkatRichertSourceMediumPrimes N) : LinearSieve.IsUpperRosserCertificate (jurkatRichertSourceSiftingProduct N) (jurkatRichertSourceUpperLevel N q ε)

At every medium prime and for the epsilon range supplied by Chen's prime-sum argument, the explicit coefficient is a finite upper-Möbius certificate.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQMainSum (N : ℕ) (ε : ℝ) : ℝ

The exact sum of the q-conditioned upper Rosser main terms.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQMainSum N ε = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes N, (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditionedBoundingSieve N q).totalMass * BoundingSieve.mainSum (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQUpperRosserWeight N q ε)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQRemainderSum (N : ℕ) (ε : ℝ) : ℝ

The exact sum of the q-conditioned, level-D/q upper Rosser remainders.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQRemainderSum N ε = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes N, MathlibNt.SieveTheory.LinearSieve.upperErrSum (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditionedBoundingSieve N q) (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperLevel N q ε) (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQUpperRosserWeight N q ε)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrime_coprime_siftingDivisor {N q d : ℕ} (hq : q ∈ jurkatRichertSourceMediumPrimes N) (hd : d ∣ jurkatRichertSourceSiftingProduct N) : q.Coprime d

A source medium prime is coprime to every divisor of the source sifting product: the prime lies strictly above N^(1/10), whereas every prime factor of the product lies at or below that cutoff.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditionedMultSum_eq_modEq_count (N q d : ℕ) (hEven : Even N) (hN : 2 < N) (hq : q ∈ jurkatRichertSourceMediumPrimes N) (hd : d ∣ jurkatRichertSourceSiftingProduct N) : BoundingSieve.multSum d = ↑{p ∈ jurkatRichertSourceUnsiftedPrimeSupport N | p ≡ N [MOD q * d]}.card

The conditioned multSum is exactly the source prime-support count in the single progression modulo q*d.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditionedRem_eq_modEq_count (N q d : ℕ) (hEven : Even N) (hN : 2 < N) (hq : q ∈ jurkatRichertSourceMediumPrimes N) (hd : d ∣ jurkatRichertSourceSiftingProduct N) : BoundingSieve.rem d = ↑{p ∈ jurkatRichertSourceUnsiftedPrimeSupport N | p ≡ N [MOD q * d]}.card - BombieriVinogradov.trueLogarithmicIntegral ↑N / ↑(q * d).totient

On the source divisor carrier, the conditioned remainder is the exact prime-support AP count modulo q*d, centered at li(N)/φ(q*d).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperLevel_mul_le {N q d : ℕ} {ε : ℝ} (hq : q ∈ jurkatRichertSourceMediumPrimes N) (hd : d < jurkatRichertSourceUpperLevel N q ε) : ↑(q * d) ≤ ↑N ^ (1 / 2 - ε)

Membership in the exact integer level ⌊N^(1/2-ε)/q⌋ + 1 implies the required real modulus cutoff, including the floor endpoint.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSource_mul_mod_coprime {N q d : ℕ} (hq : q ∈ jurkatRichertSourceMediumPrimes N) (hd : d ∣ jurkatRichertSourceSiftingProduct N) (hqN : ¬q ∣ N) : (N % (q * d)).Coprime (q * d)

If the medium prime does not divide N, then N mod (q*d) is the canonical reduced residue for the combined modulus.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSource_mul_mod_mem_unitResidues {N q d : ℕ} (hq : q ∈ jurkatRichertSourceMediumPrimes N) (hd : d ∣ jurkatRichertSourceSiftingProduct N) (hqN : ¬q ∣ N) : N % (q * d) ∈ AnalyticNumberTheory.Sieve.unitResidues (q * d)

The preceding canonical residue belongs to the standard reduced-residue carrier used by the Bombieri--Vinogradov maximum.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSource_mediumPrime_mul_siftingDivisor_injective {N q₁ q₂ d₁ d₂ : ℕ} (hq₁ : q₁ ∈ jurkatRichertSourceMediumPrimes N) (hq₂ : q₂ ∈ jurkatRichertSourceMediumPrimes N) (_hd₁ : d₁ ∣ jurkatRichertSourceSiftingProduct N) (hd₂ : d₂ ∣ jurkatRichertSourceSiftingProduct N) (hmul : q₁ * d₁ = q₂ * d₂) : q₁ = q₂ ∧ d₁ = d₂

The map (q,d) ↦ q*d is injective on medium primes times source sifting divisors.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceReducedWeightedBVSum (N : ℕ) (ε : ℝ) : ℝ

The genuinely 3^ω-weighted standard AP-error sum on Chen's exact reduced (q,d) carrier. The modulus is q*d, not d, and the strict integer level is the floor-safe source level ⌊N^(1/2-ε)/q⌋ + 1.

There is no hidden multiplicity in this sum: the preceding injectivity theorem shows that (q,d) ↦ q*d has fibres of cardinality one on this carrier.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceReducedWeightedBVSum N ε = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes N with ¬q ∣ N, ∑ d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct N).divisors with d < MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperLevel N q ε, 3 ^ d.primeFactors.card * MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPMaxError N (q * d)

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQWeightedBombieriVinogradov : Prop

Source-faithful divisor-weighted Bombieri--Vinogradov interface.

For every positive logarithmic saving, this controls the actual reduced (q,d) carrier occurring in Chen's varying-q upper sieve, with its genuine 3^ω(d) Rosser majorant and modulus q*d. The proof from ordinary StandardBombieriVinogradov is supplied downstream by Richert1969.chenWeightedBombieriVinogradov_of_standard; the unconditional instance is in ChenVaryingQWeightedBVUnconditional. Fibre uniqueness is supplied by jurkatRichertSource_mediumPrime_mul_siftingDivisor_injective, so this pair-indexed formulation counts every combined modulus with multiplicity one.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQWeightedBombieriVinogradov = ∀ (ε : ℝ), 0 < ε → ε < 1 / 6 → ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceReducedWeightedBVSum N ε ≤ C * ↑N / Real.log ↑N ^ A

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQWeightMass (N : ℕ) (ε : ℝ) : ℝ

The total 3^ω(d) mass of the exact varying-level divisor carrier.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQWeightMass N ε = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes N, ∑ d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct N).divisors with d < MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperLevel N q ε, 3 ^ d.primeFactors.card

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceNonreducedCenterSum (N : ℕ) (ε : ℝ) : ℝ

The nonreduced (q ∣ N) main-term contribution left after bounding its prime count by one. This is kept outside the weighted BV hypothesis.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceNonreducedCenterSum N ε = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes N with q ∣ N, ∑ d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct N).divisors with d < MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperLevel N q ε, 3 ^ d.primeFactors.card * (MathlibNt.SieveTheory.BombieriVinogradov.trueLogarithmicIntegral ↑N / ↑(q * d).totient)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQUnconditionalCorrection (N : ℕ) (ε : ℝ) : ℝ

All source corrections not paid for by the weighted BV input: the removed small prime fibres on reduced lanes, the at-most-one prime on nonreduced lanes, and the nonreduced centering terms.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQUnconditionalCorrection N ε = (↑(MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceExceptionalPrimes N).card + 1) * MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQWeightMass N ε + MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceNonreducedCenterSum N ε

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_jurkatRichertSourceConditionedRem_le_standardMax_add_exceptional (N q d : ℕ) (hEven : Even N) (hN : 2 < N) (hq : q ∈ jurkatRichertSourceMediumPrimes N) (hd : d ∣ jurkatRichertSourceSiftingProduct N) (hqN : ¬q ∣ N) : |BoundingSieve.rem d| ≤ BombieriVinogradov.standardPrimeAPMaxError N (q * d) + ↑(jurkatRichertSourceExceptionalPrimes N).card

On a reduced q-lane the exact conditioned source remainder is bounded by the standard reduced-residue AP maximum plus the explicit removed-prime correction.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditioned_modEq_card_le_one_of_dvd (N q d : ℕ) (hq : q ∈ jurkatRichertSourceMediumPrimes N) (hqN : q ∣ N) : {p ∈ jurkatRichertSourceUnsiftedPrimeSupport N | p ≡ N [MOD q * d]}.card ≤ 1

If q ∣ N, every prime in the conditioned progression modulo q*d equals q; hence the exact source count on this nonreduced lane is at most one.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_jurkatRichertSourceConditionedRem_le_one_add_center_of_dvd (N q d : ℕ) (hEven : Even N) (hN : 2 < N) (hq : q ∈ jurkatRichertSourceMediumPrimes N) (hd : d ∣ jurkatRichertSourceSiftingProduct N) (hqN : q ∣ N) : |BoundingSieve.rem d| ≤ 1 + BombieriVinogradov.trueLogarithmicIntegral ↑N / ↑(q * d).totient

The exact nonreduced conditioned remainder is bounded without any Bombieri--Vinogradov input.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQRemainderSum_le_weightedBV_add_correction (N : ℕ) (ε : ℝ) (hEven : Even N) (hN : 2 < N) : jurkatRichertSourceVaryingQRemainderSum N ε ≤ jurkatRichertSourceReducedWeightedBVSum N ε + jurkatRichertSourceVaryingQUnconditionalCorrection N ε

Exact expansion of upperErrSum, with reduced lanes paid for by the genuinely weighted BV sum and every nonreduced or source-support correction left in the explicit unconditional term.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_jurkatRichertSource_divisorWeight_bound : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ), 3 ≤ N → ∑ d ∈ (jurkatRichertSourceSiftingProduct N).divisors, 3 ^ d.primeFactors.card / ↑d.totient ≤ C * Real.log ↑N ^ 3

The source sifting product satisfies the uniform 3^ω/φ divisor bound needed for all correction terms.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes_card_cast_le (N : ℕ) (hN : 1 ≤ N) : ↑(jurkatRichertSourceMediumPrimes N).card ≤ 2 * ↑N ^ (1 / 3)

The medium-prime carrier has the elementary cardinality bound supplied by its upper cutoff q ≤ N^(1/3).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQWeightMass_le (C : ℝ) (hC : ∀ (N : ℕ), 3 ≤ N → ∑ d ∈ (jurkatRichertSourceSiftingProduct N).divisors, 3 ^ d.primeFactors.card / ↑d.totient ≤ C * Real.log ↑N ^ 3) (N : ℕ) (ε : ℝ) (hN : 3 ≤ N) (hε : 0 < ε) : jurkatRichertSourceVaryingQWeightMass N ε ≤ 2 * C * ↑N ^ (5 / 6) * Real.log ↑N ^ 3

The total coefficient mass on all varying levels is power-saving before any analytic distribution theorem is used.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceNonreducedPrimes_card_le_primeFactors (N : ℕ) (hN : 0 < N) : {q ∈ jurkatRichertSourceMediumPrimes N | q ∣ N}.card ≤ N.primeFactors.card

Medium primes in the nonreduced lane are distinct prime divisors of N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceNonreducedCenterSum_le (C : ℝ) (hC : ∀ (N : ℕ), 3 ≤ N → ∑ d ∈ (jurkatRichertSourceSiftingProduct N).divisors, 3 ^ d.primeFactors.card / ↑d.totient ≤ C * Real.log ↑N ^ 3) (N : ℕ) (ε : ℝ) (hN : 3 ≤ N) : jurkatRichertSourceNonreducedCenterSum N ε ≤ Real.log ↑N / Real.log 2 * (2 * BombieriVinogradov.trueLogarithmicIntegral ↑N / ↑N ^ (1 / 10) * (C * Real.log ↑N ^ 3))

The nonreduced centering terms have a power-saving factor because every such medium prime divides N and is larger than N^(1/10).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.eventually_jurkatRichertSourceVaryingQUnconditionalCorrection_le (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) : ∀ᶠ (N : ℕ) in Filter.atTop, jurkatRichertSourceVaryingQUnconditionalCorrection N ε ≤ δ * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

The nonreduced lanes and the source exceptional-prime corrections are unconditionally power-saving. No part of this estimate is included in the weighted Bombieri--Vinogradov hypothesis.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimeAggregate_le_main_add_remainder (N : ℕ) (ε : ℝ) (hN : 1 < N) (hε : ε < 1 / 60) : jurkatRichertSourceMediumPrimeAggregate N ≤ jurkatRichertSourceVaryingQMainSum N ε + jurkatRichertSourceVaryingQRemainderSum N ε

The q-conditioned finite upper sieves sum to Chen's literal medium-prime aggregate, with no asymptotic step: only their exact main and remainder sums remain.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimeAggregate_eq (N : ℕ) : jurkatRichertSourceMediumPrimeAggregate N = ∑ p ∈ jurkatRichertSourceCandidates N, ↑(jurkatRichertSourceMediumPrimeCount N p)

Finite Fubini identity between Chen's displayed q-outer aggregate and the distinct-prime divisor count attached to each source candidate.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceWeightedCount_eq (N : ℕ) : jurkatRichertSourceWeightedCount N = ↑(jurkatRichertSourceCandidates N).card - jurkatRichertSourceMediumPrimeAggregate N / 2

The exact finite weighted-count identity used to consume the two sieve asymptotics in Chen's Lemma 9.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceWeightedCount_sub_boundary_le_distinct (N : ℕ) (hNbig : 2 ^ 110 < N) (hEven : Even N) : jurkatRichertSourceWeightedCount N - 10 * ↑N ^ (9 / 10) ≤ jurkatRichertDistinctWeightedCount N

Explicit finite comparison between Chen's literal real-cutoff weight and the corrected distinct-prime weight. The only positive losses are the lower floor fibre (at most 2 N^(9/10) candidates, each costing at most four), and the two exceptional source fibres p = 2 and N - p = 1.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertDistinctWeightedLowerBound : Prop

Source-faithful Chen/Jurkat--Richert lower-sieve input. Chen 1973, Lemma 9 (equations (25)--(27)), lower-bounds the finite weight

#candidates - (1/2) * Σ_q #candidates_q,

where the medium primes q are distinct. Its analytic proof requires:

• the Mertens normalization Γ_N(z) ~ 20 exp(-γ) 𝔖(N) / log N;
• the lower sieve at level N^(1/2-ε) and the q-conditioned upper sieves at the varying levels N^(1/2-ε)/q;
• the integral estimate J - K/4 ≥ -0.0164725, whose final coefficient conversion is jurkatRichert_mainCoefficient_ge_twoPoint6408.

The real cutoff inequalities and the exceptional p = 2/unit fibres are kept in this source object. Valuation multiplicity and the ordered-triple penalty are deliberately absent.

Equations

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

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceLowerLevel (N : ℕ) (ε : ℝ) : ℕ

The integral-free natural-number level corresponding exactly to d ≤ N^(1/2-ε).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceLowerLevel N ε = ⌊↑N ^ (1 / 2 - ε)⌋₊ + 1

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseLowerRosserWeight (N : ℕ) (ε : ℝ) (d : ℕ) : ℝ

The explicit lower Rosser coefficient used for Chen's base sieve.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseLowerRosserWeight N ε d = MathlibNt.SieveTheory.LinearSieve.lowerRosserWeight (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct N) (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceLowerLevel N ε) d