Uniform Siegel--Walfisz transport under divisor deletion

Every constant is chosen before the original family index, residue and scale. The extra divisor order absorbs the deleted mass even when the original sieve order is zero. The logarithmic payment holds at every scale at least one.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaCoprimeAPDiscrepancy_add (N : Finset ℕ) (β γ : ℕ → ℝ) (d h b : ℕ) : betaCoprimeAPDiscrepancy N (fun (n : ℕ) => β n + γ n) d h b = betaCoprimeAPDiscrepancy N β d h b + betaCoprimeAPDiscrepancy N γ d h b

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

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_AP_abs_le (N : Finset ℕ) (β : ℕ → ℝ) (a : ℤ) {d : ℕ} (hd : 0 < d) (h b : ℕ) : |betaCoprimeAPDiscrepancy N (betaClean β a) d h b| ≤ |betaCoprimeAPDiscrepancy N β d h b| + 2 * ∑ n ∈ N, |betaDivisorPart β a n|

Deleting beta on divisors changes any coprime-sieved AP discrepancy by at most twice the actual deleted mass.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_log_pow_le_const_rpow (B : ℕ) {θ : ℝ} (hθ : 0 < θ) : ∃ (L : ℝ), 0 < L ∧ ∀ (T : ℝ), 1 ≤ T → Real.log (2 * T) ^ B ≤ L * T ^ θ

A uniform elementary log-versus-power bound, including the compact range 1 ≤ T and the saving order B = 0.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_betaDivisorPart_uniform_log_payment (k B : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (x T : ℝ), 1 ≤ x → 1 ≤ T → x ^ ε ≤ T → ∀ (a : ℤ), a ≠ 0 → ↑a.natAbs ≤ x → ∀ (N : Finset ℕ) (β : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → ∑ n ∈ N, |betaDivisorPart β a n| ≤ C * T / Real.log (2 * T) ^ B

Divisor deletion is uniformly cheaper than every SW logarithmic error at T ≥ x^ε; neither T ≤ x nor interval support is needed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.BetaCoprimeSWFamily.betaClean_uniform {ι : Type u_1} {κ k : ℕ} {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hβ : ∀ (i : ι), ∀ n ∈ N i, |β i n| ≤ ↑((fouvryTau k) n)) {ε : ℝ} (hε : 0 < ε) (B : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (i : ι), 1 ≤ T i → ∀ (x : ℝ), 1 ≤ x → x ^ ε ≤ T i → ∀ (a : ℤ), a ≠ 0 → ↑a.natAbs ≤ x → ∀ (d h : ℕ), 0 < d → 0 < h → ∀ (b : ℕ), b.Coprime d → |betaCoprimeAPDiscrepancy (N i) (LiLiuPrereqFouvry.betaClean (β i) a) d h b| ≤ C * T i * ↑((fouvryTau (κ + 1)) h) / Real.log (2 * T i) ^ B

Uniform transport with all changing arithmetic data after the constant. The original coefficient order k and SW sieve order κ are independent.

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

The family really contains all admissible old indices, residues and scales, not only a fixed residue chosen before the SW constants.

• index : ι
• residue : ℤ
• scale : ℝ
• one_le_T : 1 ≤ T self.index
• one_le_scale : 1 ≤ self.scale
• residue_ne_zero : self.residue ≠ 0
• residue_le_scale : ↑self.residue.natAbs ≤ self.scale
• scale_rpow_le : self.scale ^ ε ≤ T self.index

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.BetaCoprimeSWFamily.betaClean {ι : Type u_1} {κ k : ℕ} {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hβ : ∀ (i : ι), ∀ n ∈ N i, |β i n| ≤ ↑((fouvryTau k) n)) {ε : ℝ} (hε : 0 < ε) : BetaCoprimeSWFamily (κ + 1) (fun (j : BetaCleanIndex T ε) => T j.index) (fun (j : BetaCleanIndex T ε) => N j.index) fun (j : BetaCleanIndex T ε) => LiLiuPrereqFouvry.betaClean (β j.index) j.residue