Source sieve carriers and Jurkat--Richert factors

The literal source cutoffs define sieve carriers and arithmetic-progression remainders, including exceptional endpoints. Conditioned carriers and explicit upper linear-sieve factors retain their precise boundary conventions.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

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

The distinct-medium-prime count in Chen's Lemma 9. Each prime q ∈ [correctedChenZ N, correctedChenY N) dividing N - p contributes once, regardless of its valuation.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertDistinctWeightedCount N = ↑(MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N).card - MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenQ1Count N / 2

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceCandidates (N : ℕ) : Finset ℕ

Chen's literal P_N(N, N^(1/10)) carrier: primes p ≤ N for which no odd prime through the real cutoff N^(1/10) divides N - p.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceCandidates N = {p ∈ Finset.range (N + 1) | Nat.Prime p ∧ ∀ (r : ℕ), Nat.Prime r → 2 < r → ↑r ≤ ↑N ^ (1 / 10) → ¬r ∣ N - p}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceZ (N : ℕ) : ℕ

The integer endpoint whose strict range is Chen's literal real cutoff r ≤ N^(1/10).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceZ N = ⌊↑N ^ (1 / 10)⌋₊ + 1

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct (N : ℕ) : ℕ

Odd cutoff primes not dividing N; these are the primes treated by the Goldbach density 1 / (p - 1).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct N = {r ∈ Finset.range (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceZ N) | Nat.Prime r ∧ 2 < r ∧ ¬r ∣ N}.prod id

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct_squarefree (N : ℕ) : Squarefree (jurkatRichertSourceSiftingProduct N)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct_ne_zero (N : ℕ) : jurkatRichertSourceSiftingProduct N ≠ 0

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct_primeFactors (N : ℕ) : (jurkatRichertSourceSiftingProduct N).primeFactors = {r ∈ Finset.range (jurkatRichertSourceZ N) | Nat.Prime r ∧ 2 < r ∧ ¬r ∣ N}

theorem MathlibNt.SieveTheory.SwitchingPrinciple.prime_dvd_jurkatRichertSourceSiftingProduct {N r : ℕ} (hr : Nat.Prime r) : r ∣ jurkatRichertSourceSiftingProduct N ↔ 2 < r ∧ ↑r ≤ ↑N ^ (1 / 10) ∧ ¬r ∣ N

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUnsiftedPrimeSupport (N : ℕ) : Finset ℕ

Before the Goldbach sieve, primes whose complement is divisible by an odd cutoff prime dividing N are removed. Such a prime is the exceptional prime itself; separating it is what makes every remaining local density 1 / (r - 1).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUnsiftedPrimeSupport N = {p ∈ Finset.range (N + 1) | Nat.Prime p ∧ ∀ (r : ℕ), Nat.Prime r → 2 < r → ↑r ≤ ↑N ^ (1 / 10) → r ∣ N → ¬r ∣ N - p}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUnsiftedComplements (N : ℕ) : Finset ℕ

The source Goldbach sequence A = {N - p : p ≤ N, p prime}, after only the exceptional residue-zero cutoff primes have been removed.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUnsiftedComplements N = Finset.image (fun (p : ℕ) => N - p) (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUnsiftedPrimeSupport N)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceBoundingSieve (N : ℕ) : BoundingSieve

Chen's literal base sequence as a BoundingSieve.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceBoundingSieve N = { support := MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUnsiftedComplements N, prodPrimes := MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct N, prodPrimes_squarefree := ⋯, weights := fun (x : ℕ) => 1, weights_nonneg := MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceBoundingSieve._proof_1, totalMass := MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) ↑N, nu := AnalyticNumberTheory.Sieve.goldbachNu, nu_mult := AnalyticNumberTheory.Sieve.goldbachNu_isMultiplicative, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftedComplements_eq_candidate_image (N : ℕ) : {a ∈ jurkatRichertSourceUnsiftedComplements N | (jurkatRichertSourceSiftingProduct N).Coprime a} = Finset.image (fun (p : ℕ) => N - p) (jurkatRichertSourceCandidates N)

The source support survives the remaining odd-prime sieve exactly when its prime partner belongs to Chen's literal carrier.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceBoundingSieve_siftedSum_eq_card (N : ℕ) : BoundingSieve.siftedSum = ↑(jurkatRichertSourceCandidates N).card

Exact finite identification of the source BoundingSieve with P_N(N, N^(1/10)). The range is p ≤ N; hence both p = 2 and the unit complement N - p = 1 are retained exactly when the literal source admits them.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSieveProduct_eq_goldbachSieveProduct (N : ℕ) (hEven : Even N) : AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (jurkatRichertSourceBoundingSieve N) = MertensTheorem.goldbachSieveProduct N (jurkatRichertSourceZ N)

