Uniform scalar payment for the three actual normalized monomials. This module selects no analytic hypotheses and does not assert C.2.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_direct_zero_monomial {x ν ε L : ℝ} (hx : 1 ≤ x) (hε : 0 ≤ ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10) (hL : L ≤ ε / 4) : x ^ L * (x ^ c2RExponent ν ε * √(x ^ c2SExponent ν ε) / √x) ≤ x ^ (-(ε / 2))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_direct_main_monomial {x ν ε L : ℝ} (hx : 1 ≤ x) (hε : 0 ≤ ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10) (hL : L ≤ ε / 4) : x ^ L * ((x ^ ν) ^ (5 / 4) * (x ^ c2RExponent ν ε) ^ (7 / 4) * (x ^ c2SExponent ν ε) ^ 2 / x) ≤ x ^ (-(ε / 2))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_direct_secondary_monomial {x ν ε L : ℝ} (hx : 1 ≤ x) (hε : 0 ≤ ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10) (hL : L ≤ ε / 4) : x ^ L * (x ^ ν * (x ^ c2RExponent ν ε) ^ (3 / 4) * (x ^ c2SExponent ν ε) ^ (3 / 2) / √x) ≤ x ^ (-(ε / 2))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_direct_common_exponent {ε : ℝ} (hε : 0 < ε) : ∃ (η : ℝ), 0 < η ∧ η ≤ 1 ∧ η < ε ∧ 416 * η ≤ ε / 4

One internal exponent is fixed before all varying data. It simultaneously pays the four arithmetic exponents and the remaining analytic losses.