Unmasked transport for the fixed external families

The full-modulus and reduced-progression sums use precisely externalTerm. The quantitative hypotheses remain positive/injective or prime-shift ones; arbitrary weighted convolution consumers are not asserted here.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.externalFullRemainder {ι : Type u_1} (upper : Bool) (P : Finset ℕ) (D ε z : ℝ) (I : Finset ι) (a : ι → ℕ) (X : ℝ) (g : ArithmeticFunction ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.externalFullRemainder upper P D ε z I a X g = ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags upper P D ε z, ∑ d ∈ Finset.Icc 1 ⌊D ^ (1 + ε + ε ^ 9)⌋₊, (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm upper P D ε z t) d * MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceRemainder I a X g d

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.externalFullTransportCost (upper : Bool) (P : Finset ℕ) (D ε z : ℝ) (N : ℕ) (X : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.externalFullTransportCost upper P D ε z N X = if z ≤ √D then MathlibNt.SieveTheory.LiLiuPrereqWF.fullModulusTransportCost upper P D ε (MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSieveLabel D ε) N X else if upper = true then MathlibNt.SieveTheory.LiLiuPrereqWF.fullModulusTransportCost true (MathlibNt.SieveTheory.LiLiuPrereqWF.externalEdgePrimes P D) D ε (MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSieveLabel D ε) N X else 0

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.externalProgressionDiscrepancy (upper : Bool) (P : Finset ℕ) (D ε z : ℝ) (I : Finset ℕ) (a : ℕ) : ℝ

Equations

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

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

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.externalPrimeTransportCost upper P D ε z I N X = if z ≤ √D then MathlibNt.SieveTheory.LiLiuPrereqWF.primeProgressionTransportCost upper P D ε (MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSieveLabel D ε) I N X else if upper = true then MathlibNt.SieveTheory.LiLiuPrereqWF.primeProgressionTransportCost true (MathlibNt.SieveTheory.LiLiuPrereqWF.externalEdgePrimes P D) D ε (MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSieveLabel D ε) I N X else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalFullRemainder_eq {ι : Type u_1} (upper : Bool) (P : Finset ℕ) (D ε z : ℝ) (I : Finset ι) (a : ι → ℕ) (X : ℝ) (g : ArithmeticFunction ℝ) : externalFullRemainder upper P D ε z I a X g = if z ≤ √D then fullSignedFamilyRemainder upper P D ε (geometricSieveLabel D ε) I a X g else if upper = true then fullSignedFamilyRemainder true (externalEdgePrimes P D) D ε (geometricSieveLabel D ε) I a X g else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalProgressionDiscrepancy_eq (upper : Bool) (P : Finset ℕ) (D ε z : ℝ) (I : Finset ℕ) (a : ℕ) : externalProgressionDiscrepancy upper P D ε z I a = if z ≤ √D then familyProgressionDiscrepancy upper P D ε (geometricSieveLabel D ε) I a else if upper = true then familyProgressionDiscrepancy true (externalEdgePrimes P D) D ε (geometricSieveLabel D ε) I a else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalFamily_full_sequence_sieve {ι : Type u_1} (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε z : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hcut : ∀ p ∈ P, ↑p < z) (I : Finset ι) (a : ι → ℕ) (N : ℕ) (ha : ∀ i ∈ I, 0 < a i ∧ a i ≤ N) (hinj : Set.InjOn a ↑I) (X : ℝ) {g : ArithmeticFunction ℝ} (hg : ∀ (d : ℕ), |g d| ≤ (↑d.totient)⁻¹) : X * externalDensity false P D ε z g + externalFullRemainder false P D ε z I a X g - externalFullTransportCost false P D ε z N X ≤ sequenceSifted I a P ∧ sequenceSifted I a P ≤ X * externalDensity true P D ε z g + externalFullRemainder true P D ε z I a X g + externalFullTransportCost true P D ε z N X

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalFamily_reduced_prime_sieve (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε z : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hcut : ∀ p ∈ P, ↑p < z) (I : Finset ℕ) (hIprime : ∀ p ∈ I, Nat.Prime p) (N : ℕ) (hI : ∀ p ∈ I, p < N) (hPN : ∀ p ∈ P, p.Coprime N) (X : ℝ) : X * externalDensity false P D ε z (progressionDensity N) + externalProgressionDiscrepancy false P D ε z I N - externalPrimeTransportCost false P D ε z I N X ≤ sequenceSifted I (fun (p : ℕ) => N - p) P ∧ sequenceSifted I (fun (p : ℕ) => N - p) P ≤ X * externalDensity true P D ε z (progressionDensity N) + externalProgressionDiscrepancy true P D ε z I N + externalPrimeTransportCost true P D ε z I N X

This is the actual reduced residue discrepancy, not a maximal absolute error and not a squarefree-masked weight. Both transport costs are retained.