A common smooth main term for the signed U and V dispersion sums

The restricted Möbius density is evaluated by a finite prime-factor argument. Consequently the two actual dispersion sums have the same zero mode. Their errors are bounded by explicit coefficient envelopes, with constants chosen before the scale, supports, coefficients, moduli, and residue. No growth bound for those envelopes and no well-factorability hypothesis is asserted here.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.restricted_moebius_density_prod (q : ℕ) {r : ℕ} (hr : r ≠ 0) : ∑ d ∈ r.divisors with d.Coprime q, ↑(ArithmeticFunction.moebius d) / ↑d = ∏ p ∈ r.primeFactors with p.Coprime q, (1 - (↑p)⁻¹)

Only the squarefree divisors supported on primes coprime to q contribute.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.restricted_moebius_density {q r : ℕ} (hq : q ≠ 0) (hr : r ≠ 0) : (∑ d ∈ r.divisors with d.Coprime q, ↑(ArithmeticFunction.moebius d) / ↑d) / ↑q = ↑(q * r).totient / (↑q.totient * ↑(q * r))

The exact finite arithmetic identity identifying the U and V zero modes.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothUMain (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : ℝ

The common zero-frequency contribution, with all coefficient signs retained.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothUMain M N Q β c a = ∑ q ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, ∑ r ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.uModulusCoefficient N β c q r * (M * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffMass * ↑(q * r).totient / ↑(q * r))

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.vModulusCoefficient (N : Finset ℕ) (β c : ℕ → ℝ) (q r : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.vModulusCoefficient N β c q r = c q * c r / ↑r.totient * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimeMass N β r

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothVZeroMode (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : ℝ

The zero mode obtained directly from the mixed progression expansion.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothVZeroMode M N Q β c a = ∑ q ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, ∑ r ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.vModulusCoefficient N β c q r * (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimeMass N β q * (M * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffMass / ↑q * ∑ d ∈ r.divisors with d.Coprime q, ↑(ArithmeticFunction.moebius d) / ↑d))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothVZeroMode_eq_smoothUMain (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hQ : ∀ q ∈ Q, q ≠ 0) : smoothVZeroMode M N Q β c a = smoothUMain M N Q β c a

Equality of the actual U and V zero-mode formulas, not an asymptotic premise.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothUErrorEnvelope (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : ℝ

The divisor-count envelope for U; no logarithmic growth estimate is implicit.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothUErrorEnvelope N Q β c a = ∑ q ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, ∑ r ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, |MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.uModulusCoefficient N β c q r| * ↑(q * r).divisors.card

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothVErrorEnvelope (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : ℝ

The mixed envelope uses the signed r-mass in its outer coefficient and the absolute q-coprime beta mass only in the error majorant.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothVErrorEnvelope N Q β c a = ∑ q ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, ∑ r ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, |MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.vModulusCoefficient N β c q r| * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimeMass N (fun (n : ℕ) => |β n|) q * ↑r.divisors.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothUErrorEnvelope_nonneg (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : 0 ≤ smoothUErrorEnvelope N Q β c a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothVErrorEnvelope_nonneg (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : 0 ≤ smoothVErrorEnvelope N Q β c a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionU_smooth_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (S : Finset ℕ), (∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ S) → ∀ (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ), (∀ q ∈ Q, q ≠ 0) → |dispersionU S N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - smoothUMain M N Q β c a| ≤ C * smoothUErrorEnvelope N Q β c a

The actual signed U dispersion sum is approximated by the common smooth main term, uniformly before every changing scale, support, and arithmetic input.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionV_smooth_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (S : Finset ℕ), (∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ S) → ∀ (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ), (∀ q ∈ Q, q ≠ 0) → |dispersionV S N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - smoothUMain M N Q β c a| ≤ C * smoothVErrorEnvelope N Q β c a

The actual signed V dispersion sum has the same main term as U.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionUV_smooth_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (S : Finset ℕ), (∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ S) → ∀ (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ), (∀ q ∈ Q, q ≠ 0) → |dispersionU S N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - smoothUMain M N Q β c a| ≤ C * smoothUErrorEnvelope N Q β c a ∧ |dispersionV S N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - smoothUMain M N Q β c a| ≤ C * smoothVErrorEnvelope N Q β c a ∧ |dispersionV S N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - dispersionU S N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a| ≤ C * (smoothUErrorEnvelope N Q β c a + smoothVErrorEnvelope N Q β c a)

One universal constant controls U, V, and their difference; the common signed zero mode cancels exactly in the last bound.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionV_sub_U_dyadicCutoff_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ), (∀ q ∈ Q, q ≠ 0) → |dispersionV (dyadicCutoffNatSupport M) N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - dispersionU (dyadicCutoffNatSupport M) N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a| ≤ C * (smoothUErrorEnvelope N Q β c a + smoothVErrorEnvelope N Q β c a)

The canonical cutoff support removes the support-containment hypothesis.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_sq_le_dyadicCutoff_dispersion {M : ℝ} (hM : 0 < M) (A N Q : Finset ℕ) (α β c : ℕ → ℝ) (a : ℤ) (hA : ∀ m ∈ A, ↑m ∈ Set.Icc M (2 * M)) : signedError A N Q α β c a ^ 2 ≤ (∑ m ∈ A, α m ^ 2) * (dispersionW (dyadicCutoffNatSupport M) N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - 2 * dispersionV (dyadicCutoffNatSupport M) N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a + dispersionU (dyadicCutoffNatSupport M) N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a)

The constructed cutoff, rather than an assumed majorant, gives the smoothed dispersion reduction for an alpha support in [M, 2M].