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_extended_zero_monomial {x ν ε L : ℝ} (hx : 1 ≤ x) (hε : 0 < ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10 + ε / 10) (hL : L ≤ ε / 4) : x ^ L * (x ^ c2RExponent ν ε * √(x ^ c2SExponent ν ε) / √x) ≤ x ^ (-(ε / 2))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_extended_main_monomial {x ν ε L : ℝ} (hx : 1 ≤ x) (hε : 0 < ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10 + ε / 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_extended_secondary_monomial {x ν ε L : ℝ} (hx : 1 ≤ x) (hε : 0 < ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10 + ε / 10) (hL : L ≤ ε / 4) : x ^ L * (x ^ ν * (x ^ c2RExponent ν ε) ^ (3 / 4) * (x ^ c2SExponent ν ε) ^ (3 / 2) / √x) ≤ x ^ (-(ε / 2))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_extended_factor_levels {x ν ε : ℝ} (hx : 1 ≤ x) (hε : 0 < ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10 + ε / 10) : have R := x ^ c2RExponent ν ε; have S := x ^ c2SExponent ν ε; 1 ≤ R ∧ 1 ≤ S ∧ R * S = x ^ ((5 - 5 * ν) / 9 - ε) ∧ max (R ^ 2 * S) ((x ^ ν) ^ (5 / 4) * R ^ (7 / 4) * S ^ 2) ≤ x ^ (1 - 3 * ε / 2)