The same rough signed density at the normalized analytic scale

Both actual error classes are now paid. The comparison is to the very same ordinary rough Rosser coefficient, with its original level and parity.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughCollisionPairContribution_le_target (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε K : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hlarge : 1 ≤ ε ^ 2 * Real.log D) (hK : 0 ≤ K) (hcut : ∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < √D) {g : ℕ → ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) (hdim : SmallRosser.DimensionOneProductBound P g K) : have R := P \ geometricSmallPrimes P D ε; have b := fun (p : ℕ) => geometricLower D ε (ε ^ 9) (geometricSieveLabel D ε p); (∏ p ∈ R, (1 + g p)) * roughCollisionPairMass b R g ≤ (10 * ∏ p ∈ R, (1 - g p)) * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log D ^ (-(1 / 3)))

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughSignedDensity_abs_sub_le_target (upper : Bool) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε K : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hlarge : 1 ≤ ε ^ 2 * Real.log D) (hK : 0 ≤ K) (hcut : ∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < √D) {g : ℕ → ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) (hdim : SmallRosser.DimensionOneProductBound P g K) : have R := P \ geometricSmallPrimes P D ε; have b := fun (p : ℕ) => geometricLower D ε (ε ^ 9) (geometricSieveLabel D ε p); have c := fun (p : ℕ) => b p ^ (1 + ε ^ 9); |roughSignedDensity upper b c D R g - roughOrdinaryDensity upper D R g| ≤ (20 * ∏ p ∈ R, (1 - g p)) * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log D ^ (-(1 / 3)))

Both signs of the actual rough family differ from the ordinary family by at most the same Euler-normalized error.