Uniform coprime Siegel--Walfisz transport at the growing omega cutoff

The enlarged family contains every scale x >= T >= 1. The bounded-scale range is paid explicitly, so no saving-dependent lower cutoff is hidden in the index type. Coefficient order is unchanged; the SW sieve order rises by one to include order zero.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmega_uniform_bound (K : ℝ) (hK : 0 ≤ K) (B : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ), 1 ≤ x → K * 2 ^ (-highOmegaCutoff x) * (1 + Real.log (2 * x)) ^ B ≤ C

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_betaHighOmega_uniform_log_payment (k B : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x T : ℝ), 1 ≤ T → T ≤ x → ∀ N ⊆ Finset.Ioc 0 ⌊2 * T⌋₊, ∀ (β : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → ∑ n ∈ N, |betaHighOmega β (highOmegaCutoff x) n| ≤ C * T / Real.log (2 * T) ^ B

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaLowOmega_AP_abs_le (N : Finset ℕ) (β : ℕ → ℝ) (ξ : ℝ) {d : ℕ} (hd : 0 < d) (h b : ℕ) : |betaCoprimeAPDiscrepancy N (betaLowOmega β ξ) d h b| ≤ |betaCoprimeAPDiscrepancy N β d h b| + 2 * ∑ n ∈ N, |betaHighOmega β ξ n|

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.BetaCoprimeSWFamily.betaLowOmega_uniform {ι : Type u_1} {κ k : ℕ} {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (z : ι), 1 ≤ T z) (hN : ∀ (z : ι), N z ⊆ Finset.Ioc 0 ⌊2 * T z⌋₊) (hβ : ∀ (z : ι), ∀ n ∈ N z, |β z n| ≤ ↑((fouvryTau k) n)) (B : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (z : ι) (x : ℝ), T z ≤ x → ∀ (d h : ℕ), 0 < d → 0 < h → ∀ (b : ℕ), b.Coprime d → |betaCoprimeAPDiscrepancy (N z) (LiLiuPrereqFouvry.betaLowOmega (β z) (highOmegaCutoff x)) d h b| ≤ C * T z * ↑((fouvryTau (κ + 1)) h) / Real.log (2 * T z) ^ B

structure MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.BetaLowOmegaIndex {ι : Type u_1} (T : ι → ℝ) : Type u_1

• index : ι
• scale : ℝ
• T_le_scale : T self.index ≤ self.scale

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.BetaCoprimeSWFamily.betaLowOmega {ι : Type u_1} {κ k : ℕ} {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (z : ι), 1 ≤ T z) (hN : ∀ (z : ι), N z ⊆ Finset.Ioc 0 ⌊2 * T z⌋₊) (hβ : ∀ (z : ι), ∀ n ∈ N z, |β z n| ≤ ↑((fouvryTau k) n)) : BetaCoprimeSWFamily (κ + 1) (fun (z : BetaLowOmegaIndex T) => T z.index) (fun (z : BetaLowOmegaIndex T) => N z.index) fun (z : BetaLowOmegaIndex T) => LiLiuPrereqFouvry.betaLowOmega (β z.index) (highOmegaCutoff z.scale)