The Jurkat--Richert 1965 gamma(p) = 1, q = 1 specialization

This file begins the literal finite specialization of Jurkat--Richert (1965), with local density exactly 1 / p. The companion ChenTheoremFive module proves its complete two-sided Theorem 5. The separate ChenRichertConsumer module connects the actual Goldbach density 1 / (p - 1) through constructed delay majorants and modern sieve comparisons, not by identifying the densities.

The literal Buchstab and Euler identities (2.2) and (2.3) are proved below. The concrete count is then expanded to every positive finite depth along explicit chains pᵢ < ... < p₁, in the nested recursive form used by the paper's induction, and then flattened into the four displayed finite sums of formula (2.1). The finite Rosser identities instantiate existing adapted coefficient machinery at 1 / p; no identification with the concrete count expansion is asserted. The algebraic comparison and terminal lemmas isolate two further finite steps needed by the source proof.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.localDensity (p : ℕ) : ℝ

The literal local density gamma(p) / p when gamma(p) = 1.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.localDensity p = 1 / ↑p

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.one_sub_localDensity_ne_zero {p : ℕ} (hp : Nat.Prime p) : 1 - localDensity p ≠ 0

The local Euler factor is nonzero at every prime.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.localDensity_div_one_sub {p : ℕ} (hp : Nat.Prime p) : localDensity p / (1 - localDensity p) = 1 / (↑p - 1)

After Euler normalization, a selected prime contributes 1 / (p - 1).

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes (k : ℕ) (z : ℝ) : Finset ℕ

The finite prime carrier p < z, p ∤ k from the 1965 paper.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes k z = {p ∈ Finset.range ⌈z⌉₊ | Nat.Prime p ∧ ↑p < z ∧ ¬p ∣ k}

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.mem_siftingPrimes {k p : ℕ} {z : ℝ} : p ∈ siftingPrimes k z ↔ Nat.Prime p ∧ ↑p < z ∧ ¬p ∣ k

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes_one_eq_primesBelow {z : ℝ} : siftingPrimes 1 z = ⌈z⌉₊.primesBelow

At k = 1, the source's strict real cutoff is exactly Mathlib's natural prime cutoff at ceil z.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.excludedSiftingPrimes (k : ℕ) (z : ℝ) : Finset ℕ

The selected primes below z omitted only because they divide k.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.excludedSiftingPrimes k z = {p ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes 1 z | p ∣ k}

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.excludedSiftingFactor (k : ℕ) (z : ℝ) : ℕ

The squarefree product of the primes omitted from P_k(z).

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.excludedSiftingFactor k z = (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.excludedSiftingPrimes k z).prod id

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes_union_excluded (k : ℕ) (z : ℝ) : siftingPrimes k z ∪ excludedSiftingPrimes k z = siftingPrimes 1 z

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.excludedSiftingFactor_dvd_siftingPrimes_one (k : ℕ) (z : ℝ) : excludedSiftingFactor k z ∣ (siftingPrimes 1 z).prod id

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.excludedSiftingFactor_primeFactors (k : ℕ) (z : ℝ) : (excludedSiftingFactor k z).primeFactors = excludedSiftingPrimes k z

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct (k : ℕ) (z : ℝ) : ℝ

The paper's finite Euler product R_k(z).

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct k z = ∏ p ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes k z, (1 - MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.localDensity p)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct_pos (k : ℕ) (z : ℝ) : 0 < sieveProduct k z

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct_one_eq_mertensPrimeProduct (z : ℝ) : sieveProduct 1 z = AnalyticNumberTheory.Mertens.primeProduct (⌈z⌉₊ - 1)

The literal product over primes p < z is the standard finite Mertens product through ceil z - 1; this records the strict real cutoff exactly.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.exists_sieveProduct_one_mertens_bound : ∃ C > 0, ∀ (z : ℝ), 2 ≤ ⌈z⌉₊ - 1 → |sieveProduct 1 z - Real.exp (-Real.eulerMascheroniConstant) / Real.log ↑(⌈z⌉₊ - 1)| ≤ C / Real.log ↑(⌈z⌉₊ - 1) ^ 2

Mertens' product theorem with the paper's literal strict real cutoff. The proof of (3.9) below transports log (ceil z - 1) to log z.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.exists_sieveProduct_one_inv_le_log_div_add : ∃ B > 0, ∀ (z : ℝ), 1 < z → (sieveProduct 1 z)⁻¹ ≤ Real.log z / Real.exp (-Real.eulerMascheroniConstant) + B

Uniform reciprocal Mertens bound at the paper's strict real cutoff. The leading coefficient is exactly exp EulerGamma; the finite initial range is absorbed into one additive constant rather than checked by a finite scan.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.exists_sieveProduct_one_inv_le_exp_mul_log_add : ∃ B > 0, ∀ (z : ℝ), 1 < z → (sieveProduct 1 z)⁻¹ ≤ Real.exp Real.eulerMascheroniConstant * Real.log z + B

The preceding strict-cutoff inversion with its leading coefficient in the paper's displayed exp EulerGamma normalization.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct_eq_one_sub_sum (k : ℕ) (z : ℝ) : sieveProduct k z = 1 - ∑ p ∈ siftingPrimes k z, localDensity p * sieveProduct k ↑p

The literal finite Euler identity (2.3): R_k(z) = 1 - sum_{p < z, p ∤ k} R_k(p) / p.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCount (M : Finset ℕ) (k : ℕ) (z : ℝ) : ℝ

The paper's sifted cardinality A_k(M; z).

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCount M k z = ↑{n ∈ M | ((MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes k z).prod id).Coprime n}.card

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCountOn (M P : Finset ℕ) : ℝ

The same sifted cardinality with an explicit finite prime carrier.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCountOn M P = ↑{n ∈ M | (P.prod id).Coprime n}.card

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.conditionedSiftedCountOn (M P : Finset ℕ) (p : ℕ) : ℝ

The divisibility-fiber realization of the paper's conditioned count A_k(M_p; p): p divides the original element, and no selected prime below p divides it.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.conditionedSiftedCountOn M P p = ↑{n ∈ M | p ∣ n ∧ ({q ∈ P | q < p}.prod id).Coprime n}.card

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCountOn_eq_card_sub_conditioned_sum (M P : Finset ℕ) (hprime : ∀ p ∈ P, Nat.Prime p) : siftedCountOn M P = ↑M.card - ∑ p ∈ P, conditionedSiftedCountOn M P p

Finite Buchstab partition over an arbitrary finite prime carrier. Every non-sifted element is assigned to its least selected prime divisor.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCount_eq_card_sub_conditioned_sum (M : Finset ℕ) (k : ℕ) (z : ℝ) : siftedCount M k z = ↑M.card - ∑ p ∈ siftingPrimes k z, conditionedSiftedCountOn M (siftingPrimes k z) p

The literal finite Buchstab identity (2.2) for the paper's carrier p < z, p ∤ k.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCount_eq_siftedCount_sub_interval (M : Finset ℕ) (k : ℕ) {z₁ z : ℝ} (hz : z₁ ≤ z) : siftedCount M k z = siftedCount M k z₁ - ∑ p ∈ siftingPrimes k z with z₁ ≤ ↑p, conditionedSiftedCountOn M (siftingPrimes k z) p

Subtracting (2.2) at two cutoffs leaves exactly the conditioned primes in the interval z₁ ≤ p < z. This is the unsplit identity used to begin formula (2.4).

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorPrimes (k : ℕ) (z₁ z y : ℝ) : Finset ℕ

The first, recursively expandable prime range in the depth-one instance of Theorem 1.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorPrimes k z₁ z y = {p ∈ {p ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes k z | z₁ ≤ ↑p} | ↑p < √(y / ↑p)}

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryPrimes (k : ℕ) (z₁ z y : ℝ) : Finset ℕ

The terminal boundary-prime range in the depth-one instance of Theorem 1.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryPrimes k z₁ z y = {p ∈ {p ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes k z | z₁ ≤ ↑p} | √(y / ↑p) ≤ ↑p ∧ ↑p < y / ↑p}

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCount_theoremOne_depthOne (M : Finset ℕ) (k : ℕ) {z₁ z y : ℝ} (hz₁ : 2 ≤ z₁) (hz : z₁ ≤ z) (hzy : z ≤ √y) : siftedCount M k z = siftedCount M k z₁ - ∑ p ∈ theoremOneInteriorPrimes k z₁ z y, conditionedSiftedCountOn M (siftingPrimes k z) p - ∑ p ∈ theoremOneBoundaryPrimes k z₁ z y, conditionedSiftedCountOn M (siftingPrimes k z) p

Formula (2.4), equivalently the depth-one case of Theorem 1. The conditioned primes are split at sqrt (y / p), and the upper boundary p < y / p follows from p < z ≤ sqrt y.

def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.conditionedCarrier (M : Finset ℕ) : List ℕ → Finset ℕ

The original-source divisibility fiber for successive chain primes. Chains are stored least/newest prime first, so [pᵢ, ..., p₁] displays the source order pᵢ < ... < p₁.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.conditionedCarrier M [] = M
• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.conditionedCarrier M (p :: ps) = {n ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.conditionedCarrier M ps | p ∣ n}

def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale (y : ℝ) : List ℕ → ℝ

The successive source scale: for [pᵢ, ..., p₁] this is y / (p₁ ... pᵢ).

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale y [] = y
• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale y (p :: ps) = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale y ps / ↑p

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainSiftedCount (M : Finset ℕ) (k : ℕ) (ps : List ℕ) (u : ℝ) : ℝ

The divisibility-fiber realization of A_k(M_{p₁...pᵢ}; u) attached to a prime chain.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainSiftedCount M k ps u = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCount (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.conditionedCarrier M ps) k u

def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorChain (k : ℕ) (z₁ z y : ℝ) : List ℕ → Prop

An explicit interior chain from Theorem 1. For the list [pᵢ, ..., p₁], every prime lies in [z₁, z), the entries satisfy pᵢ < ... < p₁, and each pⱼ < sqrt (yⱼ).

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorChain k z₁ z y [] = True
• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorChain k z₁ z y (p :: ps) = (Nat.Prime p ∧ z₁ ≤ ↑p ∧ ↑p < z ∧ ¬p ∣ k ∧ (∀ q ∈ ps, p < q) ∧ ↑p < √(MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale y (p :: ps)) ∧ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorChain k z₁ z y ps)

def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryChain (k : ℕ) (z₁ z y : ℝ) : List ℕ → Prop

An explicit boundary chain from Theorem 1. Its least/newest prime pᵢ satisfies sqrt (yᵢ) ≤ pᵢ < yᵢ; all preceding primes satisfy the interior constraints.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryChain k z₁ z y [] = False
• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryChain k z₁ z y (p :: ps) = (Nat.Prime p ∧ z₁ ≤ ↑p ∧ ↑p < z ∧ ¬p ∣ k ∧ (∀ q ∈ ps, p < q) ∧ √(MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale y (p :: ps)) ≤ ↑p ∧ ↑p < MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale y (p :: ps) ∧ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorChain k z₁ z y ps)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale_eq_div_prod (y : ℝ) (ps : List ℕ) : chainScale y ps = y / ↑ps.prod

