theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_floor_log_comparison {x : ℝ} (hx : 3 ≤ x) : 0 < Real.log ↑⌊x⌋₊ ∧ Real.log x ≤ 2 * Real.log ↑⌊x⌋₊

The real upper endpoint and its natural floor have comparable logarithms.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_interval_card_bound {T u v : ℝ} (hT : 1 ≤ T) (hv : v ≤ 2 * T) {d : ℕ} (hd : 0 < d) (h b : ℕ) : |betaCoprimeAPDiscrepancy (primeSWInterval u v) primeSWBeta d h b| ≤ 4 * T

A simple global interval bound, with no lower-endpoint prime-density input.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_uniform_real (B : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (T u v : ℝ), 1 ≤ T → T ≤ u → u ≤ v → v ≤ 2 * T → ∀ (d h : ℕ), 0 < d → 0 < h → ∀ (b : ℕ), b.Coprime d → |betaCoprimeAPDiscrepancy (primeSWInterval u v) primeSWBeta d h b| ≤ C * T * ↑((fouvryTau 2) h) / Real.log (2 * T) ^ B

All real dyadic prime intervals satisfy the independently sieved SW estimate. The saving constant is selected before the scale, both endpoints, and all arithmetic data.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_BetaCoprimeSWFamily {ι : Type u_1} (T u v : ι → ℝ) (hT : ∀ (i : ι), 1 ≤ T i) (hTu : ∀ (i : ι), T i ≤ u i) (huv : ∀ (i : ι), u i ≤ v i) (hv : ∀ (i : ι), v i ≤ 2 * T i) : BetaCoprimeSWFamily 2 T (fun (i : ι) => primeSWInterval (u i) (v i)) fun (x : ι) => primeSWBeta

The concrete prime-interval family, with fixed divisor order two.