Finite sieve inequalities for the fixed normalized signed family

The full-integer family is not squarefree-masked. Consequently its sieve inequalities are stated over divisors of the sieve primorial (or its gcd with an arbitrary integer), not over unrestricted divisors.

We first sum the actual small Rosser weights on the positive and negative rough branches separately. Only then do we use the normalized rough sieve inequalities. The tight lower-even convention remains that of (18).

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.sum_powerset_partition (N B : Finset ℕ) (f : Finset ℕ → Finset ℕ → ℝ) : ∑ s ∈ N.powerset, f (s \ B) (s ∩ B) = ∑ r ∈ (N \ B).powerset, ∑ a ∈ (N ∩ B).powerset, f r a

The actual powerset bijection used in the small/rough join.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedSignedSet_small_sum_bounds (P A r : Finset ℕ) {D ε : ℝ} (b c : ℕ → ℝ) (hD : 2 ≤ D) (hε : 0 < ε) (hε1 : ε ≤ 1) (hA : A ⊆ geometricSmallPrimes P D ε) : (normalizedLowerSet b c D r * ∑ a ∈ A.powerset, (signedSmallWeight false P D ε r.card) (a.prod id) ≤ normalizedLowerSet b c D r * if A = ∅ then 1 else 0) ∧ (normalizedUpperSet b c D r * if A = ∅ then 1 else 0) ≤ normalizedUpperSet b c D r * ∑ a ∈ A.powerset, (signedSmallWeight true P D ε r.card) (a.prod id)

Each rough branch is multiplied only after the small divisor sum is bounded with its correct sign. In particular no small coefficient is assumed nonnegative.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyAggregate_divisor_sum_partition (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hlabel : ∀ p ∈ P \ geometricSmallPrimes P D ε, p ∈ geometricPrimeBox P D ε (ε ^ 9) (label p)) (hhead : ∀ p ∈ P \ geometricSmallPrimes P D ε, geometricLower D ε (ε ^ 9) (label p) ^ 2 < D) {n : ℕ} (hn : Squarefree n) (hsub : n.primeFactors ⊆ P) : ∑ d ∈ n.divisors, (signedFamilyAggregate upper P D ε label) d = ∑ r ∈ (n.primeFactors \ geometricSmallPrimes P D ε).powerset, normalizedSignedSet upper (fun (p : ℕ) => geometricLower D ε (ε ^ 9) (label p)) (fun (p : ℕ) => geometricLower D ε (ε ^ 9) (label p) ^ (1 + ε ^ 9)) D r * ∑ a ∈ (n.primeFactors ∩ geometricSmallPrimes P D ε).powerset, (signedSmallWeight upper P D ε r.card) (a.prod id)

Exact sum reindexing for the same full-integer aggregate. The outer variable is the rough prime subset, so its sign and small-weight choice stay fixed throughout the inner sum.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyAggregate_divisor_sum_bounds (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hlabel : ∀ p ∈ P \ geometricSmallPrimes P D ε, p ∈ geometricPrimeBox P D ε (ε ^ 9) (label p)) (hhead : ∀ p ∈ P \ geometricSmallPrimes P D ε, geometricLower D ε (ε ^ 9) (label p) ^ 2 < D) {n : ℕ} (hn : n ∣ P.prod id) : (∑ d ∈ n.divisors, (signedFamilyAggregate false P D ε label) d ≤ if n = 1 then 1 else 0) ∧ (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, (signedFamilyAggregate true P D ε label) d

Both finite sieve directions for the actual normalized family, on a divisor of the fixed prime product. Geometric membership and the source head restriction are the only box-label inputs.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyAggregate_gcd_divisor_sum_bounds (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hlabel : ∀ p ∈ P \ geometricSmallPrimes P D ε, p ∈ geometricPrimeBox P D ε (ε ^ 9) (label p)) (hhead : ∀ p ∈ P \ geometricSmallPrimes P D ε, geometricLower D ε (ε ^ 9) (label p) ^ 2 < D) (n : ℕ) : (∑ d ∈ (n.gcd (P.prod id)).divisors, (signedFamilyAggregate false P D ε label) d ≤ if n.Coprime (P.prod id) then 1 else 0) ∧ (if n.Coprime (P.prod id) then 1 else 0) ≤ ∑ d ∈ (n.gcd (P.prod id)).divisors, (signedFamilyAggregate true P D ε label) d

Restricting to primorial divisors also handles zero, including the empty primorial. No assertion is made about unrestricted prime-power divisors.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSieveLabel (D ε : ℝ) (p : ℕ) : ℕ

The first geometric box whose upper endpoint exceeds p. This choice is fixed independently of every level split and every sieve integer.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSieveLabel D ε p = if h : ∃ (j : ℕ), ↑p < MathlibNt.SieveTheory.LiLiuPrereqWF.geometricLower D ε (ε ^ 9) (j + 1) then Nat.find h else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSieveLabel_mem (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε : ℝ} (hD : 1 < D) (hε : 0 < ε) (p : ℕ) : p ∈ P \ geometricSmallPrimes P D ε → p ∈ geometricPrimeBox P D ε (ε ^ 9) (geometricSieveLabel D ε p)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSieveLabel_head_lt (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε : ℝ} (hD : 1 < D) (hε : 0 < ε) (hcut : ∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < √D) (p : ℕ) : p ∈ P \ geometricSmallPrimes P D ε → geometricLower D ε (ε ^ 9) (geometricSieveLabel D ε p) ^ 2 < D

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyAggregate_canonical_gcd_divisor_sum_bounds (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) (n : ℕ) : (∑ d ∈ (n.gcd (P.prod id)).divisors, (signedFamilyAggregate false P D ε (geometricSieveLabel D ε)) d ≤ if n.Coprime (P.prod id) then 1 else 0) ∧ (if n.Coprime (P.prod id) then 1 else 0) ≤ ∑ d ∈ (n.gcd (P.prod id)).divisors, (signedFamilyAggregate true P D ε (geometricSieveLabel D ε)) d

The canonical label discharges all box hypotheses under the usual rough-prime cutoff p < sqrt D. The coefficients remain unchanged.