The reduced-residue discrepancy and its actual coprime-mass correction

Fouvry's discrepancy subtracts the modulus-dependent coprime mass, not a fixed X / φ(d). The identity below displays that difference explicitly. For a set of primes its correction is bounded by finite harmonic sums; no equidistribution theorem is asserted or assumed.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.primeCoprimeMass (I : Finset ℕ) (d : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.primeCoprimeMass I d = ∑ p ∈ I, if p.Coprime d then 1 else 0

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.primeProgressionDiscrepancy (I : Finset ℕ) (a d : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.primeProgressionDiscrepancy I a d = (∑ p ∈ I, if p ≡ a [MOD d] then 1 else 0) - MathlibNt.SieveTheory.LiLiuPrereqWF.primeCoprimeMass I d * (↑d.totient)⁻¹

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.familyProgressionDiscrepancy (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (label : ℕ → ℕ) (I : Finset ℕ) (a : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.familyProgressionDiscrepancy upper P D ε label I a = ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags upper P D ε label, ∑ d ∈ Finset.Icc 1 ⌊D ^ (1 + ε + ε ^ 9)⌋₊ with d.Coprime a, (MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm upper P D ε t) d * MathlibNt.SieveTheory.LiLiuPrereqWF.primeProgressionDiscrepancy I a d

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.familyCoprimeCorrection (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (label : ℕ → ℕ) (I : Finset ℕ) (a : ℕ) (X : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.familyCoprimeCorrection upper P D ε label I a X = ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags upper P D ε label, ∑ d ∈ Finset.Icc 1 ⌊D ^ (1 + ε + ε ^ 9)⌋₊ with d.Coprime a, (MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm upper P D ε t) d * ((MathlibNt.SieveTheory.LiLiuPrereqWF.primeCoprimeMass I d - X) * (↑d.totient)⁻¹)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm_coprime_of_ne_zero (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (t : List ℕ) {a d : ℕ} (hP : ∀ p ∈ P, p.Coprime a) (hd : (signedFamilyTerm upper P D ε t) d ≠ 0) : d.Coprime a

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.shifted_sequence_progression (I : Finset ℕ) (a d : ℕ) (hI : ∀ p ∈ I, p ≤ a) : sequenceDivisibility I (fun (p : ℕ) => a - p) d = ∑ p ∈ I, if p ≡ a [MOD d] then 1 else 0

The original shifted count is an actual progression count, including the endpoint p = a; no sieve or distribution estimate enters this identity.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.fullSignedFamilyRemainder_progression_identity (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (label : ℕ → ℕ) (I : Finset ℕ) (a : ℕ) (X : ℝ) (hP : ∀ p ∈ P, p.Coprime a) (hI : ∀ p ∈ I, p ≤ a) : fullSignedFamilyRemainder upper P D ε label I (fun (p : ℕ) => a - p) X (progressionDensity a) = familyProgressionDiscrepancy upper P D ε label I a + familyCoprimeCorrection upper P D ε label I a X

Full-modulus transport is not silently identified with Fouvry's discrepancy: its additional coprime-mass term is retained exactly. The reduced-modulus restriction follows from the ORIGINAL coefficient support.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeCoprimeMass_identity (I : Finset ℕ) (hI : ∀ p ∈ I, Nat.Prime p) (d : ℕ) : primeCoprimeMass I d = ↑I.card - ∑ p ∈ I, if p ∣ d then 1 else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.prime_divisor_mass_le (I : Finset ℕ) (hI : ∀ p ∈ I, Nat.Prime p) (N T : ℕ) (hN : ∀ p ∈ I, p ≤ N) : ∑ d ∈ Finset.Icc 1 T, (∑ p ∈ I, if p ∣ d then 1 else 0) * (↑d.totient)⁻¹ ≤ PrimeSquareMass.harmonicSum N ^ 2 * PrimeSquareMass.harmonicSum T ^ 2

Only the actual prime entries dividing the modulus are removed from the coprime mass. Their total inverse-totient cost is logarithmic, not proportional to the cardinality of the prime sequence.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.coprimeCorrection_abs_le (f : ArithmeticFunction ℝ) (hf : BoundedOne f) (I : Finset ℕ) (hI : ∀ p ∈ I, Nat.Prime p) (N T a : ℕ) (hN : ∀ p ∈ I, p ≤ N) (X : ℝ) : |∑ d ∈ Finset.Icc 1 T with d.Coprime a, f d * ((primeCoprimeMass I d - X) * (↑d.totient)⁻¹)| ≤ (|↑I.card - X| + PrimeSquareMass.harmonicSum N ^ 2) * PrimeSquareMass.harmonicSum T ^ 2

A bounded unmasked coefficient needs no squarefree restriction for this prime-sequence coprime-mass estimate.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.familyCoprimeCorrection_abs_le (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (I : Finset ℕ) (hI : ∀ p ∈ I, Nat.Prime p) (N a : ℕ) (hN : ∀ p ∈ I, p ≤ N) (X : ℝ) : |familyCoprimeCorrection upper P D ε label I a X| ≤ ↑(signedTags upper P D ε label).card * ((|↑I.card - X| + PrimeSquareMass.harmonicSum N ^ 2) * PrimeSquareMass.harmonicSum ⌊D ^ (1 + ε + ε ^ 9)⌋₊ ^ 2)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.primeProgressionTransportCost (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (label : ℕ → ℕ) (I : Finset ℕ) (N : ℕ) (X : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.primeProgressionTransportCost upper P D ε label I N X = MathlibNt.SieveTheory.LiLiuPrereqWF.fullModulusTransportCost upper P D ε label N X + ↑(MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags upper P D ε label).card * ((|↑I.card - X| + MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.harmonicSum N ^ 2) * MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.harmonicSum ⌊D ^ (1 + ε + ε ^ 9)⌋₊ ^ 2)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamily_reduced_prime_sequence_sieve (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hcut : ∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < √D) (I : Finset ℕ) (hIprime : ∀ p ∈ I, Nat.Prime p) (N : ℕ) (hI : ∀ p ∈ I, p < N) (hPN : ∀ p ∈ P, p.Coprime N) (X : ℝ) : have label := geometricSieveLabel D ε; have g := progressionDensity N; X * signedFamilyDensity false P D ε label g + familyProgressionDiscrepancy false P D ε label I N - primeProgressionTransportCost false P D ε label I N X ≤ sequenceSifted I (fun (p : ℕ) => N - p) P ∧ sequenceSifted I (fun (p : ℕ) => N - p) P ≤ X * signedFamilyDensity true P D ε label g + familyProgressionDiscrepancy true P D ε label I N + primeProgressionTransportCost true P D ε label I N X

The actual prime-shift consumer, with the full reduced-residue discrepancy and both corrections paid. When X = #I the fixed-mass discrepancy vanishes. Any analytic distribution bound on the displayed signed discrepancy is a separate theorem; it has not been inserted as a hypothesis here.