The recursive scale is literally y / (p₁ ... pᵢ).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.prime_of_mem_theoremOneInteriorChain {k q : ℕ} {ps : List ℕ} {z₁ z y : ℝ} (hchain : theoremOneInteriorChain k z₁ z y ps) (hq : q ∈ ps) : Nat.Prime q

Every entry of an interior chain is prime.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.conditionedCarrier_eq_filter_prod_of_interiorChain (M : Finset ℕ) {k : ℕ} {ps : List ℕ} {z₁ z y : ℝ} (hchain : theoremOneInteriorChain k z₁ z y ps) : conditionedCarrier M ps = {n ∈ M | ps.prod ∣ n}

Along an interior chain, successive divisibility conditioning is exactly conditioning by the product p₁ ... pᵢ.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.conditionedSiftedCountOn_siftingPrimes_eq (M : Finset ℕ) (k : ℕ) {z : ℝ} {p : ℕ} (hp : p ∈ siftingPrimes k z) : conditionedSiftedCountOn M (siftingPrimes k z) p = siftedCount ({n ∈ M | p ∣ n}) k ↑p

On the paper's prime carrier, conditioning at p is exactly sifting the p-divisibility fibre at cutoff p.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorChain_cons_of_mem {k p q : ℕ} {ps : List ℕ} {z₁ z y : ℝ} (hchain : theoremOneInteriorChain k z₁ z y (p :: ps)) (hq : q ∈ theoremOneInteriorPrimes k z₁ (↑p) (chainScale y (p :: ps))) : theoremOneInteriorChain k z₁ z y (q :: p :: ps)

Appending an interior prime to an explicit interior chain preserves all of the paper's chain and square-root constraints.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryChain_cons_of_mem {k p q : ℕ} {ps : List ℕ} {z₁ z y : ℝ} (hchain : theoremOneInteriorChain k z₁ z y (p :: ps)) (hq : q ∈ theoremOneBoundaryPrimes k z₁ (↑p) (chainScale y (p :: ps))) : theoremOneBoundaryChain k z₁ z y (q :: p :: ps)

Appending a boundary prime to an explicit interior chain produces exactly the boundary condition sqrt (yᵢ) ≤ pᵢ < yᵢ.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainSiftedCount_eq_at_z₁_sub_extensions (M : Finset ℕ) (k p : ℕ) (ps : List ℕ) {z₁ z y : ℝ} (hz₁ : 2 ≤ z₁) (hchain : theoremOneInteriorChain k z₁ z y (p :: ps)) : chainSiftedCount M k (p :: ps) ↑p = chainSiftedCount M k (p :: ps) z₁ - ∑ q ∈ theoremOneInteriorPrimes k z₁ (↑p) (chainScale y (p :: ps)), chainSiftedCount M k (q :: p :: ps) ↑q - ∑ q ∈ theoremOneBoundaryPrimes k z₁ (↑p) (chainScale y (p :: ps)), chainSiftedCount M k (q :: p :: ps) ↑q

The exact induction step in the proof of Theorem 1. Starting from any nonempty interior chain [pᵢ, ..., p₁], it applies (2.4) to (M_{p₁...pᵢ}, yᵢ, pᵢ), producing the next interior and boundary chains.

def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainCutoff (z : ℝ) : List ℕ → ℝ

The current upper cutoff at a node of the Theorem 1 recursion.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainCutoff z [] = z
• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainCutoff z (p :: ps) = ↑p

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneRecursiveExpansion (M : Finset ℕ) (k : ℕ) (z₁ z y : ℝ) (ps : List ℕ) : ℕ → ℝ

The exact finite recursive expansion generated by the proof of Theorem 1. At positive depth it replaces every interior terminal count by (2.4); boundary counts are terminal and are not expanded.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneRecursiveExpansion M k z₁ z y ps 0 = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainSiftedCount M k ps (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainCutoff z ps)
• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneRecursiveExpansion M k z₁ z y ps r.succ = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainSiftedCount M k ps z₁ - ∑ q ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorPrimes k z₁ (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainCutoff z ps) (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale y ps), MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneRecursiveExpansion M k z₁ z y (q :: ps) r - ∑ q ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryPrimes k z₁ (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainCutoff z ps) (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale y ps), MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainSiftedCount M k (q :: ps) ↑q

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorChain_singleton_of_mem {k q : ℕ} {z₁ z y : ℝ} (hq : q ∈ theoremOneInteriorPrimes k z₁ z y) : theoremOneInteriorChain k z₁ z y [q]

A prime in the initial interior range is an explicit one-prime interior chain.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryChain_singleton_of_mem {k q : ℕ} {z₁ z y : ℝ} (hq : q ∈ theoremOneBoundaryPrimes k z₁ z y) : theoremOneBoundaryChain k z₁ z y [q]

A prime in the initial boundary range is an explicit one-prime boundary chain.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCount_eq_at_z₁_sub_chain_extensions (M : Finset ℕ) (k : ℕ) {z₁ z y : ℝ} (hz₁ : 2 ≤ z₁) (hz : z₁ ≤ z) (hzy : z ≤ √y) : siftedCount M k z = siftedCount M k z₁ - ∑ q ∈ theoremOneInteriorPrimes k z₁ z y, chainSiftedCount M k [q] ↑q - ∑ q ∈ theoremOneBoundaryPrimes k z₁ z y, chainSiftedCount M k [q] ↑q

Formula (2.4) with its conditioned terms written as the one-prime chains that seed the finite Theorem 1 recursion.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainSiftedCount_eq_recursiveExpansion (M : Finset ℕ) (k p : ℕ) (ps : List ℕ) {z₁ z y : ℝ} (hz₁ : 2 ≤ z₁) (hchain : theoremOneInteriorChain k z₁ z y (p :: ps)) (r : ℕ) : chainSiftedCount M k (p :: ps) ↑p = theoremOneRecursiveExpansion M k z₁ z y (p :: ps) r

Every explicit interior chain admits the exact recursive expansion at every finite depth. This is the arbitrary-depth induction statement before flattening the nested sums into the four alternating sums of (2.1).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCount_eq_theoremOneRecursiveExpansion (M : Finset ℕ) (k : ℕ) {z₁ z y : ℝ} (hz₁ : 2 ≤ z₁) (hz : z₁ ≤ z) (hzy : z ≤ √y) (r : ℕ) : siftedCount M k z = theoremOneRecursiveExpansion M k z₁ z y [] (r + 1)

The concrete count has the exact nested Theorem 1 expansion at every positive finite depth. The recursion ranges only over explicit chains pᵢ < ... < p₁, with all interior and boundary inequalities enforced by the prime carriers and preserved by the chain lemmas above.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorDepthSum (M : Finset ℕ) (k : ℕ) (z₁ z y : ℝ) (ps : List ℕ) (u : ℝ) : ℕ → ℝ

The sum over all interior extensions of ps by exactly i primes, evaluated at the common cutoff u. Its nested finite sums are the explicit prime-chain sum pᵢ < ... < p₁ in (2.1).

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorDepthSum M k z₁ z y ps u 0 = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainSiftedCount M k ps u
• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorDepthSum M k z₁ z y ps u r.succ = ∑ q ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorPrimes k z₁ (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainCutoff z ps) (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale y ps), MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorDepthSum M k z₁ z y (q :: ps) u r

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneTerminalDepthSum (M : Finset ℕ) (k : ℕ) (z₁ z y : ℝ) (ps : List ℕ) : ℕ → ℝ

The sum over the interior chains obtained from ps at exact depth i, with each terminal count evaluated at its newest prime.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneTerminalDepthSum M k z₁ z y ps 0 = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainSiftedCount M k ps (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainCutoff z ps)
• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneTerminalDepthSum M k z₁ z y ps r.succ = ∑ q ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorPrimes k z₁ (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainCutoff z ps) (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale y ps), MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneTerminalDepthSum M k z₁ z y (q :: ps) r

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryDepthSum (M : Finset ℕ) (k : ℕ) (z₁ z y : ℝ) (ps : List ℕ) : ℕ → ℝ

The sum over exact-depth boundary chains extending ps. The final prime is in the boundary range; all earlier primes are in the interior range.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryDepthSum M k z₁ z y ps 0 = 0
• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryDepthSum M k z₁ z y ps 1 = ∑ q ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryPrimes k z₁ (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainCutoff z ps) (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale y ps), MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainSiftedCount M k (q :: ps) ↑q
• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryDepthSum M k z₁ z y ps i.succ.succ = ∑ q ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorPrimes k z₁ (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainCutoff z ps) (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.chainScale y ps), MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryDepthSum M k z₁ z y (q :: ps) (i + 1)

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorCumulative (M : Finset ℕ) (k : ℕ) (z₁ z y : ℝ) (ps : List ℕ) (r : ℕ) : ℝ

The signed sum of the common-z₁ interior terms at depths 0,...,r-1.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorCumulative M k z₁ z y ps r = ∑ i ∈ Finset.range r, (-1) ^ i * MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorDepthSum M k z₁ z y ps z₁ i

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryCumulative (M : Finset ℕ) (k : ℕ) (z₁ z y : ℝ) (ps : List ℕ) (r : ℕ) : ℝ

The signed sum of boundary terms at depths 1,...,r.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryCumulative M k z₁ z y ps r = ∑ i ∈ Finset.range r, (-1) ^ (i + 1) * MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryDepthSum M k z₁ z y ps (i + 1)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneInteriorCumulative_succ (M : Finset ℕ) (k : ℕ) (z₁ z y : ℝ) (ps : List ℕ) (r : ℕ) : theoremOneInteriorCumulative M k z₁ z y ps (r + 1) = chainSiftedCount M k ps z₁ - ∑ q ∈ theoremOneInteriorPrimes k z₁ (chainCutoff z ps) (chainScale y ps), theoremOneInteriorCumulative M k z₁ z y (q :: ps) r

Pulling the first prime out of the signed interior-depth sum.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneBoundaryCumulative_succ (M : Finset ℕ) (k : ℕ) (z₁ z y : ℝ) (ps : List ℕ) (r : ℕ) : theoremOneBoundaryCumulative M k z₁ z y ps (r + 1) = -∑ q ∈ theoremOneBoundaryPrimes k z₁ (chainCutoff z ps) (chainScale y ps), chainSiftedCount M k (q :: ps) ↑q - ∑ q ∈ theoremOneInteriorPrimes k z₁ (chainCutoff z ps) (chainScale y ps), theoremOneBoundaryCumulative M k z₁ z y (q :: ps) r

