theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable.factorSupported {j : ℕ} {L : ℝ} {c : ℕ → ℝ} (hc : SignedWellFactorable j L c) (hL : 1 ≤ L) : LiLiuPrereqFouvry.factorSupported L c

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_level_eq_of_support {L L' : ℝ} (hLL' : L ≤ L') (U V : Finset ℕ) (α β c : ℕ → ℝ) (a : ℤ) (hc : factorSupported L c) : signedError U V (Finset.Ioc 0 ⌊L⌋₊) α β c a = signedError U V (Finset.Ioc 0 ⌊L'⌋₊) α β c a

Enlarging only the summation interval leaves the same supported weight unchanged. This is not closure of well-factorability under masking.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_levels_eq_of_support {L L' : ℝ} (U V : Finset ℕ) (α β c : ℕ → ℝ) (a : ℤ) (hc : factorSupported L c) (hc' : factorSupported L' c) : signedError U V (Finset.Ioc 0 ⌊L⌋₊) α β c a = signedError U V (Finset.Ioc 0 ⌊L'⌋₊) α β c a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9Scale_global_level_ge_one {N T δ : ℝ} (hN : 1 ≤ N) (hT : 1 ≤ T) (hTN : T ≤ N ^ (1 / 10)) (hδ : δ ≤ 1 / 2) : 1 ≤ N ^ (5 / 9 - δ) / T ^ (5 / 9)

The global level is genuinely at least one in the G9 range.