Arithmetic Poisson summation for the fixed dyadic cutoff

The finite natural progression is identified with the entire affine integer lattice using the positive support of the cutoff. The error constant is chosen before the scale, modulus, residue, and finite support set.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffNatSupport (M : ℝ) : Finset ℕ

One explicit finite set containing every natural point of the cutoff support.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffNatSupport M = Finset.Icc 0 ⌈3 * M⌉₊

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_mem_Icc_of_ne_zero {M x : ℝ} (hM : 0 < M) (hx : scaledDyadicCutoff M x ≠ 0) : x ∈ Set.Icc (M / 2) (3 * M)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_mem_natSupport {M : ℝ} (hM : 0 < M) (m : ℕ) (hm : scaledDyadicCutoff M ↑m ≠ 0) : m ∈ dyadicCutoffNatSupport M

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_finset_progression_eq_tsum {M : ℝ} (hM : 0 < M) (S : Finset ℕ) (hS : ∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ S) {q : ℕ} (hq : 0 < q) (a : ℤ) : (∑ m ∈ S, if ↑m ≡ a [ZMOD ↑q] then ↑(scaledDyadicCutoff M ↑m) else 0) = ∑' (z : ℤ), ↑(scaledDyadicCutoff M (↑a + ↑q * ↑z))

The actual finite natural arithmetic progression equals the complete affine integer lattice, even for negative representatives of the residue class.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_progression_eq_tsum {M : ℝ} (hM : 0 < M) {q : ℕ} (hq : 0 < q) (a : ℤ) : (∑ m ∈ dyadicCutoffNatSupport M, if ↑m ≡ a [ZMOD ↑q] then ↑(scaledDyadicCutoff M ↑m) else 0) = ∑' (z : ℤ), ↑(scaledDyadicCutoff M (↑a + ↑q * ↑z))

Canonical finite-support specialization of the arithmetic lattice bridge.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffMass : ℝ

The real zero-frequency mass of the fixed, scale-independent cutoff.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffMass = ((FourierTransform.fourier MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffSchwartz) 0).re

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_finset_progression_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (S : Finset ℕ), (∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ S) → ∀ (q : ℕ), 0 < q → ∀ (a : ℤ), |(∑ m ∈ S, if ↑m ≡ a [ZMOD ↑q] then scaledDyadicCutoff M ↑m else 0) - M / ↑q * dyadicCutoffMass| ≤ C

Uniform arithmetic progression error for every support-containing finite set.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_finset_multiples_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (S : Finset ℕ), (∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ S) → ∀ (d : ℕ), 0 < d → |(∑ m ∈ S, if d ∣ m then scaledDyadicCutoff M ↑m else 0) - M / ↑d * dyadicCutoffMass| ≤ C

The same constant bounds each sum over multiples, with no scale restriction.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_finset_coprime_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (S : Finset ℕ), (∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ S) → ∀ (q : ℕ), q ≠ 0 → |(∑ m ∈ S, if m.Coprime q then scaledDyadicCutoff M ↑m else 0) - M * dyadicCutoffMass * ↑q.totient / ↑q| ≤ C * ↑q.divisors.card

Smooth coprime counting, obtained from the already proved finite Mobius identity and density. The universal error is at most C times the divisor count.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_progression_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (q : ℕ), 0 < q → ∀ (a : ℤ), |(∑ m ∈ dyadicCutoffNatSupport M, if ↑m ≡ a [ZMOD ↑q] then scaledDyadicCutoff M ↑m else 0) - M / ↑q * dyadicCutoffMass| ≤ C

The canonical finite arithmetic progression has a universal O(1) error.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_coprime_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (q : ℕ), q ≠ 0 → |(∑ m ∈ dyadicCutoffNatSupport M, if m.Coprime q then scaledDyadicCutoff M ↑m else 0) - M * dyadicCutoffMass * ↑q.totient / ↑q| ≤ C * ↑q.divisors.card

The canonical finite coprime sum supplies the smooth U counting estimate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.exists_progression_for_divisor_congruence {q d n : ℕ} (hd : d.Coprime q) (hn : n.Coprime q) (a : ℤ) : ∃ (b : ℤ), ∀ (m : ℕ), d ∣ m ∧ ↑m * ↑n ≡ a [ZMOD ↑q] ↔ ↑m ≡ b [ZMOD ↑(q * d)]

Bezout inverses and the Chinese remainder theorem combine the divisibility condition and the product congruence into one actual residue class.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_finset_divisor_progression_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (S : Finset ℕ), (∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ S) → ∀ (q d n : ℕ), 0 < q → 0 < d → d.Coprime q → n.Coprime q → ∀ (a : ℤ), |(∑ m ∈ S, if d ∣ m ∧ ↑m * ↑n ≡ a [ZMOD ↑q] then scaledDyadicCutoff M ↑m else 0) - M * dyadicCutoffMass / ↑q / ↑d| ≤ C

A mixed divisibility/congruence sum is estimated using its constructed residue class modulo q * d, not an assumed progression-count formula.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprime_product_progression_weight_eq_moebius (S : Finset ℕ) (w : ℕ → ℝ) {q r n : ℕ} (hr : r ≠ 0) {a : ℤ} (ha : a.gcd ↑q = 1) : (∑ m ∈ S, if m.Coprime r ∧ ↑m * ↑n ≡ a [ZMOD ↑q] then w m else 0) = ∑ d ∈ r.divisors with d.Coprime q, ↑(ArithmeticFunction.moebius d) * ∑ m ∈ S, if d ∣ m ∧ ↑m * ↑n ≡ a [ZMOD ↑q] then w m else 0

Finite Mobius inversion for the mixed term. Divisors sharing a factor with q cannot occur because the product is congruent to a reduced residue.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_finset_coprime_progression_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (S : Finset ℕ), (∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ S) → ∀ (q r n : ℕ), 0 < q → r ≠ 0 → n.Coprime q → ∀ (a : ℤ), a.gcd ↑q = 1 → |(∑ m ∈ S, if m.Coprime r ∧ ↑m * ↑n ≡ a [ZMOD ↑q] then scaledDyadicCutoff M ↑m else 0) - M * dyadicCutoffMass / ↑q * ∑ d ∈ r.divisors with d.Coprime q, ↑(ArithmeticFunction.moebius d) / ↑d| ≤ C * ↑r.divisors.card

The smooth arithmetic V estimate, uniformly in the scale, both moduli, the reduced residue, the invertible multiplier, and the finite support set.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_coprime_progression_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (q r n : ℕ), 0 < q → r ≠ 0 → n.Coprime q → ∀ (a : ℤ), a.gcd ↑q = 1 → |(∑ m ∈ dyadicCutoffNatSupport M, if m.Coprime r ∧ ↑m * ↑n ≡ a [ZMOD ↑q] then scaledDyadicCutoff M ↑m else 0) - M * dyadicCutoffMass / ↑q * ∑ d ∈ r.divisors with d.Coprime q, ↑(ArithmeticFunction.moebius d) / ↑d| ≤ C * ↑r.divisors.card

Canonical finite-support version of the arithmetic V estimate.