Pulling the first prime out of the signed boundary-depth sum.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.theoremOneRecursiveExpansion_eq_alternatingDepthSums (M : Finset ℕ) (k : ℕ) (z₁ z y : ℝ) (ps : List ℕ) (r : ℕ) : theoremOneRecursiveExpansion M k z₁ z y ps r = theoremOneInteriorCumulative M k z₁ z y ps r + (-1) ^ r * theoremOneTerminalDepthSum M k z₁ z y ps r + theoremOneBoundaryCumulative M k z₁ z y ps r

The nested recursion is exactly the sum of its signed interior levels, its last interior level, and all boundary levels.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCount_eq_theoremOneFourSums (M : Finset ℕ) (k : ℕ) {z₁ z y : ℝ} (hz₁ : 2 ≤ z₁) (hz : z₁ ≤ z) (hzy : z ≤ √y) (r : ℕ) (hr : 0 < r) : siftedCount M k z = siftedCount M k z₁ + ∑ i ∈ Finset.range (r - 1), (-1) ^ (i + 1) * theoremOneInteriorDepthSum M k z₁ z y [] z₁ (i + 1) + (-1) ^ r * theoremOneTerminalDepthSum M k z₁ z y [] r + ∑ i ∈ Finset.range r, (-1) ^ (i + 1) * theoremOneBoundaryDepthSum M k z₁ z y [] (i + 1)

The four finite sums displayed in Jurkat--Richert formula (2.1).

The first term is A_k(M;z₁). The first sum has depths 1 ≤ i < r and common cutoff z₁; the next term is the exact depth-r interior sum with cutoff pᵣ; and the last sum has boundary depths 1 ≤ i ≤ r. In the two outer sums, i + 1 is the displayed one-based depth. The recursively defined inner sums range only over the explicit prime chains enforced by theoremOneInteriorPrimes and theoremOneBoundaryPrimes.

structure MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource : Type

A literal H_k(M) source: M consists of positive integers and every coprime divisor count differs from y / d by at most one.

• carrier : Finset ℕ
• zero_not_mem : 0 ∉ self.carrier
• k : ℕ
• k_pos : 0 < self.k
• y : ℝ
• one_lt_y : 1 < self.y
• regular (d : ℕ) : 0 < d → d.Coprime self.k → |↑{n ∈ self.carrier | d ∣ n}.card - self.y / ↑d| ≤ 1

def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.literalQuotientCarrier (M : Finset ℕ) (d : ℕ) : Finset ℕ

Jurkat--Richert's literal finite quotient set M_d = {m | m * d ∈ M}.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.literalQuotientCarrier M d = Finset.image (fun (n : ℕ) => n / d) ({n ∈ M | d ∣ n})

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.mem_literalQuotientCarrier (M : Finset ℕ) {d m : ℕ} (hd : 0 < d) : m ∈ literalQuotientCarrier M d ↔ m * d ∈ M

The quotient-set definition has the paper's literal membership condition when d is positive.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.literalQuotientCarrier_bijOn (M : Finset ℕ) {d : ℕ} (hd : 0 < d) : Set.BijOn (fun (n : ℕ) => n / d) ↑({n ∈ M | d ∣ n}) ↑(literalQuotientCarrier M d)

Division by d is the exact bijection from the original-element divisibility fibre to the literal quotient carrier.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.card_literalQuotientCarrier (M : Finset ℕ) {d : ℕ} (hd : 0 < d) : (literalQuotientCarrier M d).card = {n ∈ M | d ∣ n}.card

The literal quotient carrier and the original divisibility fibre have the same cardinality.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.card_filter_literalQuotientCarrier (M : Finset ℕ) {d e : ℕ} (hd : 0 < d) : {m ∈ literalQuotientCarrier M d | e ∣ m}.card = {n ∈ M | d * e ∣ n}.card

Divisibility by e in the literal quotient is divisibility by d * e in the original source.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.literalQuotient (source : RegularSource) (d : ℕ) (hd : 0 < d) (hdk : d.Coprime source.k) (hdy : ↑d < source.y) : RegularSource

A regular source remains regular after literal quotienting: its new scale is y / d, its excluded modulus is k * d, and regularity at e is inherited from the original divisor d * e.

Equations

• source.literalQuotient d hd hdk hdy = { carrier := MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.literalQuotientCarrier source.carrier d, zero_not_mem := ⋯, k := source.k * d, k_pos := ⋯, y := source.y / ↑d, one_lt_y := ⋯, regular := ⋯ }

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftedCount_literalQuotientCarrier_eq_divisibilityFiber (M : Finset ℕ) (k d : ℕ) (z : ℝ) (hd : 0 < d) (hz : ∀ (p : ℕ), Nat.Prime p → p ∣ d → z ≤ ↑p) : siftedCount (literalQuotientCarrier M d) (k * d) z = siftedCount ({n ∈ M | d ∣ n}) k z

Below every prime divisor of d, quotienting and adding d to the excluded modulus preserves the existing divisibility-fibre sifted count.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.prod_one_sub_localDensity_eq_totient_div_prod (s : Finset ℕ) (hs : ∀ p ∈ s, Nat.Prime p) : ∏ p ∈ s, (1 - localDensity p) = ↑(s.prod id).totient / ↑(s.prod id)

The Euler product over any finite prime carrier is its product's exact totient ratio.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.natReciprocalMonoidHom : ℕ →* ℝ

The completely multiplicative reciprocal used in the geometric Euler products behind Lemma 3.1 (3.3).

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.natReciprocalMonoidHom = { toFun := fun (n : ℕ) => (↑n)⁻¹, map_one' := MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.natReciprocalMonoidHom._proof_1, map_mul' := MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.natReciprocalMonoidHom._proof_2 }

@[simp]

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.natReciprocalMonoidHom_apply (n : ℕ) : natReciprocalMonoidHom n = 1 / ↑n

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.radicalQuotientEmbedding (q : ℕ) : { n : ℕ // 0 < n ∧ UniqueFactorizationMonoid.radical n = q } ↪ ↑(Nat.factoredNumbers q.primeFactors)

For a positive integer with squarefree kernel q, division by q injects its fiber into the positive integers factored over the primes of q. This is the source's grouping by the largest squarefree divisor.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.radicalQuotientEmbedding q = { toFun := fun (n : { n : ℕ // 0 < n ∧ UniqueFactorizationMonoid.radical n = q }) => have hqDiv := ⋯; ⟨↑n / q, ⋯⟩, inj' := ⋯ }

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sum_reciprocal_of_radical_eq_le {q : ℕ} (hq : Squarefree q) (s : Finset ℕ) (hsPos : ∀ n ∈ s, 0 < n) (hsRadical : ∀ n ∈ s, UniqueFactorizationMonoid.radical n = q) : ∑ n ∈ s, 1 / ↑n ≤ 1 / ↑q.totient

The geometric-series estimate for one squarefree-kernel fiber used in the proof of Lemma 3.1 (3.3).

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.boundingSieve (source : RegularSource) (z : ℝ) : BoundingSieve

The literal H_k(M) source as a BoundingSieve, with the exact local density ν(d) = 1 / d and the paper's finite prime carrier.

Equations

