A uniform elementary main-term estimate for hard cutoffs

Mobius inversion and the error in counting multiples give the coprime prefix count with error at most the number of divisors of the modulus. This supplies an actual U main-term estimate for a hard cutoff. It does not supply the smooth Poisson estimates needed later for V and W.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePrefix (H q : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePrefix H q = ∑ m ∈ Finset.Ioc 0 H, if m.Coprime q then 1 else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePrefix_eq_divisor_sum (H : ℕ) {q : ℕ} (hq : q ≠ 0) : coprimePrefix H q = ∑ d ∈ q.divisors, ↑(ArithmeticFunction.moebius d) * ↑(H / d)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePrefix_period (q : ℕ) : coprimePrefix q q = ↑q.totient

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.moebius_density {q : ℕ} (hq : q ≠ 0) : ∑ d ∈ q.divisors, ↑(ArithmeticFunction.moebius d) / ↑d = ↑q.totient / ↑q

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.nat_div_error_le_one (H : ℕ) {d : ℕ} (hd : 0 < d) : |↑(H / d) - ↑H / ↑d| ≤ 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePrefix_error (H : ℕ) {q : ℕ} (hq : q ≠ 0) : |coprimePrefix H q - ↑H * (↑q.totient / ↑q)| ≤ ↑q.divisors.card

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

Equations

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

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

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.hardCutoffUMain H 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 * (↑H * ↑(q * r).totient / ↑(q * r))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionU_hardCutoff_error (H : ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hQ : ∀ q ∈ Q, q ≠ 0) : |dispersionU (Finset.Ioc 0 H) N Q (fun (x : ℕ) => 1) β c a - hardCutoffUMain H N Q β c a| ≤ ∑ q ∈ reducedModuli Q a, ∑ r ∈ reducedModuli Q a, |uModulusCoefficient N β c q r| * ↑(q * r).divisors.card