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

Upper bound for the actual, unchanged external family on 2 ≤ z ≤ Q². The fixed constant precedes epsilon, and the threshold precedes all density, carrier, cutoff and dimension data. No lower bound is asserted.