Exact inner interval for the paid floor cutoff

The repaired cutoff has a closed ceiling lower endpoint involving |h|, not the old strict floor endpoint involving |h|-1. These identities retain the fixed gcd condition; they do not remove the other arithmetic masks.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFloorCutoff_frequency_iff {M Z : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) (q r : ℕ) (h : ℤ) : h.natAbs ≤ wFloorCutoff M Z q r ↔ ↑h.natAbs ≤ ↑(q.lcm r) / M * Z

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFloorCutoff_factor_interval_iff {M Z : ℝ} (hM : 0 < M) (hZ : 0 < Z) {q d k δ : ℕ} (hq : 0 < q) (hd : 0 < d) (hg : q.gcd (d * k) = δ) (h : ℤ) : h.natAbs ≤ wFloorCutoff M Z q (d * k) ↔ ⌈↑h.natAbs * M * ↑δ / (↑q * ↑d * Z)⌉₊ ≤ k

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFloorCutoff_factor_mem_Icc_iff {M Z : ℝ} (hM : 0 < M) (hZ : 0 < Z) {q d k δ F : ℕ} (hq : 0 < q) (hd : 0 < d) (hg : q.gcd (d * k) = δ) (h : ℤ) : k ≤ F ∧ h.natAbs ≤ wFloorCutoff M Z q (d * k) ↔ k ∈ Finset.Icc ⌈↑h.natAbs * M * ↑δ / (↑q * ↑d * Z)⌉₊ F