Admissible C.2 factor levels, including the endpoint

In the interior these are the exponents printed in Fouvry (1987), p. 620. When the printed S exponent is negative, set S = 1 and transfer its exponent to R, keeping the original level exactly. This is only a parameter lemma: it does not assert any distribution estimate or a dyadic decomposition.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2SExponent (ν ε : ℝ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2SExponent ν ε = max 0 ((1 - 10 * ν) / 9 - ε / 2)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2RExponent (ν ε : ℝ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2RExponent ν ε = (5 - 5 * ν) / 9 - ε - MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2SExponent ν ε

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_exponent_bounds {ν ε : ℝ} (hε : 0 ≤ ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10) : 0 ≤ c2RExponent ν ε ∧ 0 ≤ c2SExponent ν ε ∧ c2RExponent ν ε + c2SExponent ν ε = (5 - 5 * ν) / 9 - ε ∧ 2 * c2RExponent ν ε + c2SExponent ν ε ≤ 1 - 3 * ε / 2 ∧ 5 * ν / 4 + 7 * c2RExponent ν ε / 4 + 2 * c2SExponent ν ε ≤ 1 - 3 * ε / 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2SExponent_eq_zero_near_endpoint {ν ε : ℝ} (h : (1 - 10 * ν) / 9 ≤ ε / 2) : c2SExponent ν ε = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2SExponent_endpoint {ε : ℝ} (hε : 0 ≤ ε) : c2SExponent (1 / 10) ε = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_factor_levels {x ν ε : ℝ} (hx : 1 ≤ x) (hε : 0 ≤ ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 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)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_S_level_endpoint (x : ℝ) {ε : ℝ} (hε : 0 ≤ ε) : x ^ c2SExponent (1 / 10) ε = 1