• source.boundingSieve z = { support := source.carrier, prodPrimes := (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes source.k z).prod id, prodPrimes_squarefree := ⋯, weights := fun (x : ℕ) => 1, weights_nonneg := MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.boundingSieve._proof_2, totalMass := source.y, nu := (↑ArithmeticFunction.zeta).pdiv ↑ArithmeticFunction.id, nu_mult := MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.boundingSieve._proof_3, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.boundingSieve_nu_apply (source : RegularSource) (z : ℝ) {d : ℕ} (hd : 0 < d) : (source.boundingSieve z).nu d = 1 / ↑d

The local density of the literal source sieve is exactly 1 / d away from d = 0.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.boundingSieve_siftedSum_eq (source : RegularSource) (z : ℝ) : BoundingSieve.siftedSum = siftedCount source.carrier source.k z

The sifted sum of the literal source BoundingSieve is the concrete cardinality A_k(M; z), not a coefficient-density surrogate.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.boundingSieve_sieveProduct_eq (source : RegularSource) (z : ℝ) : AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (source.boundingSieve z) = sieveProduct source.k z

The Euler product of the literal source BoundingSieve is exactly the paper's R_k(z).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.boundingSieve_selbergTerm_prime (source : RegularSource) (z : ℝ) {p : ℕ} (hp : Nat.Prime p) : BoundingSieve.selbergTerms p = 1 / (↑p - 1)

At one selected prime, the source Selberg denominator has the literal local factor 1 / (p - 1) occurring in S_k(xi, z).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.boundingSieve_selbergTerm_of_dvd (source : RegularSource) (z : ℝ) {d : ℕ} (hd : d ∣ (siftingPrimes source.k z).prod id) : BoundingSieve.selbergTerms d = 1 / ↑d.totient

On every divisor of the literal sifting product, the complete Selberg denominator term is exactly the reciprocal totient appearing in the paper's S_k(xi, z).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.coprime_of_dvd_siftingPrimes_prod {k d : ℕ} {z : ℝ} (hd : d ∣ (siftingPrimes k z).prod id) : d.Coprime k

Every divisor of the paper's sifting product is coprime to the excluded modulus k.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes_mul_eq_sdiff_primeFactors {k d : ℕ} {z : ℝ} (hd : d ∣ (siftingPrimes k z).prod id) : siftingPrimes (k * d) z = siftingPrimes k z \ d.primeFactors

If d divides the literal sifting product, adjoining d to the excluded modulus removes exactly the prime factors of d from the finite prime carrier.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes_excludedSiftingFactor (k : ℕ) (z : ℝ) : siftingPrimes (excludedSiftingFactor k z) z = siftingPrimes k z

Excluding the squarefree omitted-prime factor is the same as excluding the original modulus k from the prime carrier below z.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct_one_eq_mul_excludedFactor (k : ℕ) (z : ℝ) : sieveProduct 1 z = sieveProduct k z * (↑(excludedSiftingFactor k z).totient / ↑(excludedSiftingFactor k z))

The Euler ratio in Lemma 3.1 (3.2): restoring the primes omitted by k multiplies R_k(z) by phi(d) / d, where d is their squarefree product.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes_mul_prod_mul {k d : ℕ} {z : ℝ} (hd : d ∣ (siftingPrimes k z).prod id) : (siftingPrimes (k * d) z).prod id * d = (siftingPrimes k z).prod id

The preceding carrier identity gives the exact product factorization P_k(z) = P_(k*d)(z) * d used in the source's divisor reindexing.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.abs_boundingSieve_rem_le_one_of_dvd (source : RegularSource) (z : ℝ) {d : ℕ} (hd : d ∣ (siftingPrimes source.k z).prod id) : |BoundingSieve.rem d| ≤ 1

On every divisor of the actual sifting product, the BoundingSieve remainder is precisely controlled by the source hypothesis H_k(M).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.boundingSieve_errSum_le (source : RegularSource) (z : ℝ) (muPlus : ℕ → ℝ) : BoundingSieve.errSum muPlus ≤ ∑ d ∈ ((siftingPrimes source.k z).prod id).divisors, |muPlus d|

The complete Selberg error of the literal source is bounded only from the proved unit remainder |R_d| ≤ 1; no analytic source estimate is assumed.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.siftedCount_le_moebius_divisorError (source : RegularSource) (z : ℝ) : siftedCount source.carrier source.k z ≤ source.y * sieveProduct source.k z + ↑((siftingPrimes source.k z).prod id).divisors.card

The exact finite Möbius expansion from (1.1), used for the bounded-z branch of Theorem 3. Its error is bounded by the symbolic divisor count of the actual finite sifting product; no cutoff values are enumerated.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct_exp_two_le_of_log_le_two {k : ℕ} {z : ℝ} (hz : 0 < z) (hlog : Real.log z ≤ 2) : sieveProduct 1 (Real.exp 2) ≤ sieveProduct k z

Enlarging the real prime cutoff and restoring primes dividing k can only decrease the source Euler product.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.exists_siftedCount_le_moebius_bounded_log (b : ℝ) : ∃ D > 0, ∀ (source : RegularSource) {z : ℝ}, 0 < z → Real.log z ≤ b → siftedCount source.carrier source.k z ≤ source.y * sieveProduct source.k z + D

On the bounded-z lane, the divisor error in the exact finite Möbius expansion is bounded by one symbolic absolute constant.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.exists_siftedCount_le_moebius_boundedZ : ∃ D > 0, ∀ (source : RegularSource) {z : ℝ}, 0 < z → Real.log z ≤ 2 → siftedCount source.carrier source.k z ≤ source.y * sieveProduct source.k z + D

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.exists_siftedCount_le_selberg (source : RegularSource) (z : ℝ) : ∃ (w : ℕ → ℝ), w 1 = 1 ∧ siftedCount source.carrier source.k z ≤ source.y * (∑ l ∈ ((siftingPrimes source.k z).prod id).divisors, BoundingSieve.selbergTerms l)⁻¹ + ∑ d ∈ ((siftingPrimes source.k z).prod id).divisors, |BoundingSieve.lambdaSquared w d|

The unconditional finite Selberg upper bound specialized to the literal H_k(M) source. The explicit denominator and smooth-number estimates used for (3.9) and (4.2) are proved separately, without a generic-density premise.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.levelSelbergDenominator (source : RegularSource) (z : ℝ) (xi : ℕ) : ℝ

The independent finite level in the source's Selberg denominator. This is the literal finite S_k(xi, z) construction behind Theorem 2, before its reciprocal-totient and rough-number estimates are applied.

Equations

• source.levelSelbergDenominator z xi = MathlibNt.SieveTheory.LiuWeight.truncatedSelbergDenominator (source.boundingSieve z) xi

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergReciprocalTotientCarrier (k xi : ℕ) (z : ℝ) : Finset ℕ

The divisor carrier in the paper's finite sum S_k(xi, z).

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergReciprocalTotientCarrier k xi z = {d ∈ ((MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes k z).prod id).divisors | d ≤ xi}

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsiCarrier (xi : ℕ) (z : ℝ) : Finset ℕ

The source carrier counted by Psi(xi, z): positive integers at most xi whose greatest prime divisor is below z, with the printed convention that the greatest prime divisor of 1 is 1.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsiCarrier xi z = {n ∈ Finset.Icc 1 xi | (n = 1 → 1 < z) ∧ ∀ p ∈ n.primeFactors, ↑p < z}

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsi (xi : ℕ) (z : ℝ) : ℝ

The finite smooth-number quantity Psi(xi, z) in Theorem 2.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsi xi z = ↑(MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsiCarrier xi z).card

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergSmoothReciprocalSum (xi : ℕ) (z : ℝ) : ℝ

The reciprocal smooth-number sum denoted by T(x,z) in Lemma 3.1.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergSmoothReciprocalSum xi z = ∑ n ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsiCarrier xi z, 1 / ↑n

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergSmoothRpowSum (xi : ℕ) (z sigma : ℝ) : ℝ

The finite Rankin moment of the source's literal smooth-number carrier.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergSmoothRpowSum xi z sigma = ∑ n ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsiCarrier xi z, ↑n ^ (-sigma)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasSum_selbergSmoothReciprocal (z : ℝ) : HasSum (fun (m : ↑(Nat.factoredNumbers (siftingPrimes 1 z))) => 1 / ↑↑m) (sieveProduct 1 z)⁻¹

The exact Euler series identity in (4.4), before passing to the paper's finite truncations T(x,z).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasSum_selbergSmoothRpow (z sigma : ℝ) (hsigma : 0 < sigma) : HasSum (fun (m : ↑(Nat.factoredNumbers (siftingPrimes 1 z))) => ↑↑m ^ (-sigma)) (∏ p ∈ siftingPrimes 1 z, (1 - ↑p ^ (-sigma))⁻¹)

The exact Euler series for every positive Rankin exponent. This is the finite-prime product to be estimated in Vinogradov's argument, not an assumed smooth-number bound.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.mem_selbergPsiCarrier_iff_factoredNumbers {xi n : ℕ} {z : ℝ} (hz : 1 < z) : n ∈ selbergPsiCarrier xi z ↔ n ≤ xi ∧ n ∈ Nat.factoredNumbers (siftingPrimes 1 z)

For z > 1, the source's finite smooth carrier is exactly the bounded part of the finite-prime-factor subtype used by the Euler product.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsiCarrier_eq_smoothNumbersUpTo {xi : ℕ} {z : ℝ} (hz : 1 < z) : selbergPsiCarrier xi z = xi.smoothNumbersUpTo ⌈z⌉₊

The paper's literal finite Psi(xi,z) carrier is exactly Mathlib's finite smooth-number carrier, including the strict real cutoff through ceil z.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsiCarrier_mono {xi₁ xi₂ : ℕ} {z₁ z₂ : ℝ} (hxi : xi₁ ≤ xi₂) (hz : z₁ ≤ z₂) : selbergPsiCarrier xi₁ z₁ ⊆ selbergPsiCarrier xi₂ z₂

The literal smooth carrier is monotone jointly in both source cutoffs.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsi_mono {xi₁ xi₂ : ℕ} {z₁ z₂ : ℝ} (hxi : xi₁ ≤ xi₂) (hz : z₁ ≤ z₂) : selbergPsi xi₁ z₁ ≤ selbergPsi xi₂ z₂

Consequently the source's finite Psi count is jointly monotone.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsiCarrier_card_le_pow_primeCounting_mul_sqrt {xi : ℕ} {z : ℝ} (hz : 1 < z) : (selbergPsiCarrier xi z).card ≤ 2 ^ ⌈z⌉₊.primesBelow.card * xi.sqrt

The strongest smooth-number count currently available from Mathlib, transported to the exact source carrier. Its prime-counting factor is the remaining gap to Vinogradov's uniform estimate (4.3).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergSmoothReciprocalSum_eq_sum_range_indicator {xi : ℕ} {z : ℝ} (hz : 1 < z) : selbergSmoothReciprocalSum xi z = ∑ n ∈ Finset.range (xi + 1), (Nat.factoredNumbers (siftingPrimes 1 z)).indicator (fun (m : ℕ) => 1 / ↑m) n

The source's T(x,z) is the ordinary natural partial sum of the exact Euler series in (4.4).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergSmoothRpowSum_eq_sum_range_indicator {xi : ℕ} {z sigma : ℝ} (hz : 1 < z) : selbergSmoothRpowSum xi z sigma = ∑ n ∈ Finset.range (xi + 1), (Nat.factoredNumbers (siftingPrimes 1 z)).indicator (fun (m : ℕ) => ↑m ^ (-sigma)) n

The finite Rankin moment is the ordinary natural partial sum of its exact Euler series.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergSmoothRpowSum_le_eulerProduct {xi : ℕ} {z sigma : ℝ} (hz : 1 < z) (hsigma : 0 < sigma) : selbergSmoothRpowSum xi z sigma ≤ ∏ p ∈ siftingPrimes 1 z, (1 - ↑p ^ (-sigma))⁻¹

The literal finite Rankin moment is bounded by its finite-prime Euler product. This is the summation step in the proof of (4.3).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsi_le_rpow_mul_smoothRpowSum {xi : ℕ} {z sigma : ℝ} (hsigma : 0 ≤ sigma) : selbergPsi xi z ≤ ↑xi ^ sigma * selbergSmoothRpowSum xi z sigma

Rankin's inequality on the paper's actual finite smooth-number carrier.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsi_le_rpow_mul_eulerProduct {xi : ℕ} {z sigma : ℝ} (hz : 1 < z) (hsigma : 0 < sigma) : selbergPsi xi z ≤ ↑xi ^ sigma * ∏ p ∈ siftingPrimes 1 z, (1 - ↑p ^ (-sigma))⁻¹

The unconditional finite Rankin bound reducing Vinogradov's estimate (4.3) to a finite-prime Euler-product estimate.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.tendsto_selbergSmoothReciprocalSum (z : ℝ) (hz : 1 < z) : Filter.Tendsto (fun (xi : ℕ) => selbergSmoothReciprocalSum xi z) Filter.atTop (nhds (sieveProduct 1 z)⁻¹)

Formula (4.4): the source's finite reciprocal smooth sums converge exactly to the reciprocal finite Euler product.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.exists_selbergSmoothReciprocalSum_tail_lt {z epsilon : ℝ} (hz : 1 < z) (hepsilon : 0 < epsilon) : ∃ (X : ℕ), ∀ xi ≥ X, |selbergSmoothReciprocalSum xi z - (sieveProduct 1 z)⁻¹| < epsilon

Finite-tail form of (4.4). The source obtains a uniform rate from Vinogradov's (4.3); ChenTheoremThree instead proves the required normalized estimate without that historical input.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.radical_mem_selbergReciprocalTotientCarrier {xi n : ℕ} {z : ℝ} (hn : n ∈ selbergPsiCarrier xi z) : UniqueFactorizationMonoid.radical n ∈ selbergReciprocalTotientCarrier 1 xi z

The squarefree kernel of a smooth integer belongs to the divisor carrier of the paper's reciprocal-totient sum.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergReciprocalTotientCarrier_subset_psiCarrier {k xi : ℕ} {z : ℝ} (hz : 1 < z) : selbergReciprocalTotientCarrier k xi z ⊆ selbergPsiCarrier xi z

Every divisor retained in S_k(xi, z) is counted by the source's Psi(xi, z).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergReciprocalTotientCarrier_map_mul {k d xi : ℕ} {z : ℝ} (hd : d ∣ (siftingPrimes k z).prod id) : have mulD := { toFun := fun (m : ℕ) => d * m, inj' := ⋯ }; Finset.map mulD (selbergReciprocalTotientCarrier (k * d) (xi / d) z) = {e ∈ selbergReciprocalTotientCarrier k xi z | d ∣ e}

