Global bounds for the actual smooth U and V error terms

These bounds apply to arbitrary signed coefficients of fixed divisor order, arbitrary subsets of the real-endpoint supports, and every integer residue. No well-factorability, squarefree support, or error estimate is assumed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.card_divisors_mul_le (q r : ℕ) : (q * r).divisors.card ≤ q.divisors.card * r.divisors.card

Submultiplicativity of the ordinary divisor count, without coprimality.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_le_fouvryTau_mean {k : ℕ} (hk : 1 ≤ k) {T : ℝ} (hT : 1 ≤ T) (N : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (β : ℕ → ℝ) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) : ∑ n ∈ N, |β n| ≤ T * (1 + Real.log T) ^ (k - 1)

A signed fixed-order sequence has the elementary global absolute mean.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimeMass_abs_le_sum_abs (N : Finset ℕ) (β : ℕ → ℝ) (q : ℕ) : |coprimeMass N β q| ≤ ∑ n ∈ N, |β n|

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimeMass_of_abs_le_sum_abs (N : Finset ℕ) (β : ℕ → ℝ) (q : ℕ) : coprimeMass N (fun (n : ℕ) => |β n|) q ≤ ∑ n ∈ N, |β n|

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_reduced_abs_mul_card_divisors_div_totient_le (j : ℕ) {L : ℝ} (hL : 1 ≤ L) (Q : Finset ℕ) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (c : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) : ∑ q ∈ reducedModuli Q a, |c q| * ↑q.divisors.card / ↑q.totient ≤ (1 + Real.log L) ^ (4 * j)

The exact modulus weight appearing after divisor-count submultiplicativity has a global logarithmic mean, uniform in the changing residue.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothUErrorEnvelope_le_fouvryTau {k : ℕ} (hk : 1 ≤ k) (j : ℕ) {T L : ℝ} (hT : 1 ≤ T) (hL : 1 ≤ L) (N Q : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (β c : ℕ → ℝ) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) : smoothUErrorEnvelope N Q β c a ≤ (T * (1 + Real.log T) ^ (k - 1)) ^ 2 * (1 + Real.log L) ^ (8 * j)

The actual U envelope has only logarithmic dependence on the modulus endpoint, and retains arbitrary fixed beta and modulus divisor orders.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothVErrorEnvelope_le_fouvryTau {k j : ℕ} (hk : 1 ≤ k) (hj : 1 ≤ j) {T L : ℝ} (hT : 1 ≤ T) (hL : 1 ≤ L) (N Q : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (β c : ℕ → ℝ) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) : smoothVErrorEnvelope N Q β c a ≤ (T * (1 + Real.log T) ^ (k - 1)) ^ 2 * L * (1 + Real.log L) ^ (5 * j - 1)

The actual V envelope costs one power of the modulus endpoint, not two.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionU_smooth_fouvryTau_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (S : Finset ℕ), (∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ S) → ∀ (k : ℕ), 1 ≤ k → ∀ (j : ℕ) (T L : ℝ), 1 ≤ T → 1 ≤ L → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (β c : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), |dispersionU S N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - smoothUMain M N Q β c a| ≤ C * ((T * (1 + Real.log T) ^ (k - 1)) ^ 2 * (1 + Real.log L) ^ (8 * j))

A global bound for the signed U error itself, with a constant chosen before all changing arithmetic data and both fixed divisor orders.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionV_smooth_fouvryTau_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (S : Finset ℕ), (∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ S) → ∀ (k j : ℕ), 1 ≤ k → 1 ≤ j → ∀ (T L : ℝ), 1 ≤ T → 1 ≤ L → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (β c : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), |dispersionV S N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - smoothUMain M N Q β c a| ≤ C * ((T * (1 + Real.log T) ^ (k - 1)) ^ 2 * L * (1 + Real.log L) ^ (5 * j - 1))

A global bound for the signed V error itself; no error-envelope premise is left to the consumer.