For even N, the source sieve product is the standard Goldbach product at the literal real cutoff. Equation (25), not equation (26), supplies the Mertens normalization of this product.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMultiples_card_eq_primeSupport (N d : ℕ) : {a ∈ jurkatRichertSourceUnsiftedComplements N | d ∣ a}.card = {p ∈ jurkatRichertSourceUnsiftedPrimeSupport N | d ∣ N - p}.card

Multiples in the source complement support are counted by their unique prime partners.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMultSum_eq_modEq_count (N d : ℕ) (hEven : Even N) (hN : 2 < N) : BoundingSieve.multSum d = ↑{p ∈ jurkatRichertSourceUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card

On even N > 2, the source sieve multSum is exactly the Goldbach arithmetic-progression count p ≡ N (mod d). The p ≤ N endpoint causes no exception because such an N is not prime.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceRem_eq_modEq_count (N d : ℕ) (hEven : Even N) (hN : 2 < N) : BoundingSieve.rem d = ↑{p ∈ jurkatRichertSourceUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card - AnalyticNumberTheory.Sieve.goldbachNu d * LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) ↑N

The source sieve remainder is the exact Goldbach AP discrepancy.

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

The level-restricted Goldbach remainder sum used by the source lower sieve. Only squarefree divisors of the odd cutoff product with d ≤ N^(1/2-ε) occur.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceRemainderSum N ε = ∑ d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct N).divisors with ↑d ≤ ↑N ^ (1 / 2 - ε), |BoundingSieve.rem d|

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceRemainderSum_eq_AP (N : ℕ) (ε : ℝ) (hEven : Even N) (hN : 2 < N) : jurkatRichertSourceRemainderSum N ε = ∑ d ∈ (jurkatRichertSourceSiftingProduct N).divisors with ↑d ≤ ↑N ^ (1 / 2 - ε), |↑{p ∈ jurkatRichertSourceUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card - AnalyticNumberTheory.Sieve.goldbachNu d * LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) ↑N|

The level-restricted remainder is literally a sum of Goldbach AP discrepancies.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct_coprime_N (N : ℕ) : (jurkatRichertSourceSiftingProduct N).Coprime N

Every source modulus is coprime to the Goldbach integer: the source product omits precisely the cutoff primes dividing N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSource_goldbachNu_eq_inv_totient {N d : ℕ} (hd : d ∣ jurkatRichertSourceSiftingProduct N) : AnalyticNumberTheory.Sieve.goldbachNu d = 1 / ↑d.totient

On the squarefree source-divisor carrier the Goldbach local density is exactly the reduced-residue density 1 / φ(d).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSource_mod_coprime {N d : ℕ} (hd : d ∣ jurkatRichertSourceSiftingProduct N) : (N % d).Coprime d

The residue N mod d is a canonical reduced residue for every source modulus, including the canonical residue 0 at d = 1.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceExceptionalPrimes (N : ℕ) : Finset ℕ

The finitely many prime partners removed before sifting: they are exactly the odd cutoff primes already dividing N.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceExceptionalPrimes N = {r ∈ Finset.range (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceZ N) | Nat.Prime r ∧ 2 < r ∧ r ∣ N}

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSource_full_not_support_subset_exceptional (N : ℕ) : Finset.filter Nat.Prime (Finset.range (N + 1)) \ jurkatRichertSourceUnsiftedPrimeSupport N ⊆ jurkatRichertSourceExceptionalPrimes N

