theorem MathlibNt.SieveTheory.LiLiuPrereqWF.G9ExtendedUpper.exists_signedFamilyDensity_upper_extended : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 / 8 → ∃ (D₀ : ℝ), 4 ≤ D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p) → ∀ (ω : ArithmeticFunction ℝ), ω.IsMultiplicative → (∀ p ∈ P, 0 ≤ ω p / ↑p ∧ ω p / ↑p < 1) → ∀ (K : ℝ), 0 ≤ K → SmallRosser.DimensionOneProductBound P (⇑(SmallRosser.primeDensity ω)) K → ∀ (z : ℝ), √D < z → z ≤ (D ^ (1 + ε + ε ^ 9)) ^ 2 → (∀ p ∈ P, ↑p < z) → signedFamilyDensity true ({p ∈ P | ↑p < √D}) D ε (geometricSieveLabel D ε) (SmallRosser.primeDensity ω) ≤ (∏ p ∈ P, (1 - ω p / ↑p)) * (JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log (D ^ (1 + ε + ε ^ 9)) / Real.log z) + C * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log D ^ (-(1 / 3))))

The absolute constant is chosen before epsilon; the threshold precedes the prime carrier, multiplicative density, original dimension constant and external cutoff. The weights are exactly the already accepted family.