Transport to full-modulus sums without masking the WF coefficients

The exact transport holds for arbitrary indexed sequences, including zeros and multiplicities. Its quantitative version has separate, explicit sequence hypotheses and uses the canonical arithmetic-progression density 1 / φ(d) on reduced residue classes. A prime-only dimension-one condition is never used to control arbitrary prime-power densities.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity (a : ℕ) : ArithmeticFunction ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity a = { toFun := fun (d : ℕ) => if d.Coprime a then (↑d.totient)⁻¹ else 0, map_zero' := ⋯ }

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity_abs_le (a d : ℕ) : |(progressionDensity a) d| ≤ (↑d.totient)⁻¹

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

Equations

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

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

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.exceptionalFamilyRemainder upper P D ε label I a X g = ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags upper P D ε label, ∑ d ∈ Finset.Icc 1 ⌊D ^ (1 + ε + ε ^ 9)⌋₊ with ¬d ∣ P.prod id, (MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm upper P D ε t) d * MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceRemainder I a X g d

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

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.fullModulusTransportCost upper P D ε label N X = ↑(MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags upper P D ε label).card * ((↑N + |X|) * (4 / D ^ ε ^ 2 * (1 + Real.log ↑⌊D ^ (1 + ε + ε ^ 9)⌋₊) ^ 2))

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.supported_sum_split_primorial {f : ArithmeticFunction ℝ} {Q : ℝ} (hQ : 0 ≤ Q) (hf : SupportedAt f Q) {M : ℕ} (hM : M ≠ 0) (r : ℕ → ℝ) : ∑ d ∈ Finset.Icc 1 ⌊Q⌋₊, f d * r d = ∑ d ∈ M.divisors, f d * r d + ∑ d ∈ Finset.Icc 1 ⌊Q⌋₊ with ¬d ∣ M, f d * r d

Only the summation region changes. The arithmetic function in all three sums is identical, with its non-squarefree extension intact.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyRemainder_full_identity {ι : Type u_1} (upper : Bool) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (I : Finset ι) (a : ι → ℕ) (X : ℝ) (g : ArithmeticFunction ℝ) : fullSignedFamilyRemainder upper P D ε label I a X g = signedFamilyRemainder upper P D ε label I a X g + exceptionalFamilyRemainder upper P D ε label I a X g

Exact restricted-to-full transport for the actual family and actual remainders, with no assumptions on the sequence or density.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceDivisibility_le_div {ι : Type u_1} (I : Finset ι) (a : ι → ℕ) (N : ℕ) (ha : ∀ i ∈ I, 0 < a i ∧ a i ≤ N) (hinj : Set.InjOn a ↑I) (d : ℕ) : sequenceDivisibility I a d ≤ ↑N / ↑d

Divisibility counts for a genuinely injective positive bounded sequence. The exact transport above does not require these quantitative hypotheses.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceRemainder_abs_le_inv_totient {ι : Type u_1} (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)⁻¹) {d : ℕ} (hd : 0 < d) : |sequenceRemainder I a X g d| ≤ (↑N + |X|) * (↑d.totient)⁻¹

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.exceptionalFamilyRemainder_abs_le {ι : Type u_1} (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (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)⁻¹) : |exceptionalFamilyRemainder upper P D ε label I a X g| ≤ ↑(signedTags upper P D ε label).card * ((↑N + |X|) * (4 / D ^ ε ^ 2 * (1 + Real.log ↑⌊D ^ (1 + ε + ε ^ 9)⌋₊) ^ 2))

Quantitative transport for a canonical-density majorant. It costs 4 J (N+|X|) (1+log(floor Q))^2 / D^(epsilon^2), with the ACTUAL tag count J. No family-cardinality estimate is assumed. The all-modulus density majorant is explicit, and is proved above for progressionDensity.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamily_full_sequence_sieve {ι : Type u_1} (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 ι) (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)⁻¹) : have label := geometricSieveLabel D ε; X * signedFamilyDensity false P D ε label g + fullSignedFamilyRemainder false P D ε label I a X g - fullModulusTransportCost false P D ε label N X ≤ sequenceSifted I a P ∧ sequenceSifted I a P ≤ X * signedFamilyDensity true P D ε label g + fullSignedFamilyRemainder true P D ε label I a X g + fullModulusTransportCost true P D ε label N X

The finite sieve now has genuinely full-modulus signed remainders, against the original WF members. The density remains that of the accepted family; the explicit correction pays both the extra main terms and actual counts.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamily_full_shifted_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 ℕ) (N : ℕ) (hI : ∀ p ∈ I, p < N) (X : ℝ) : have label := geometricSieveLabel D ε; have a := fun (p : ℕ) => N - p; have g := progressionDensity N; X * signedFamilyDensity false P D ε label g + fullSignedFamilyRemainder false P D ε label I a X g - fullModulusTransportCost false P D ε label N X ≤ sequenceSifted I a P ∧ sequenceSifted I a P ≤ X * signedFamilyDensity true P D ε label g + fullSignedFamilyRemainder true P D ε label I a X g + fullModulusTransportCost true P D ε label N X

Concrete Goldbach-shift specialization. Distinct p < N give distinct positive entries N-p; primality may be imposed by the caller's index set. The density is constructed, not supplied as a prime-power bound.