Multiplication by a retained divisor d bijects the source carrier for S_(k*d)(xi/d, z) with the retained multiples of d in S_k(xi, z).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sum_selbergReciprocalTotientCarrier_if_dvd {k d xi : ℕ} {z : ℝ} (hd : d ∣ (siftingPrimes k z).prod id) (f : ℕ → ℝ) : (∑ e ∈ selbergReciprocalTotientCarrier k xi z, if d ∣ e then f (e / d) else 0) = ∑ m ∈ selbergReciprocalTotientCarrier (k * d) (xi / d) z, f m

Sum form of the preceding bijection: retained multiples of d are reindexed by their unique quotient in the source carrier for k*d.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.moebius_mul_moebius_div_totient_of_dvd {k d xi e : ℕ} {z : ℝ} (hd : d ∣ (siftingPrimes k z).prod id) (he : e ∈ selbergReciprocalTotientCarrier k xi z) (hde : d ∣ e) : ↑(ArithmeticFunction.moebius (e / d)) * ↑(ArithmeticFunction.moebius e) * (1 / ↑e.totient) = ↑(ArithmeticFunction.moebius d) * (1 / ↑d.totient) * (1 / ↑(e / d).totient)

The Möbius factors in a retained multiple e = d*m collapse to mu(d), while the reciprocal totient splits multiplicatively. This is the termwise arithmetic identity in the paper's printed lambda_d.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergReciprocalTotientSum (k xi : ℕ) (z : ℝ) : ℝ

The paper's finite reciprocal-totient sum S_k(xi, z) = sum_{d <= xi, d | P_k(z)} 1 / phi(d).

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergReciprocalTotientSum k xi z = ∑ d ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergReciprocalTotientCarrier k xi z, 1 / ↑d.totient

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergSmoothReciprocalSum_le (xi : ℕ) (z : ℝ) : selbergSmoothReciprocalSum xi z ≤ selbergReciprocalTotientSum 1 xi z

Lemma 3.1 (3.3) at a natural cutoff: grouping smooth integers by their largest squarefree divisor gives T(x,z) ≤ S₁(x,z).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergReciprocalTotientSum_congr_siftingPrimes {k₁ k₂ xi : ℕ} {z : ℝ} (h : siftingPrimes k₁ z = siftingPrimes k₂ z) : selbergReciprocalTotientSum k₁ xi z = selbergReciprocalTotientSum k₂ xi z

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergReciprocalTotientSum_mono (k : ℕ) (z : ℝ) {xi₁ xi₂ : ℕ} (hxi : xi₁ ≤ xi₂) : selbergReciprocalTotientSum k xi₁ z ≤ selbergReciprocalTotientSum k xi₂ z

Increasing the truncation level only adds nonnegative reciprocal-totient terms.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.reciprocalTotientSum_coprime_mul_decomposition {P d xi : ℕ} (hcop : P.Coprime d) : ∑ n ∈ (P * d).divisors with n ≤ xi, 1 / ↑n.totient = ∑ t ∈ d.divisors, 1 / ↑t.totient * ∑ m ∈ P.divisors with m ≤ xi / t, 1 / ↑m.totient

A truncated reciprocal-totient divisor sum over a coprime product splits into disjoint packets indexed by the divisor from the second factor.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.reciprocalTotientArithmeticFunction : ArithmeticFunction ℝ

