Genuine F/f density of the fixed normalized signed family

All three terms in the comparison use the same coefficients. In particular, the lower small-weight density is never assumed positive: its error is paid against the absolute rough Euler majorant before the coarse F/f inequalities are used. The original dimension-one constant and uniform threshold order are retained.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughSignedDensity_abs_le_euler (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (R : Finset ℕ) (g : ℕ → ℝ) (hg : ∀ p ∈ R, 0 ≤ g p) : |roughSignedDensity upper b c D R g| ≤ ∏ p ∈ R, (1 + g p)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.exists_signedFamilyDensity_coarse_comparison_target : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 / 8 → ∃ (D₀ : ℝ), 2 ≤ D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p) → (∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < √D) → ∀ (ω : ArithmeticFunction ℝ), ω.IsMultiplicative → (∀ p ∈ P, 0 ≤ ω p / ↑p ∧ ω p / ↑p < 1) → ∀ (K : ℝ), 0 ≤ K → SmallRosser.DimensionOneProductBound P (⇑(SmallRosser.primeDensity ω)) K → ∀ (upper : Bool), have B := geometricSmallPrimes P D ε; have g := SmallRosser.primeDensity ω; |signedFamilyDensity upper P D ε (geometricSieveLabel D ε) g - (∏ p ∈ B, (1 - g p)) * roughOrdinaryDensity upper D (P \ B) ⇑g| ≤ (∏ p ∈ P, (1 - g p)) * C * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log D ^ (-(1 / 3)))

A full-V(P) comparison with the same ordinary coarse density. The small weight, rough signed weight, and replacement remainder are not changed.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.exists_signedFamilyDensity_ff : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 / 8 → ∃ (D₀ : ℝ), 2 ≤ D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p) → ∀ (ω : ArithmeticFunction ℝ), ω.IsMultiplicative → (∀ p ∈ P, 0 ≤ ω p / ↑p ∧ ω p / ↑p < 1) → ∀ (z : ℝ), 2 ≤ z → z ≤ √D → (∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < z) → ∀ (K : ℝ), 0 ≤ K → SmallRosser.DimensionOneProductBound P (⇑(SmallRosser.primeDensity ω)) K → have V := ∏ p ∈ P, (1 - ω p / ↑p); have E := C * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log D ^ (-(1 / 3))); V * (JurkatRichert1965ChenGammaOneQOne.jr1965f (Real.log D / Real.log z) - E) ≤ signedFamilyDensity false P D ε (geometricSieveLabel D ε) (SmallRosser.primeDensity ω) ∧ signedFamilyDensity true P D ε (geometricSieveLabel D ε) (SmallRosser.primeDensity ω) ≤ V * (JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log D / Real.log z) + E)

The actual common signed family has the genuine linear-sieve densities on the internal domain 2 ≤ z ≤ sqrt D. The lower error is subtracted.