Full-carrier normalization of the actual small-weight replacement

The rough Euler majorant is paid using the same dimension-one constant. The absolute constant precedes epsilon, and the threshold precedes all prime carriers, densities, depths, and signs. This does not estimate the remaining signed rough density by the linear-sieve functions.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughEulerProduct_le_normalized (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) (hcut : ∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < √D) {g : ℕ → ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) (hdim : SmallRosser.DimensionOneProductBound P g K) : ∏ p ∈ P \ geometricSmallPrimes P D ε, (1 + g p) ≤ (∏ p ∈ P \ geometricSmallPrimes P D ε, (1 - g p)) * ((1 + K / (ε ^ 2 * Real.log D)) / ε ^ 2) ^ 2

The rough product is normalized by its own Euler factor, with an explicit dimension-one loss and no threshold depending on K.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.exists_signedFamilyDensity_replacement_normalized : ∃ (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 label := geometricSieveLabel D ε; have b := fun (p : ℕ) => geometricLower D ε (ε ^ 9) (label p); have c := fun (p : ℕ) => b p ^ (1 + ε ^ 9); have V := ∏ p ∈ P, (1 - ω p / ↑p); have E := C * (Real.exp (-(1 / ε)) + Real.exp (√K - 1 / ε) * (ε * Real.log D) ^ (-(1 / 3))); have δ := signedFamilyDensity upper P D ε label (SmallRosser.primeDensity ω) - smallWeightDensity upper P D ε (SmallRosser.primeDensity ω) * roughSignedDensity upper b c D (P \ B) ⇑(SmallRosser.primeDensity ω); 1 ≤ ε ^ 2 * Real.log D ∧ 0 ≤ (if upper = true then 1 else -1) * δ ∧ |δ| ≤ 2 * V * E / ε ^ 4 * (1 + K / (ε ^ 2 * Real.log D)) ^ 2

Explicit full-V(P) bound for the replacement in the actual signed family. In particular the enlargement of the threshold is independent of the original dimension-one constant K.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roughEuler_replacement_scalar {ε L K : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hL : 0 < L) (hK : 0 ≤ K) (ht : 1 ≤ ε ^ 2 * L) : (Real.exp (-(1 / ε)) + Real.exp (√K - 1 / ε) * (ε * L) ^ (-(1 / 3))) / ε ^ 4 * (1 + K / (ε ^ 2 * L)) ^ 2 ≤ 120 * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * L ^ (-(1 / 3)))

Scalar absorption keeps the leading epsilon term independent of K. The logarithmic term, rather than the threshold, pays every rough factor.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.exists_signedFamilyDensity_replacement_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 label := geometricSieveLabel D ε; have b := fun (p : ℕ) => geometricLower D ε (ε ^ 9) (label p); have c := fun (p : ℕ) => b p ^ (1 + ε ^ 9); have V := ∏ p ∈ P, (1 - ω p / ↑p); have δ := signedFamilyDensity upper P D ε label (SmallRosser.primeDensity ω) - smallWeightDensity upper P D ε (SmallRosser.primeDensity ω) * roughSignedDensity upper b c D (P \ B) ⇑(SmallRosser.primeDensity ω); 0 ≤ (if upper = true then 1 else -1) * δ ∧ |δ| ≤ V * C * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log D ^ (-(1 / 3)))

The complete small-weight replacement cost at the target scale, for the same signed family and the original K. The remaining rough-density comparison with F and f is not asserted.