Reciprocal totient as an arithmetic function, used only to evaluate the finite divisor packet in Lemma 3.1.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.reciprocalTotientArithmeticFunction = { toFun := fun (n : ℕ) => 1 / ↑n.totient, map_zero' := MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.reciprocalTotientArithmeticFunction._proof_1 }

@[simp]

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.reciprocalTotientArithmeticFunction_apply (n : ℕ) : reciprocalTotientArithmeticFunction n = 1 / ↑n.totient

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.reciprocalTotientArithmeticFunction_isMultiplicative : reciprocalTotientArithmeticFunction.IsMultiplicative

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sum_reciprocalTotient_divisors_eq {d : ℕ} (hd : Squarefree d) : ∑ t ∈ d.divisors, 1 / ↑t.totient = ↑d / ↑d.totient

On a squarefree divisor packet, the total reciprocal-totient weight is exactly d / phi(d).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergReciprocalTotientSum_eq_divisorPackets {k d xi : ℕ} {z : ℝ} (hd : d ∣ (siftingPrimes k z).prod id) : selbergReciprocalTotientSum k xi z = ∑ t ∈ d.divisors, 1 / ↑t.totient * selbergReciprocalTotientSum (k * d) (xi / t) z

The exact divisor-packet decomposition (3.4) of Lemma 3.1. The packet indexed by t | d contains the unique divisor whose d-part is t.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.mul_selbergReciprocalTotientSum_le {k d xi : ℕ} {z : ℝ} (hd : d ∣ (siftingPrimes k z).prod id) : ↑d / ↑d.totient * selbergReciprocalTotientSum (k * d) (xi / d) z ≤ selbergReciprocalTotientSum k xi z

The natural-cutoff form of Lemma 3.1 (3.1). It follows from the exact packet decomposition (3.4), monotonicity in the cutoff, and the packet mass sum_{t | d} 1 / phi(t) = d / phi(d).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergReciprocalTotientSum_one_le_excludedFactor (k xi : ℕ) (z : ℝ) : selbergReciprocalTotientSum 1 xi z ≤ ↑(excludedSiftingFactor k z) / ↑(excludedSiftingFactor k z).totient * selbergReciprocalTotientSum k xi z

Formula (3.4) also gives the reverse comparison needed in (3.2): restoring every prime omitted by k costs at most the complete packet factor d / phi(d).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct_one_mul_selbergReciprocalTotientSum_le (k xi : ℕ) (z : ℝ) : sieveProduct 1 z * selbergReciprocalTotientSum 1 xi z ≤ sieveProduct k z * selbergReciprocalTotientSum k xi z

The natural-cutoff form of Lemma 3.1 (3.2).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct_one_mul_selbergSmoothReciprocalSum_le (k xi : ℕ) (z : ℝ) : sieveProduct 1 z * selbergSmoothReciprocalSum xi z ≤ sieveProduct k z * selbergReciprocalTotientSum k xi z

Combining (3.2) and (3.3) at a natural cutoff gives the normalized smooth-number comparison at the end of Lemma 3.1.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergMoebiusPacket_eq {k d xi : ℕ} {z : ℝ} (hd : d ∣ (siftingPrimes k z).prod id) : (∑ e ∈ selbergReciprocalTotientCarrier k xi z, if d ∣ e then ↑(ArithmeticFunction.moebius (e / d)) * ↑(ArithmeticFunction.moebius e) * (1 / ↑e.totient) else 0) = ↑(ArithmeticFunction.moebius d) * (1 / ↑d.totient) * selbergReciprocalTotientSum (k * d) (xi / d) z

The complete finite Möbius packet in the truncated optimizer is the reciprocal-totient sum for the conditioned modulus k*d.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.levelSelbergDenominator_eq_reciprocalTotientSum (source : RegularSource) (z : ℝ) (xi : ℕ) : source.levelSelbergDenominator z xi = selbergReciprocalTotientSum source.k xi z

The independently truncated Selberg denominator is literally the source sum S_k(xi, z).

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.levelSelbergWeight (source : RegularSource) (z : ℝ) (xi : ℕ) : ℕ → ℝ

The cutoff-supported Selberg weight attached to the literal regular source. Its support level xi is independent of the sifting cutoff z.

Equations

• source.levelSelbergWeight z xi = MathlibNt.SieveTheory.LiuWeight.truncatedSelbergOptimalLambda (source.boundingSieve z) xi

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.levelSelbergWeight_eq_printed (source : RegularSource) (z : ℝ) {xi d : ℕ} (hd : d ∣ (siftingPrimes source.k z).prod id) (hdxi : d ≤ xi) : source.levelSelbergWeight z xi d = ↑(ArithmeticFunction.moebius d) * ↑d / ↑d.totient * (selbergReciprocalTotientSum (source.k * d) (xi / d) z / selbergReciprocalTotientSum source.k xi z)

On its source support, the independently constructed optimizer is exactly the paper's printed coefficient mu(d) * d / phi(d) * S_(k*d)(xi/d,z) / S_k(xi,z).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.levelSelbergDenominator_pos (source : RegularSource) (z : ℝ) {xi : ℕ} (hxi : 1 ≤ xi) : 0 < source.levelSelbergDenominator z xi

The level denominator is positive as soon as the source cutoff contains the divisor 1.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.levelSelbergWeight_one (source : RegularSource) (z : ℝ) {xi : ℕ} (hxi : 1 ≤ xi) : source.levelSelbergWeight z xi 1 = 1

The source's finite level weight has the normalization lambda_1 = 1.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.levelSelbergWeight_support (source : RegularSource) (z : ℝ) {xi d : ℕ} (hd : source.levelSelbergWeight z xi d ≠ 0) : d ∣ (siftingPrimes source.k z).prod id ∧ d ≤ xi

Every nonzero source weight is a divisor of the actual sifting product and is supported at the independent level d ≤ xi.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.levelSelbergWeight_eq_zero_of_not_support (source : RegularSource) (z : ℝ) {xi d : ℕ} (hd : ¬(d ∣ (siftingPrimes source.k z).prod id ∧ d ≤ xi)) : source.levelSelbergWeight z xi d = 0

Off the literal divisor carrier or beyond xi, the source weight is identically zero.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.abs_levelSelbergWeight_le_one (source : RegularSource) (z : ℝ) {xi : ℕ} (hxi : 1 ≤ xi) (d : ℕ) : |source.levelSelbergWeight z xi d| ≤ 1

The source's explicit finite Selberg weight satisfies the classical coefficient bound |lambda_d| ≤ 1.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.sum_abs_levelSelbergWeight_le_psi (source : RegularSource) {z : ℝ} (hz : 1 < z) {xi : ℕ} (hxi : 1 ≤ xi) : ∑ d ∈ ((siftingPrimes source.k z).prod id).divisors, |source.levelSelbergWeight z xi d| ≤ selbergPsi xi z

The total absolute mass of the printed level weight is bounded by the source smooth-number count Psi(xi, z).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.levelSelbergLambdaSquared_mass_le_psi_sq (source : RegularSource) {z : ℝ} (hz : 1 < z) {xi : ℕ} (hxi : 1 ≤ xi) : ∑ d ∈ ((siftingPrimes source.k z).prod id).divisors, |BoundingSieve.lambdaSquared (source.levelSelbergWeight z xi) d| ≤ selbergPsi xi z ^ 2

The exact coefficient-mass estimate in the proof of Theorem 2: sum |Lambda^2(d)| <= Psi(xi, z)^2.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.levelSelbergLambdaSquared_support (source : RegularSource) (z : ℝ) {xi d : ℕ} (hd : BoundingSieve.lambdaSquared (source.levelSelbergWeight z xi) d ≠ 0) : d ∣ (siftingPrimes source.k z).prod id ∧ d ≤ xi ^ 2

Squaring the level-xi weight enlarges support only to xi^2, and the resulting modulus still divides the literal sifting product.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.siftedCount_le_levelSelberg (source : RegularSource) (z : ℝ) {xi : ℕ} (hxi : 1 ≤ xi) : siftedCount source.carrier source.k z ≤ source.y * (source.levelSelbergDenominator z xi)⁻¹ + ∑ d ∈ ((siftingPrimes source.k z).prod id).divisors, |BoundingSieve.lambdaSquared (source.levelSelbergWeight z xi) d|

The exact level-xi Selberg upper bound for the literal source. Unlike the full-divisor optimizer above, both the main denominator and the weight are cut off independently of z; no form of (3.9) or (4.2) is assumed.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.siftedCount_le_levelSelberg_psi (source : RegularSource) {z : ℝ} (hz : 1 < z) {xi : ℕ} (hxi : 1 ≤ xi) : siftedCount source.carrier source.k z ≤ source.y * (source.levelSelbergDenominator z xi)⁻¹ + selbergPsi xi z ^ 2

The source-faithful finite Selberg estimate before the analytic lower bound for S_k(xi, z): its error is exactly bounded by Psi(xi, z)^2.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealReciprocalTotientCarrier (k : ℕ) (xi z : ℝ) : Finset ℕ

The divisor carrier with the paper's real cutoff d <= xi.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealReciprocalTotientCarrier k xi z = {d ∈ ((MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes k z).prod id).divisors | ↑d ≤ xi}

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealReciprocalTotientSum (k : ℕ) (xi z : ℝ) : ℝ

The paper's reciprocal-totient sum at a real cutoff.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealReciprocalTotientSum k xi z = ∑ d ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealReciprocalTotientCarrier k xi z, 1 / ↑d.totient

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsiCarrier (xi z : ℝ) : Finset ℕ

The source's Psi(xi, z) carrier at a real cutoff.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsiCarrier xi z = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergPsiCarrier ⌊xi⌋₊ z

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsi (xi z : ℝ) : ℝ

The source's smooth-number count at a real cutoff.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsi xi z = ↑(MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsiCarrier xi z).card

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealSmoothReciprocalSum (xi z : ℝ) : ℝ

The source's reciprocal smooth-number sum T(xi,z) at a real cutoff.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealSmoothReciprocalSum xi z = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergSmoothReciprocalSum ⌊xi⌋₊ z

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealReciprocalTotientCarrier_eq_floor (k : ℕ) {xi z : ℝ} (hxi : 0 ≤ xi) : selbergRealReciprocalTotientCarrier k xi z = selbergReciprocalTotientCarrier k ⌊xi⌋₊ z

A nonnegative real cutoff selects exactly the divisors selected by its natural floor.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealReciprocalTotientSum_eq_floor (k : ℕ) {xi z : ℝ} (hxi : 0 ≤ xi) : selbergRealReciprocalTotientSum k xi z = selbergReciprocalTotientSum k ⌊xi⌋₊ z

Consequently the real-cutoff denominator is the proved natural-cutoff denominator at floor xi.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealSmoothReciprocalSum_le {xi z : ℝ} (hxi : 0 ≤ xi) : selbergRealSmoothReciprocalSum xi z ≤ selbergRealReciprocalTotientSum 1 xi z

Lemma 3.1 (3.3) at the paper's real cutoff.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealReciprocalTotientSum_eq_divisorPackets {k d : ℕ} {xi z : ℝ} (hxi : 0 ≤ xi) (hd : d ∣ (siftingPrimes k z).prod id) : selbergRealReciprocalTotientSum k xi z = ∑ t ∈ d.divisors, 1 / ↑t.totient * selbergRealReciprocalTotientSum (k * d) (xi / ↑t) z

The paper's real-cutoff divisor-packet identity (3.4).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.mul_selbergRealReciprocalTotientSum_le {k d : ℕ} {xi z : ℝ} (hxi : 0 ≤ xi) (hd : d ∣ (siftingPrimes k z).prod id) : ↑d / ↑d.totient * selbergRealReciprocalTotientSum (k * d) (xi / ↑d) z ≤ selbergRealReciprocalTotientSum k xi z

The source's real-cutoff Lemma 3.1 inequality (3.1).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct_one_mul_selbergRealReciprocalTotientSum_le (k : ℕ) {xi z : ℝ} (hxi : 0 ≤ xi) : sieveProduct 1 z * selbergRealReciprocalTotientSum 1 xi z ≤ sieveProduct k z * selbergRealReciprocalTotientSum k xi z

The source's real-cutoff Lemma 3.1 comparison (3.2).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct_one_mul_selbergRealSmoothReciprocalSum_le (k : ℕ) {xi z : ℝ} (hxi : 0 ≤ xi) : sieveProduct 1 z * selbergRealSmoothReciprocalSum xi z ≤ sieveProduct k z * selbergRealReciprocalTotientSum k xi z

The real-cutoff normalized smooth-number comparison obtained by combining Lemma 3.1 (3.2) and (3.3).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.mem_selbergRealPsiCarrier {n : ℕ} {xi z : ℝ} (hxi : 0 ≤ xi) : n ∈ selbergRealPsiCarrier xi z ↔ 1 ≤ n ∧ ↑n ≤ xi ∧ (n = 1 → 1 < z) ∧ ∀ p ∈ n.primeFactors, ↑p < z

Membership in the real Psi carrier has the literal source inequalities 1 <= n <= xi and greatest prime divisor below z.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsi_eq_floor (xi z : ℝ) : selbergRealPsi xi z = selbergPsi ⌊xi⌋₊ z

The real smooth-number count is exactly the natural count at floor xi.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergSmoothReciprocalSum_sub_eq_psi_div_add_integral {n m : ℕ} {z : ℝ} (hz : 1 < z) (hn : 1 ≤ n) (hnm : n ≤ m) : selbergSmoothReciprocalSum m z - selbergSmoothReciprocalSum n z = selbergPsi m z / ↑m - selbergPsi n z / ↑n + ∫ (t : ℝ) in Set.Ioc ↑n ↑m, selbergRealPsi t z / t ^ 2

The exact finite partial-summation identity used immediately after (4.4) in the source. Both endpoint terms are retained, and the step-function prefix inside the integral is the literal real Psi.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsi_le_rpow_mul_eulerProduct {xi z sigma : ℝ} (hxi : 0 ≤ xi) (hz : 1 < z) (hsigma : 0 < sigma) : selbergRealPsi xi z ≤ xi ^ sigma * ∏ p ∈ siftingPrimes 1 z, (1 - ↑p ^ (-sigma))⁻¹

The finite Rankin reduction at the source's literal real cutoff. This retains the full joint dependence on xi and z; estimating the displayed finite-prime product uniformly is the remaining content of (4.3).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergEulerProduct_le_exp_four_mul {z sigma : ℝ} (hsmall : ∀ p ∈ siftingPrimes 1 z, ↑p ^ (-sigma) ≤ 3 / 4) : ∏ p ∈ siftingPrimes 1 z, (1 - ↑p ^ (-sigma))⁻¹ ≤ Real.exp (4 * ∑ p ∈ siftingPrimes 1 z, ↑p ^ (-sigma))

A finite Euler product is controlled by its first logarithmic moment when all local terms are at most 3/4.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sum_inv_siftingPrimes_le_one_add_log {z : ℝ} (hz : 1 ≤ z) : ∑ p ∈ siftingPrimes 1 z, 1 / ↑p ≤ 1 + Real.log z

The reciprocal-prime mass on the literal sifting carrier is bounded by the ordinary harmonic integral estimate.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sum_siftingPrimes_rpow_one_sub_le {z delta : ℝ} (hz : 1 ≤ z) (hdelta : 0 ≤ delta) : ∑ p ∈ siftingPrimes 1 z, ↑p ^ (-(1 - delta)) ≤ z ^ delta * (1 + Real.log z)

Moving the Rankin exponent from 1 by delta costs at most z^delta on every prime in the literal sifting carrier.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.vinogradovRankinEulerProduct_le {z : ℝ} (hz : 1 ≤ z) (hlog : 2 ≤ Real.log z) : ∏ p ∈ siftingPrimes 1 z, (1 - ↑p ^ (-(1 - 1 / Real.log z)))⁻¹ ≤ Real.exp (4 * (z ^ (1 / Real.log z) * (1 + Real.log z)))

The finite-prime Euler-product estimate at the Vinogradov Rankin exponent sigma = 1 - 1 / log z. This is an unconditional finite estimate; no smooth-number asymptotic is used in its proof.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsi_le_vinogradovRankin {xi z : ℝ} (hxi : 0 ≤ xi) (hz : 1 ≤ z) (hlog : 2 ≤ Real.log z) : selbergRealPsi xi z ≤ xi ^ (1 - 1 / Real.log z) * Real.exp (4 * (z ^ (1 / Real.log z) * (1 + Real.log z)))

The literal real smooth-number count after inserting the Vinogradov Rankin exponent and the unconditional finite-prime product estimate.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsi_le_self {xi z : ℝ} (hxi : 0 ≤ xi) : selbergRealPsi xi z ≤ xi

The real smooth-number count never exceeds its ambient real cutoff.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsi_le_rankin_logSq {xi z : ℝ} (hxi : 1 ≤ xi) (hz : 1 ≤ z) (hlog : 2 ≤ Real.log z) : selbergRealPsi xi z ≤ Real.exp (24 * Real.exp 1) * (xi * Real.exp (-2 * Real.log xi / Real.log z ^ 2))

An unconditional logarithmic-square smooth-number estimate on the source's literal real-cutoff carrier, with an explicit absolute constant. This is the weaker Rankin consequence sufficient below; it is not the sharper printed Vinogradov estimate (4.3), whose denominator is log z.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsi_div_sq_le_rankin_logSq {t z : ℝ} (ht : 1 ≤ t) (hz : 1 ≤ z) (hlog : 2 ≤ Real.log z) : selbergRealPsi t z / t ^ 2 ≤ Real.exp (24 * Real.exp 1) * t ^ (-1 - 2 / Real.log z ^ 2)

Dividing the logarithmic-square Rankin estimate by the square from partial summation gives the power majorant used below.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.integral_selbergRealPsi_div_sq_le_rankin_logSq {n m : ℕ} {z : ℝ} (hn : 1 ≤ n) (hnm : n ≤ m) (hz : 1 ≤ z) (hlog : 2 ≤ Real.log z) : ∫ (t : ℝ) in Set.Ioc ↑n ↑m, selbergRealPsi t z / t ^ 2 ≤ Real.exp (24 * Real.exp 1) * ((↑m ^ (-2 / Real.log z ^ 2) - ↑n ^ (-2 / Real.log z ^ 2)) / (-2 / Real.log z ^ 2))

The finite Stieltjes correction after (4.4) is bounded by integrating the logarithmic-square Rankin majorant, with both endpoints present.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergSmoothReciprocalSum_sub_le_rankin_logSq {n m : ℕ} {z : ℝ} (hn : 1 ≤ n) (hnm : n ≤ m) (hz : 1 ≤ z) (hlog : 2 ≤ Real.log z) : selbergSmoothReciprocalSum m z - selbergSmoothReciprocalSum n z ≤ 2 * Real.exp (24 * Real.exp 1) * Real.log z ^ 2 * ↑n ^ (-2 / Real.log z ^ 2)

The finite quantitative form of the partial-summation tail. The upper endpoint from the exact identity is estimated rather than discarded.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct_inv_sub_selbergSmoothReciprocalSum_le_rankin_logSq {n : ℕ} {z : ℝ} (hn : 1 ≤ n) (hz : 1 ≤ z) (hlog : 2 ≤ Real.log z) : 0 ≤ (sieveProduct 1 z)⁻¹ - selbergSmoothReciprocalSum n z ∧ (sieveProduct 1 z)⁻¹ - selbergSmoothReciprocalSum n z ≤ 2 * Real.exp (24 * Real.exp 1) * Real.log z ^ 2 * Real.exp (-2 * Real.log ↑n / Real.log z ^ 2)

The uniform reciprocal smooth-number tail deduced after (4.4). This is the source-scale O(log(z)^2 exp(-2 log(n)/log(z)^2)) estimate, obtained from the finite identity before passing to the Euler-product limit.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct_inv_sub_selbergSmoothReciprocalSum_le_rankin {n : ℕ} {z : ℝ} (hn : 1 ≤ n) (hz : 1 ≤ z) (hlog : 2 ≤ Real.log z) : 0 ≤ (sieveProduct 1 z)⁻¹ - selbergSmoothReciprocalSum n z ∧ (sieveProduct 1 z)⁻¹ - selbergSmoothReciprocalSum n z ≤ 2 * Real.log z * Real.exp (4 * (Real.exp 1 * (1 + Real.log z))) * Real.exp (-Real.log ↑n / Real.log z)

Direct Rankin weighting of the finite smooth tail retains the sharper decay exp (-log n / log z), without an Abel integral or endpoint error. This proves the original bound used by the large-ratio branch (with its literal constant), by weakening the stronger direct moment bound.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsiCarrier_eq_Icc {xi z : ℝ} (hxi : 0 ≤ xi) (hxiZ : xi < z) : selbergRealPsiCarrier xi z = Finset.Icc 1 ⌊xi⌋₊

Below the sifting cutoff every positive integer is smooth, so the source's real Psi carrier is the full interval through floor xi.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsi_eq_floor_of_lt {xi z : ℝ} (hxi : 0 ≤ xi) (hxiZ : xi < z) : selbergRealPsi xi z = ↑⌊xi⌋₊

In the large-cutoff regime used for (3.9), the source's smooth-number count is exactly floor xi.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealPsi_sq_le {xi z : ℝ} (hxi : 0 ≤ xi) (hxiZ : xi < z) : selbergRealPsi xi z ^ 2 ≤ xi ^ 2

The smooth-number error in Theorem 2 is bounded by the square of the chosen real level whenever that level lies below z.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealSmoothReciprocalSum_eq_harmonic {xi z : ℝ} (hxi : 0 ≤ xi) (hxiZ : xi < z) : selbergRealSmoothReciprocalSum xi z = ↑(harmonic ⌊xi⌋₊)

When xi < z, the reciprocal smooth-number sum in Theorem 2 is the ordinary harmonic sum through floor xi.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.log_le_selbergRealSmoothReciprocalSum {xi z : ℝ} (hxi : 0 ≤ xi) (hxiZ : xi < z) : Real.log xi ≤ selbergRealSmoothReciprocalSum xi z

The harmonic integral bound gives the explicit denominator input used in the source derivation of (3.9).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.selbergRealSmoothReciprocalSum_mono {xi eta z : ℝ} (hxi : xi ≤ eta) : selbergRealSmoothReciprocalSum xi z ≤ selbergRealSmoothReciprocalSum eta z

The real smooth reciprocal sum is monotone in its level.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.fourOneCutoff (y z : ℝ) : ℝ

The level chosen on printed p. 225: xi^2 = y / log z.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.fourOneCutoff y z = √(y / Real.log z)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.fourOneCutoff_sq {y z : ℝ} (hy : 0 ≤ y) (hlog : 0 < Real.log z) : fourOneCutoff y z ^ 2 = y / Real.log z

The defining square identity for the level on printed p. 225.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.log_fourOneCutoff {y z : ℝ} (hy : 0 < y) (hlog : 0 < Real.log z) : Real.log (fourOneCutoff y z) = (Real.log y - Real.log (Real.log z)) / 2

Logarithmic form of the defining level identity on printed p. 225.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.log_sub_log_two_le_log_floor {xi : ℝ} (hxi : 2 ≤ xi) : Real.log xi - Real.log 2 ≤ Real.log ↑⌊xi⌋₊

Passing from a real Selberg level at least two to its natural floor costs at most log 2, the floor loss used in the auxiliary large-ratio bound.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.rpow_quarter_le_fourOneCutoff {y z : ℝ} (hy : 0 < y) (hz : 0 < z) (hlog : 2 ≤ Real.log z) (hzy : Real.log z ≤ Real.log y) : z ^ (1 / 4) ≤ fourOneCutoff y z

The source's auxiliary lower range n ≤ z^(1/4) ≤ fourOneCutoff y z.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.quarter_log_le_fourOneSmoothReciprocalSum {y z : ℝ} (hy : 0 < y) (hz : 0 < z) (hlog : 2 ≤ Real.log z) (hzy : Real.log z ≤ Real.log y) : Real.log z / 4 ≤ selbergRealSmoothReciprocalSum (fourOneCutoff y z) z

The harmonic lower bound through the literal z^(1/4) range on printed p. 225.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.realLevelSelbergDenominator (source : RegularSource) (z xi : ℝ) : ℝ

The literal source denominator at real level xi.

Equations

• source.realLevelSelbergDenominator z xi = source.levelSelbergDenominator z ⌊xi⌋₊

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.realLevelSelbergWeight (source : RegularSource) (z xi : ℝ) : ℕ → ℝ

The literal source Selberg weight at real level xi.

Equations

• source.realLevelSelbergWeight z xi = source.levelSelbergWeight z ⌊xi⌋₊

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.realLevelSelbergDenominator_eq (source : RegularSource) {z xi : ℝ} (hxi : 0 ≤ xi) : source.realLevelSelbergDenominator z xi = selbergRealReciprocalTotientSum source.k xi z

The real-level denominator is the source's real reciprocal-totient sum.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.realLevelSelbergWeight_eq_printed (source : RegularSource) (z : ℝ) {xi : ℝ} {d : ℕ} (hxi : 1 < xi) (hd : d ∣ (siftingPrimes source.k z).prod id) (hdxi : ↑d ≤ xi) : source.realLevelSelbergWeight z xi d = ↑(ArithmeticFunction.moebius d) * ↑d / ↑d.totient * (selbergRealReciprocalTotientSum (source.k * d) (xi / ↑d) z / selbergRealReciprocalTotientSum source.k xi z)

At every real level xi > 1, the constructed optimizer is exactly the paper's printed coefficient with the real quotient cutoff xi / d.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.realLevelSelbergDenominator_pos (source : RegularSource) (z : ℝ) {xi : ℝ} (hxi : 1 < xi) : 0 < source.realLevelSelbergDenominator z xi

The real-level denominator is positive throughout the source range xi > 1.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.realLevelSelbergWeight_support (source : RegularSource) (z : ℝ) {xi : ℝ} {d : ℕ} (hxi : 0 ≤ xi) (hd : source.realLevelSelbergWeight z xi d ≠ 0) : d ∣ (siftingPrimes source.k z).prod id ∧ ↑d ≤ xi

Nonzero real-level weights satisfy the literal support inequalities.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.realLevelSelbergLambdaSquared_mass_le_psi_sq (source : RegularSource) {z xi : ℝ} (hz : 1 < z) (hxi : 1 < xi) : ∑ d ∈ ((siftingPrimes source.k z).prod id).divisors, |BoundingSieve.lambdaSquared (source.realLevelSelbergWeight z xi) d| ≤ selbergRealPsi xi z ^ 2

The complete Lambda^2 mass estimate at every real source level.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.siftedCount_le_realLevelSelberg_psi (source : RegularSource) {z xi : ℝ} (hz : 1 < z) (hxi : 1 < xi) : siftedCount source.carrier source.k z ≤ source.y * (source.realLevelSelbergDenominator z xi)⁻¹ + selbergRealPsi xi z ^ 2

The real-cutoff form of the source-faithful finite Selberg estimate.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.siftedCount_le_theoremTwo (source : RegularSource) {z xi : ℝ} (hz : 1 < z) (hxi : 1 < xi) : siftedCount source.carrier source.k z ≤ source.y * sieveProduct source.k z / (sieveProduct 1 z * selbergRealSmoothReciprocalSum xi z) + selbergRealPsi xi z ^ 2

Theorem 2 (3.5) for the literal gamma(p)=1, q=1 source. Lemma 3.1 replaces the Selberg denominator by the normalized reciprocal smooth-number sum without introducing a generic-density estimate premise.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.siftedCount_le_theoremTwo_log (source : RegularSource) {z xi : ℝ} (hz : 1 < z) (hxi : 1 < xi) (hxiZ : xi < z) : siftedCount source.carrier source.k z ≤ source.y * sieveProduct source.k z / (sieveProduct 1 z * Real.log xi) + xi ^ 2

The large-cutoff form of Theorem 2 before Mertens is substituted: when xi < z, its denominator is bounded below by the literal harmonic integral and its complete Selberg error is at most xi^2.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.exists_siftedCount_le_theoremTwo_mertens : ∃ B > 0, ∀ (source : RegularSource) {z xi : ℝ}, 1 < z → 1 < xi → xi < z → siftedCount source.carrier source.k z ≤ source.y * sieveProduct source.k z * ((Real.exp Real.eulerMascheroniConstant * Real.log z + B) / Real.log xi) + xi ^ 2

Theorem 2 after the exact uniform Mertens inversion. This is the analytic form immediately preceding the source's optimization xi^2 = y / (1 + log(y)^2) in (3.9).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.sieveProduct_one_le (k : ℕ) (z : ℝ) : sieveProduct 1 z ≤ sieveProduct k z

Omitting the primes dividing k can only increase the literal Euler product.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.exists_siftedCount_le_rankin_logSq_of_ratio_le : ∃ C > 0, ∀ (source : RegularSource) {z : ℝ}, 0 < z → 2 ≤ Real.log z → Real.log z ≤ Real.log source.y → Real.log source.y / Real.log z ^ 2 ≤ 32 * Real.exp 1 + 2 → siftedCount source.carrier source.k z ≤ source.y * sieveProduct source.k z * (1 + C * Real.exp (-Real.log source.y / Real.log z ^ 2))

The complementary-ratio branch of the auxiliary logarithmic-square bound. Theorem 2, the source cutoff xi^2 = y / log z, and the harmonic denominator give a uniform multiple of the main term; bounded log y / log(z)^2 converts that multiple to the required exponential scale.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.exists_siftedCount_le_rankin_logSq_of_ratio_ge : ∃ C > 0, ∀ (source : RegularSource) {z : ℝ}, 0 < z → 2 ≤ Real.log z → Real.log z ≤ Real.log source.y → 32 * Real.exp 1 + 2 ≤ Real.log source.y / Real.log z ^ 2 → siftedCount source.carrier source.k z ≤ source.y * sieveProduct source.k z * (1 + C * Real.exp (-Real.log source.y / Real.log z ^ 2))

The genuinely large-ratio branch of the auxiliary logarithmic-square bound. Here the finite Rankin tail controls the Selberg denominator and a logarithmic-square Rankin consequence controls the complete Selberg error, both at the source cutoff xi^2 = y / log z.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.exists_siftedCount_le_rankin_logSq : ∃ C > 0, ∀ (source : RegularSource) {z : ℝ}, 0 < z → 1 ≤ Real.log z → Real.log z ≤ Real.log source.y → siftedCount source.carrier source.k z ≤ source.y * sieveProduct source.k z * (1 + C * Real.exp (-Real.log source.y / Real.log z ^ 2))

An auxiliary upper bound for the literal gamma(p)=1, q=1 source. This is not printed (4.1): the scan has denominator log z, not (log z)^2. The weaker rate here does not imply (4.2) on its printed range. The proof separates bounded z by finite Möbius expansion, then combines the Rankin tail with the harmonic/trivial-Psi estimate.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.siftedCount_le_y_add_one (source : RegularSource) (z : ℝ) : siftedCount source.carrier source.k z ≤ source.y + 1

The d = 1 case of the printed regularity hypothesis bounds the whole source, hence every sifted subset, by y + 1.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.threeNineCutoff (y : ℝ) : ℝ

The source's literal optimizing cutoff xi^2 = y / (1 + log(y)^2).

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.threeNineCutoff y = √(y / (1 + Real.log y ^ 2))

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.threeNineCutoff_sq {y : ℝ} (hy : 0 ≤ y) : threeNineCutoff y ^ 2 = y / (1 + Real.log y ^ 2)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.exists_siftedCount_le_threeNine_of_log_ge : ∃ c₁ > 0, ∀ (source : RegularSource) {z : ℝ}, 64 ≤ Real.log source.y → √source.y ≤ z → siftedCount source.carrier source.k z ≤ source.y * sieveProduct source.k z * (2 * Real.exp Real.eulerMascheroniConstant * Real.log z / Real.log source.y + c₁ * Real.log z * Real.log (Real.log (3 * source.y)) / Real.log source.y ^ 2)

The exact large-y branch of the source corollary (3.9), at the literal choice xi^2 = y / (1 + log(y)^2). All constants are absolute and the bounded branch is deliberately not hidden in this theorem.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.RegularSource.exists_siftedCount_le_threeNine : ∃ c₁ > 0, ∀ (source : RegularSource) {z : ℝ}, √source.y ≤ z → siftedCount source.carrier source.k z ≤ source.y * sieveProduct source.k z * (2 * Real.exp Real.eulerMascheroniConstant * Real.log z / Real.log source.y + c₁ * Real.log z * Real.log (Real.log (3 * source.y)) / Real.log source.y ^ 2)

The source corollary (3.9) with one absolute constant. The large range uses the paper's literal optimized cutoff; the complementary bounded range is absorbed symbolically from H_k(M) at d = 1 and the same Mertens inversion, without enumerating any values of y or z.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.densitySum_insert (D q : ℕ) (P : Finset ℕ) (hq : q ∉ P) : LinearSieve.upperRosserSetDensitySum localDensity D (insert q P) = ∑ s ∈ P.powerset, (LinearSieve.upperRosserSetWeight D s + localDensity q * LinearSieve.upperRosserSetWeight D (insert q s)) * ∏ p ∈ s, localDensity p

Exact one-prime identity for the adapted finite Rosser coefficient at 1 / p. Its correspondence with the concrete source-count identity (2.2) is still to be proved.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.fixedDepthRelativeDensity_succ {D q : ℕ} {P : Finset ℕ} (hqs : q ∉ P) (hqprime : Nat.Prime q) (hprime : ∀ p ∈ P, Nat.Prime p) (hqmin : ∀ p ∈ P, q ≤ p) (r : ℕ) : LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity localDensity D q P (r + 1) = ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ p₀ ^ 3 < D, LinearSieve.upperRosserBoundaryRelativePairTransition localDensity P p₀ p₁ * LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity localDensity (D ⌈/⌉ (p₀ * p₁)) q ({p ∈ P | p < p₁}) r

The adapted finite-depth coefficient recursion obtained by removing two boundary primes. No infinite-depth limit or source-count correspondence is asserted.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.densityRatio_eq_finiteBoundaryDepths {D : ℕ} (P : Finset ℕ) (hD : 1 < D) (hprime : ∀ p ∈ P, Nat.Prime p) (hpD : ∀ p ∈ P, p < D) : LinearSieve.upperRosserSetDensitySum localDensity D P / ∏ p ∈ P, (1 - localDensity p) = 1 + ∑ q ∈ P, localDensity q / (1 - localDensity q) * ∑ r ∈ Finset.range ({p ∈ P | q < p}.card + 1), LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity localDensity D q ({p ∈ P | q < p}) r

Exact normalized finite boundary expansion for the adapted coefficient model at gamma(p) = 1. It is finite, but is not yet the paper's concrete Theorem 1 expansion of siftedCount.

def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.alternatingSign (i : ℕ) : ℝ

The sign (-1)^i, kept as a real number for the finite comparison.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.alternatingSign i = if Even i then 1 else -1

def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.alternatingSum (I : Finset ℕ) (a : ℕ → ℝ) : ℝ

A finite alternating sum over an explicitly supplied carrier.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.alternatingSum I a = ∑ i ∈ I, MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.alternatingSign i * a i

def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.finiteExpansion (r : ℕ) (initial : ℝ) (interior : ℕ → ℝ) (terminal : ℝ) (boundary : ℕ → ℝ) : ℝ

The four finite pieces common to Jurkat--Richert Theorems 1 and 4: the initial term, the depths 1 ≤ i < r, the depth-r terminal term, and the boundary depths 1 ≤ i ≤ r.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.finiteExpansion r initial interior terminal boundary = initial + MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.alternatingSum (Finset.Ico 1 r) interior + MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.alternatingSign r * terminal + MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.alternatingSum (Finset.Icc 1 r) boundary

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.alternatingSum_sub (I : Finset ℕ) (a b : ℕ → ℝ) (y : ℝ) : (alternatingSum I fun (i : ℕ) => a i - y * b i) = alternatingSum I a - y * alternatingSum I b

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.finiteExpansion_comparison (r : ℕ) (y aInitial bInitial : ℝ) (aInterior bInterior : ℕ → ℝ) (aTerminal bTerminal : ℝ) (aBoundary bBoundary : ℕ → ℝ) : finiteExpansion r aInitial aInterior aTerminal aBoundary - y * finiteExpansion r bInitial bInterior bTerminal bBoundary = finiteExpansion r (aInitial - y * bInitial) (fun (i : ℕ) => aInterior i - y * bInterior i) (aTerminal - y * bTerminal) fun (i : ℕ) => aBoundary i - y * bBoundary i

Algebraic term-by-term subtraction for two finite expansions with the source shape. ChenFiniteDiscrepancy applies the concrete Theorems 1 and 4, including Theorem 4's uniform remainder.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.signed_finiteExpansion_comparison (nu r : ℕ) (y count model aInitial bInitial : ℝ) (aInterior bInterior : ℕ → ℝ) (aTerminal bTerminal : ℝ) (aBoundary bBoundary : ℕ → ℝ) (hcount : count = finiteExpansion r aInitial aInterior aTerminal aBoundary) (hmodel : model = finiteExpansion r bInitial bInterior bTerminal bBoundary) : alternatingSign nu * (count - y * model) = alternatingSign nu * finiteExpansion r (aInitial - y * bInitial) (fun (i : ℕ) => aInterior i - y * bInterior i) (aTerminal - y * bTerminal) fun (i : ℕ) => aBoundary i - y * bBoundary i

The signed version of finiteExpansion_comparison, with the outer parity sign used on page 230. ChenFiniteDiscrepancy supplies the two concrete source expansions.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.terminalTheta (epsilon : ℝ) : ℝ

The one-step factor produced by the 1965 Lemma 5.2 iteration.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.terminalTheta epsilon = Real.exp 1 / 3 * (1 + epsilon)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.terminalTheta_nonneg {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) : 0 ≤ terminalTheta epsilon

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.terminalTheta_le_nineHundredSevenThousandths {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hepsilonSmall : epsilon ≤ 1 / 10000) : terminalTheta epsilon ≤ 907 / 1000

Once the source error in Lemma 5.2 is at most 10⁻⁴, its factor is at most 0.907. This preserves the small numerical margin needed beyond the critical exponent 5/21.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.terminal_le_theta_pow (terminal : ℕ → ℝ) (theta : ℝ) (htheta : 0 ≤ theta) (hstep : ∀ (r : ℕ), terminal (r + 1) ≤ theta * terminal r) (r : ℕ) : terminal r ≤ theta ^ r * terminal 0

Finite repeated elimination of terminal sums. This is the induction actually used after Lemma 5.2; it does not construct an infinite chain.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.nineHundredSevenThousandths_pow_fifty : (907 / 1000) ^ 50 ≤ (2 / 3) ^ 12

A strict-margin rational block inequality for the terminal exponent: 0.907^50 ≤ (2/3)^12. Here 12/50 > 5/21, leaving room to absorb the log-log factor introduced by the source depth choice (6.3).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.terminalTheta_pow_fifty_mul_le {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hepsilonSmall : epsilon ≤ 1 / 10000) (m : ℕ) : terminalTheta epsilon ^ (50 * m) ≤ (2 / 3) ^ (12 * m)

Lemma 5.2's finite iteration contracts every block of 50 eliminations by at least (2/3)^12, once its explicit source error is at most 10⁻⁴.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.terminalTheta_pow_le_block {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hepsilonSmall : epsilon ≤ 1 / 10000) (r : ℕ) : terminalTheta epsilon ^ r ≤ (2 / 3) ^ (12 * (r / 50))

The strict block estimate applies to every finite depth, with the final incomplete block retained through r / 50.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.terminal_le_strict_block (terminal : ℕ → ℝ) {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hepsilonSmall : epsilon ≤ 1 / 10000) (hterminalZero : 0 ≤ terminal 0) (hstep : ∀ (r : ℕ), terminal (r + 1) ≤ terminalTheta epsilon * terminal r) (r : ℕ) : terminal r ≤ (2 / 3) ^ (12 * (r / 50)) * terminal 0

Direct finite terminal-sum consumer at the arbitrary parity-compatible depth selected by (6.3). Converting this strict block exponent to the final logarithmic bound is a separate analytic step.