Actual signed remainders for the common normalized family

The sequence keeps its indices, so equal integers retain their multiplicity. All divisor sums are over the sieve primorial. The remainder is the actual divisibility count minus the chosen main density, never an assumed error certificate and never a sum of absolute values.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceDivisibility {ι : Type u_1} (I : Finset ι) (a : ι → ℕ) (d : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceDivisibility I a d = ∑ i ∈ I, if d ∣ a i then 1 else 0

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceSifted {ι : Type u_1} (I : Finset ι) (a : ι → ℕ) (P : Finset ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceSifted I a P = ∑ i ∈ I, if (a i).Coprime (P.prod id) then 1 else 0

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceRemainder {ι : Type u_1} (I : Finset ι) (a : ι → ℕ) (X : ℝ) (g : ArithmeticFunction ℝ) (d : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceRemainder I a X g d = MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceDivisibility I a d - X * g d

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

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyRemainder upper P D ε label I a X g = ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags upper P D ε label, ∑ d ∈ (P.prod id).divisors, (MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm upper P D ε t) d * MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceRemainder I a X g d

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.sum_gcd_divisors_eq_filtered {M : ℕ} (hM : M ≠ 0) (n : ℕ) (f : ℕ → ℝ) : ∑ d ∈ (n.gcd M).divisors, f d = ∑ d ∈ M.divisors, if d ∣ n then f d else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.sequence_divisor_sum {ι : Type u_1} (I : Finset ι) (a : ι → ℕ) {M : ℕ} (hM : M ≠ 0) (f : ℕ → ℝ) : ∑ i ∈ I, ∑ d ∈ ((a i).gcd M).divisors, f d = ∑ d ∈ M.divisors, f d * sequenceDivisibility I a d

Exact double-counting, valid also for zero sequence entries.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamily_main_remainder_identity {ι : Type u_1} (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (label : ℕ → ℕ) (I : Finset ι) (a : ι → ℕ) (X : ℝ) (g : ArithmeticFunction ℝ) : X * signedFamilyDensity upper P D ε label g + signedFamilyRemainder upper P D ε label I a X g = ∑ d ∈ (P.prod id).divisors, (signedFamilyAggregate upper P D ε label) d * sequenceDivisibility I a d

Main density plus the actual signed family remainder is exactly the weighted divisibility count. This holds for arbitrary X and g.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamily_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 : ι → ℕ) (X : ℝ) (g : ArithmeticFunction ℝ) : have label := geometricSieveLabel D ε; X * signedFamilyDensity false P D ε label g + signedFamilyRemainder false P D ε label I a X g ≤ sequenceSifted I a P ∧ sequenceSifted I a P ≤ X * signedFamilyDensity true P D ε label g + signedFamilyRemainder true P D ε label I a X g

A concrete common-WF family gives the true two-sided finite sieve bound with its OWN density and its OWN signed remainder. No density estimate is assumed. The short empty-profile weight is already included in the family.