theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePairBound_extended_le {x ν ε : ℝ} (hx : 4 ≤ x) (hε : 0 < ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10 + ε / 10) {N : Finset ℕ} (hN : ∀ n ∈ N, ↑n ≤ 2 * x ^ ν) : ↑(wCoprimePairBound N (x ^ c2SExponent ν ε)) ≤ x