noncomputable def LargeSieve.primesDyadic (M : ℕ) : Finset ℕ

The set of primes in the dyadic interval [M/2, M].

def LargeSieve.fiberCard (A : Finset ℕ) (p : ℕ) (a : ZMod p) : ℕ

The cardinality of the fiber of A over a ∈ ZMod p, i.e. the number of n ∈ A with n ≡ a (mod p).

noncomputable def LargeSieve.avgDeviationMod (A : Finset ℕ) (p : ℕ) : ℝ

Average deviation from equidistribution modulo p: $\frac{1}{p} \sum_{a \in \mathbb{Z}_p} \big|\, |A \cap (a + p\mathbb{Z})| - |A|/p \,\big|$.

theorem LargeSieve.avgDeviationMod_nonneg (A : Finset ℕ) (p : ℕ) : 0 ≤ avgDeviationMod A p

The average deviation avgDeviationMod A p is non-negative.

noncomputable def LargeSieve.indicatorFin (N : ℕ) (A : Finset ℕ) : Fin N → ℂ

The indicator function 1_A : Fin N → ℂ, where index n corresponds to the integer n.val + 1 ∈ [1, N].

theorem LargeSieve.large_sieve_L2_avg_bound : ∃ C₁ > 0, ∀ (N : ℕ) (A : Finset ℕ), 1 ≤ N → A ⊆ Finset.Icc 1 N → 1 / ↑(primesDyadic N.sqrt).card * ∑ p ∈ primesDyadic N.sqrt, avgDeviationMod A p ^ 2 ≤ C₁ * Real.log ↑N ^ 2 * ↑N ^ (1 / 2)

$L^2$ version of the average large sieve bound: for A ⊆ [1, N], the average over primes p ∈ P_{N^{1/2}} of (avgDeviationMod A p)^2 is at most C₁ · (log N)^2 · N^{1/2}.

theorem LargeSieve.large_sieve_equidistribution_mod_primes : ∃ C > 0, ∀ (N : ℕ) (A : Finset ℕ), 1 ≤ N → A ⊆ Finset.Icc 1 N → 1 / ↑(primesDyadic N.sqrt).card * ∑ p ∈ primesDyadic N.sqrt, avgDeviationMod A p ≤ C * Real.log ↑N * ↑N ^ (1 / 4)

Large sieve corollary on equidistribution mod primes: if A ⊆ [N] then $$\operatorname{Avg}_{p \in P_{N^{1/2}}} \operatorname{Avg}_{a \in \mathbb{Z}_p} \big| \pi_p \mathbf{1}_A(a) - |A|/p \big| \lessapprox N^{1/4}.$$ (Obtained from large_sieve_L2_avg_bound via Cauchy–Schwarz.)