Outside the source support, a standard prime can only be one of the exceptional cutoff primes dividing N. This is the finite correction that must be retained when comparing the source AP count to standard primes.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSource_AP_correction_le_exceptional (N d : ℕ) : ↑{p ∈ Finset.range (N + 1) | Nat.Prime p ∧ p ≡ N [MOD d]}.card - ↑{p ∈ jurkatRichertSourceUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card ≤ ↑(jurkatRichertSourceExceptionalPrimes N).card

Removing the exceptional source fibres changes every Goldbach AP count by at most the total number of exceptional cutoff primes.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_jurkatRichertSource_AP_sub_trueLi_div_totient_le (N d : ℕ) : |↑{p ∈ jurkatRichertSourceUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card - BombieriVinogradov.trueLogarithmicIntegral ↑N / ↑d.totient| ≤ |BombieriVinogradov.standardPrimeAPError N d (N % d)| + ↑(jurkatRichertSourceExceptionalPrimes N).card

The source AP discrepancy is bounded by the standard reduced-residue discrepancy plus the honest exceptional-fibre correction.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_jurkatRichertSource_rem_le_standardError_add_exceptional (N d : ℕ) (hEven : Even N) (hN : 2 < N) (hd : d ∣ jurkatRichertSourceSiftingProduct N) : |BoundingSieve.rem d| ≤ |BombieriVinogradov.standardPrimeAPError N d (N % d)| + ↑(jurkatRichertSourceExceptionalPrimes N).card

The exact source sieve remainder is controlled by the standard prime-AP error plus the retained exceptional-fibre correction.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceRemainderSum_le_standardMax_add_exceptional (N : ℕ) (ε : ℝ) (hEven : Even N) (hN : 2 < N) : jurkatRichertSourceRemainderSum N ε ≤ ∑ d ∈ (jurkatRichertSourceSiftingProduct N).divisors with ↑d ≤ ↑N ^ (1 / 2 - ε), BombieriVinogradov.standardPrimeAPMaxError N d + ↑{d ∈ (jurkatRichertSourceSiftingProduct N).divisors | ↑d ≤ ↑N ^ (1 / 2 - ε)}.card * ↑(jurkatRichertSourceExceptionalPrimes N).card

Before any asymptotics, the source remainder sum splits into the standard BV maximum on its divisor carrier and the explicit exceptional-fibre endpoint term.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceExceptionalPrimes_card_le_log (N : ℕ) (hN : 2 ≤ N) : ↑(jurkatRichertSourceExceptionalPrimes N).card ≤ Real.log ↑N / Real.log 2

Exceptional source primes are distinct prime divisors of N, so their cardinality is bounded by the elementary ω(N) logarithmic bound.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSource_remainderCarrier_card_le (N : ℕ) (ε : ℝ) : {d ∈ (jurkatRichertSourceSiftingProduct N).divisors | ↑d ≤ ↑N ^ (1 / 2 - ε)}.card ≤ ⌊↑N ^ (1 / 2 - ε)⌋₊ + 1

The level-restricted source divisor carrier has no more elements than its real cutoff interval.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSource_exceptional_endpoint_le (N : ℕ) (ε : ℝ) (hN : 2 ≤ N) (_hε : 0 < ε) (hεHalf : ε < 1 / 2) : ↑{d ∈ (jurkatRichertSourceSiftingProduct N).divisors | ↑d ≤ ↑N ^ (1 / 2 - ε)}.card * ↑(jurkatRichertSourceExceptionalPrimes N).card ≤ 2 * ↑N ^ (1 / 2 - ε) * Real.log ↑N / Real.log 2

The correction in the finite source-to-standard comparison has the power-saving majorant 2 N^(1/2-ε) log N / log 2.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.Internal.eventually_jurkatRichertSource_exceptional_endpoint_small (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) : ∀ᶠ (N : ℕ) in Filter.atTop, 2 * ↑N ^ (1 / 2 - ε) * Real.log ↑N / Real.log 2 ≤ δ * SingularSeries.liuUniversalProduct * ↑N / Real.log ↑N ^ 2

The exceptional-fibre majorant is genuinely power-saving relative to the Goldbach N / log² N scale.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimeCount (N p : ℕ) : ℕ

The literal medium-prime divisor count in Chen's Lemma 9: N^(1/10) < q ≤ N^(1/3). Divisors are distinct because this is a cardinality, not a valuation sum.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimeCount N p = {q ∈ Finset.range (N + 1) | Nat.Prime q ∧ ↑N ^ (1 / 10) < ↑q ∧ ↑q ≤ ↑N ^ (1 / 3) ∧ q ∣ N - p}.card

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes (N : ℕ) : Finset ℕ

The literal medium-prime range N^(1/10) < q ≤ N^(1/3) from Chen's Lemma 9.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes N = {q ∈ Finset.range (N + 1) | Nat.Prime q ∧ ↑N ^ (1 / 10) < ↑q ∧ ↑q ≤ ↑N ^ (1 / 3)}

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes_eq_Ioc_rpowFloor {N : ℕ} (hN : 1 ≤ N) : jurkatRichertSourceMediumPrimes N = Finset.filter Nat.Prime (Finset.Ioc (MertensTheorem.rpowFloor N (1 / 10)) (MertensTheorem.rpowFloor N (1 / 3)))

The real inequalities in the source range are represented exactly by floored half-open power cutoffs.

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

Chen's exact finite Lemma 9 producer P_N(N,z) - (1/2) * Σ_{z<q≤y} P_N(N,q,z), expanded as a sum over candidates.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceWeightedCount N = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceCandidates N, (1 - ↑(MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimeCount N p) / 2)

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

Chen's displayed q-outer sum of conditioned source counts in equation (26).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimeAggregate N = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimes N, ↑{p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceCandidates N | q ∣ N - p}.card

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditionedSupport (N q : ℕ) : Finset ℕ

The unsifted Goldbach-complement carrier conditioned by q ∣ N - p. No coprimality assumption between q and N is imposed here.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditionedSupport N q = {a ∈ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUnsiftedComplements N | q ∣ a}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditionedBoundingSieve (N q : ℕ) : BoundingSieve

Chen's finite P_N(N,q,z) sieve. Its main mass retains the local 1 / (q - 1) factor, while its remainder is the exact discrepancy of the conditioned finite carrier.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditionedBoundingSieve N q = { support := MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditionedSupport N q, prodPrimes := MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceSiftingProduct N, prodPrimes_squarefree := ⋯, weights := fun (x : ℕ) => 1, weights_nonneg := MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceBoundingSieve._proof_1, totalMass := MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) ↑N / (↑q - 1), nu := AnalyticNumberTheory.Sieve.goldbachNu, nu_mult := AnalyticNumberTheory.Sieve.goldbachNu_isMultiplicative, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditionedBoundingSieve_siftedSum_eq_card (N q : ℕ) : BoundingSieve.siftedSum = ↑{p ∈ jurkatRichertSourceCandidates N | q ∣ N - p}.card

Exact finite identification of the conditioned sieve with P_N(N,q,N^(1/10)). In particular, the exceptional lane q ∣ N has not been discarded or replaced by a reduced-residue approximation.

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

The integer level corresponding exactly to the varying real level N^(1/2-epsilon) / q.

Equations

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

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

The logarithmic ratio for the upper sieve at the varying level N^(1/2-epsilon) / q and sifting threshold N^(1/10).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperSieveRatio N q ε = Real.log (↑N ^ (1 / 2 - ε) / ↑q) / Real.log (↑N ^ (1 / 10))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperSieveRatio_zero {N q : ℕ} (hN : 1 < N) (hq : 0 < q) : jurkatRichertSourceUpperSieveRatio N q 0 = 5 - 10 * (Real.log ↑q / Real.log ↑N)

At zero level loss, the varying sieve ratio is exactly affine in the logarithmic prime coordinate.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperSieveRatio_eq_zero_sub {N q : ℕ} (hN : 1 < N) (hq : 0 < q) (ε : ℝ) : jurkatRichertSourceUpperSieveRatio N q ε = jurkatRichertSourceUpperSieveRatio N q 0 - 10 * ε

An epsilon loss in the level lowers every sieve ratio by exactly 10 * epsilon.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrime_log_mem {N q : ℕ} (hN : 1 < N) (hq : q ∈ jurkatRichertSourceMediumPrimes N) : Real.log ↑q / Real.log ↑N ∈ Set.Icc (1 / 10) (1 / 3)

Every source medium prime has logarithmic coordinate in the exact interval [1/10, 1/3].

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

The dimension-one upper linear-sieve factor on the range used in Chen's q-sum. The integral branch is the one whose partial summation contributes K / 2.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s = if s ≤ 3 then 2 * Real.exp Real.eulerMascheroniConstant / s else 2 * Real.exp Real.eulerMascheroniConstant / s * (1 + MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral s)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor_zeroEpsilon_continuousOn : ContinuousOn (fun (a : ℝ) => jurkatRichertUpperLinearSieveFactor (5 - 10 * a)) (Set.Icc (1 / 10) (1 / 3))

The zero-epsilon Jurkat--Richert weight is continuous on the medium-prime exponent interval.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor_zeroEpsilon_nonneg {a : ℝ} (ha : a ∈ Set.Icc (1 / 10) (1 / 3)) : 0 ≤ jurkatRichertUpperLinearSieveFactor (5 - 10 * a)

The zero-epsilon Jurkat--Richert weight is nonnegative on the medium-prime exponent interval.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor_perturbation {ε a : ℝ} (hε0 : 0 < ε) (hε : ε < 1 / 60) (ha : a ∈ Set.Icc (1 / 10) (1 / 3)) : jurkatRichertUpperLinearSieveFactor (5 - 10 * ε - 10 * a) ≤ 1 / (1 - 6 * ε) * jurkatRichertUpperLinearSieveFactor (5 - 10 * a)

Moving the sieve argument by 10 * ε costs at most the uniform factor (1 - 6 * ε)⁻¹ throughout the medium-prime exponent interval.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor_zeroEpsilon_integral : ∫ (a : ℝ) in 1 / 10..1 / 3, jurkatRichertUpperLinearSieveFactor (5 - 10 * a) / a = 2 * Real.exp Real.eulerMascheroniConstant / 5 * (Real.log 8 + jurkatRichertK / 2)

Exact zero-epsilon weighted integral used in the varying-q prime sum.