theorem G11FiniteGate.progressionEuler_rough_le (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p ∧ 2 < p) {v K : ℕ} {L : ℝ} (hv : 0 < v) (hL : 4 ≤ L) (hrough : ∀ p ∈ v.primeFactors, L ≤ ↑p) (hK : v.primeFactors.card ≤ K) : ∏ p ∈ P, (1 - (MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity v) p) ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.g9BaseEuler P * (1 + 1 / (L - 2)) ^ K

A product-dependent progression Euler factor costs one payment for each DISTINCT prime divisor. Repeated factors are allowed and no gate is discarded.

theorem G11FiniteGate.weighted_progressionEuler_rough_le {ι : Type u_1} (I : Finset ι) (a : ι → ℕ) (w : ι → ℝ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p ∧ 2 < p) {L : ℝ} {K : ℕ} (hL : 4 ≤ L) (hw : ∀ i ∈ I, 0 ≤ w i) (ha : ∀ i ∈ I, w i ≠ 0 → 0 < a i ∧ (∀ p ∈ (a i).primeFactors, L ≤ ↑p) ∧ (a i).primeFactors.card ≤ K) : ∑ i ∈ I, w i * ∏ p ∈ P, (1 - (MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity (a i)) p) ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.g9BaseEuler P * (1 + 1 / (L - 2)) ^ K * ∑ i ∈ I, w i

Finite nonnegative transfer of the preceding exact Euler correction.