A small upper-end extension of the original Fouvry parameters

The definitions c2RExponent and c2SExponent are imported unchanged. Only scalar parameter inequalities are extended; no distribution theorem, coefficient estimate, G9 boundary reduction, or residue claim is made here. The old range is discharged by the existing producers whenever applicable.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_extended_parameter_caps {ν ε : ℝ} (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10 + ε / 10) : ε ≤ 1 / 9 ∧ ν ≤ 1 / 9

The new parameter range still bounds epsilon and nu by 1/9.

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

Above the old endpoint the original S exponent vanishes.

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

Nonnegative exponents, the original level identity, and both original strong inequalities hold on the slightly extended range.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_extended_secondary_exponent_margin {ν ε : ℝ} (hε : 0 < ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10 + ε / 10) : ν + 3 * c2RExponent ν ε / 4 + 3 * c2SExponent ν ε / 2 - 1 / 2 ≤ -(3 * ε / 4)

The original secondary margin survives the upper-end extension.

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

All three normalized terms admit the same original loss allowance.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_extended_short_add_S_le_half {ν ε : ℝ} (hε : 0 < ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10 + ε / 10) : ν + c2SExponent ν ε ≤ 1 / 2

The short coordinate times S remains below the square-root level.