Finite comparison with the ordinary coarse Rosser density

The normalized signed family and the ordinary Rosser family use the same prime subsets, level, multiplicative density, and parity. Their directed discrepancy is supported on repeated lower endpoints and strict full-product or parity-qualified cubic-prefix boundary crossings. Every coefficient defect has magnitude at most one, not two.

These are finite quantitative comparisons. Estimates of the resulting pair and boundary masses on the analytic scale, and the full coarse F/f estimate, are not asserted here.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.ordinaryRoughSet (upper : Bool) (D : ℝ) (s : Finset ℕ) : ℝ

The ordinary coefficient at the same coarse level, without rounding.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.ordinaryRoughSet upper D s = if upper = true then MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetWeight D s else MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.setWeight D s

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.roughOrdinaryDensity (upper : Bool) (D : ℝ) (R : Finset ℕ) (g : ℕ → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.roughOrdinaryDensity upper D R g = ∑ s ∈ R.powerset, MathlibNt.SieveTheory.LiLiuPrereqWF.ordinaryRoughSet upper D s * ∏ p ∈ s, g p

def MathlibNt.SieveTheory.LiLiuPrereqWF.RoughCollision (b : ℕ → ℝ) (s : Finset ℕ) : Prop

Two distinct original prime slots have the same lower endpoint.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.RoughCollision b s = ¬Set.InjOn b ↑s

def MathlibNt.SieveTheory.LiLiuPrereqWF.RoughBoundaryCrossing (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (s : Finset ℕ) : Prop

Lower endpoints pass every strict test, but upper endpoints fail one.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.RoughBoundaryCrossing upper b c D s = (MathlibNt.SieveTheory.LiLiuPrereqWF.RoundedSupport upper b D s ∧ ¬MathlibNt.SieveTheory.LiLiuPrereqWF.RoundedSupport upper c D s)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.roughCollisionSets (b : ℕ → ℝ) (R : Finset ℕ) : Finset (Finset ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.roughCollisionSets b R = Finset.filter (MathlibNt.SieveTheory.LiLiuPrereqWF.RoughCollision b) R.powerset

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.roughBoundarySets (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (R : Finset ℕ) : Finset (Finset ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.roughBoundarySets upper b c D R = Finset.filter (MathlibNt.SieveTheory.LiLiuPrereqWF.RoughBoundaryCrossing upper b c D) R.powerset

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.roughCollisionMass (b : ℕ → ℝ) (R : Finset ℕ) (g : ℕ → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.roughCollisionMass b R g = ∑ s ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.roughCollisionSets b R, ∏ p ∈ s, g p

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.roughBoundaryMass (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (R : Finset ℕ) (g : ℕ → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.roughBoundaryMass upper b c D R g = ∑ s ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.roughBoundarySets upper b c D R, ∏ p ∈ s, g p

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughBoundaryCrossing_iff (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (s : Finset ℕ) : RoughBoundaryCrossing upper b c D s ↔ RoundedSupport upper b D s ∧ (∏ p ∈ s, b p < D ∧ D ≤ ∏ p ∈ s, c p ∨ ∃ p ∈ s, ({q ∈ s | p ≤ q}.card % 2 = if upper = true then 1 else 0) ∧ (∏ q ∈ s with p ≤ q, b q) * b p ^ 2 < D ∧ D ≤ (∏ q ∈ s with p ≤ q, c q) * c p ^ 2)

The crossing is an actual full-product or inclusive cubic-prefix crossing. Equality belongs to the failed (upper-endpoint) side.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.ordinaryRoughSet_eq_support (upper : Bool) (D : ℝ) (s : Finset ℕ) : ordinaryRoughSet upper D s = if RoundedSupport upper (fun (p : ℕ) => ↑p) D s then if Even s.card then 1 else -1 else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedSignedSet_eq_ordinaryRoughSet_of_good {upper : Bool} {b c : ℕ → ℝ} {D : ℝ} {s : Finset ℕ} (hb : ∀ p ∈ s, 0 ≤ b p) (hbp : ∀ p ∈ s, b p ≤ ↑p) (hpc : ∀ p ∈ s, ↑p ≤ c p) (hcollision : ¬RoughCollision b s) (hboundary : ¬RoughBoundaryCrossing upper b c D s) : normalizedSignedSet upper b c D s = ordinaryRoughSet upper D s

Away from the two concrete bad sets the exact signed coefficients agree.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedSignedSet_abs_sub_le_one (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (s : Finset ℕ) : |normalizedSignedSet upper b c D s - ordinaryRoughSet upper D s| ≤ 1

Both coefficients are either zero or the SAME parity sign. No enclosure assumptions are needed for the bound one.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedSignedSet_directed_nonneg {upper : Bool} {b c : ℕ → ℝ} {D : ℝ} {s : Finset ℕ} (hb : ∀ p ∈ s, 0 ≤ b p) (hbp : ∀ p ∈ s, b p ≤ ↑p) (hpc : ∀ p ∈ s, ↑p ≤ c p) : 0 ≤ (if upper = true then 1 else -1) * (normalizedSignedSet upper b c D s - ordinaryRoughSet upper D s)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedSignedSet_abs_sub_le_bad {upper : Bool} {b c : ℕ → ℝ} {D : ℝ} {s : Finset ℕ} (hb : ∀ p ∈ s, 0 ≤ b p) (hbp : ∀ p ∈ s, b p ≤ ↑p) (hpc : ∀ p ∈ s, ↑p ≤ c p) : |normalizedSignedSet upper b c D s - ordinaryRoughSet upper D s| ≤ (if RoughCollision b s then 1 else 0) + if RoughBoundaryCrossing upper b c D s then 1 else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughSignedDensity_comparison (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (R : Finset ℕ) (g : ℕ → ℝ) (hb : ∀ p ∈ R, 0 ≤ b p) (hbp : ∀ p ∈ R, b p ≤ ↑p) (hpc : ∀ p ∈ R, ↑p ≤ c p) (hg : ∀ p ∈ R, 0 ≤ g p) : 0 ≤ (if upper = true then 1 else -1) * (roughSignedDensity upper b c D R g - roughOrdinaryDensity upper D R g) ∧ (if upper = true then 1 else -1) * (roughSignedDensity upper b c D R g - roughOrdinaryDensity upper D R g) ≤ roughCollisionMass b R g + roughBoundaryMass upper b c D R g

Quantitative comparison to the SAME ordinary coarse density: only collisions and strict boundary crossings pay for the directed gap.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughSignedDensity_abs_sub_le (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (R : Finset ℕ) (g : ℕ → ℝ) (hb : ∀ p ∈ R, 0 ≤ b p) (hbp : ∀ p ∈ R, b p ≤ ↑p) (hpc : ∀ p ∈ R, ↑p ≤ c p) (hg : ∀ p ∈ R, 0 ≤ g p) : |roughSignedDensity upper b c D R g - roughOrdinaryDensity upper D R g| ≤ roughCollisionMass b R g + roughBoundaryMass upper b c D R g

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.sum_powerset_superset_prod (R A : Finset ℕ) (hA : A ⊆ R) (g : ℕ → ℝ) : ∑ s ∈ R.powerset with A ⊆ s, ∏ p ∈ s, g p = (∏ p ∈ A, g p) * ∏ p ∈ R \ A, (1 + g p)

Removing a compulsory subset leaves freely chosen complementary slots.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.sum_powerset_contains_pair_prod (R : Finset ℕ) (g : ℕ → ℝ) {p q : ℕ} (hp : p ∈ R) (hq : q ∈ R) (hpq : p ≠ q) : ∑ s ∈ R.powerset with p ∈ s ∧ q ∈ s, ∏ r ∈ s, g r = g p * g q * ∏ r ∈ R \ {p, q}, (1 + g r)

Exact pair-containing powerset mass, with no division and no positivity assumptions; zero prime densities are allowed.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughCollision_iff_exists_pair (b : ℕ → ℝ) (s : Finset ℕ) : RoughCollision b s ↔ ∃ p ∈ s, ∃ q ∈ s, p < q ∧ b p = b q

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.roughCollisionPairMass (b : ℕ → ℝ) (R : Finset ℕ) (g : ℕ → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.roughCollisionPairMass b R g = ∑ p ∈ R, ∑ q ∈ R with p < q ∧ b p = b q, g p * g q

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughCollisionMass_le_pair_euler (b : ℕ → ℝ) (R : Finset ℕ) (g : ℕ → ℝ) (hg : ∀ p ∈ R, 0 ≤ g p) : roughCollisionMass b R g ≤ (∏ p ∈ R, (1 + g p)) * roughCollisionPairMass b R g

A weighted union bound over distinct same-box pairs. This retains the quadratic pair factor rather than bounding by a powerset cardinality.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughSignedDensity_comparison_pair_bound (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (R : Finset ℕ) (g : ℕ → ℝ) (hb : ∀ p ∈ R, 0 ≤ b p) (hbp : ∀ p ∈ R, b p ≤ ↑p) (hpc : ∀ p ∈ R, ↑p ≤ c p) (hg : ∀ p ∈ R, 0 ≤ g p) : 0 ≤ (if upper = true then 1 else -1) * (roughSignedDensity upper b c D R g - roughOrdinaryDensity upper D R g) ∧ (if upper = true then 1 else -1) * (roughSignedDensity upper b c D R g - roughOrdinaryDensity upper D R g) ≤ (∏ p ∈ R, (1 + g p)) * roughCollisionPairMass b R g + roughBoundaryMass upper b c D R g

The remaining finite error consists of a same-box pair mass times the rough Euler product and the strict boundary mass.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughSignedDensity_canonical_comparison (upper : Bool) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε : ℝ} (hD : 1 < D) (hε : 0 < ε) (g : ℕ → ℝ) (hg : ∀ p ∈ P \ geometricSmallPrimes P D ε, 0 ≤ g p) : have R := P \ geometricSmallPrimes P D ε; have b := fun (p : ℕ) => geometricLower D ε (ε ^ 9) (geometricSieveLabel D ε p); have c := fun (p : ℕ) => b p ^ (1 + ε ^ 9); 0 ≤ (if upper = true then 1 else -1) * (roughSignedDensity upper b c D R g - roughOrdinaryDensity upper D R g) ∧ (if upper = true then 1 else -1) * (roughSignedDensity upper b c D R g - roughOrdinaryDensity upper D R g) ≤ roughCollisionMass b R g + roughBoundaryMass upper b c D R g

Canonical geometric endpoints discharge the enclosure assumptions at the original D and epsilon; no new coarse level or box family is chosen.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughSignedDensity_canonical_pair_bound (upper : Bool) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε : ℝ} (hD : 1 < D) (hε : 0 < ε) (g : ℕ → ℝ) (hg : ∀ p ∈ P \ geometricSmallPrimes P D ε, 0 ≤ g p) : have R := P \ geometricSmallPrimes P D ε; have b := fun (p : ℕ) => geometricLower D ε (ε ^ 9) (geometricSieveLabel D ε p); have c := fun (p : ℕ) => b p ^ (1 + ε ^ 9); 0 ≤ (if upper = true then 1 else -1) * (roughSignedDensity upper b c D R g - roughOrdinaryDensity upper D R g) ∧ (if upper = true then 1 else -1) * (roughSignedDensity upper b c D R g - roughOrdinaryDensity upper D R g) ≤ (∏ p ∈ R, (1 + g p)) * roughCollisionPairMass b R g + roughBoundaryMass upper b c D R g