def LinnikLargeSieve.primesInRange (M : ℕ) : Finset ℕ

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

noncomputable def LinnikLargeSieve.modProjection (N p : ℕ) (f : Fin N → ℂ) (a : ZMod p) : ℂ

Mod-p projection of f : Fin N → ℂ: $(\pi_p f)(a) = \sum_{n \equiv a \pmod p} f(n)$.

noncomputable def LinnikLargeSieve.average (N : ℕ) (f : Fin N → ℂ) : ℂ

Average value of f : Fin N → ℂ: $\bar f = \tfrac{1}{N} \sum_n f(n)$.

noncomputable def LinnikLargeSieve.highFreqPart (N : ℕ) (f : Fin N → ℂ) : Fin N → ℂ

High-frequency part f_H = f - \bar f of f : Fin N → ℂ.

noncomputable def LinnikLargeSieve.l2NormSq_ZMod (p : ℕ) [NeZero p] (g : ZMod p → ℂ) : ℝ

Squared $L^2$ norm of g : ZMod p → ℂ.

noncomputable def LinnikLargeSieve.highFreqPart_ZMod (p : ℕ) [NeZero p] (g : ZMod p → ℂ) : ZMod p → ℂ

High-frequency part of g : ZMod p → ℂ: g(a) - (1/p) ∑_b g(b).

noncomputable def LinnikLargeSieve.projHighFreqL2Sq (N p : ℕ) [NeZero p] (f : Fin N → ℂ) : ℝ

Squared $L^2$ norm of the high-frequency part of the mod-p projection: ‖(π_p f)_H‖_{L^2}^2.

noncomputable def LinnikLargeSieve.linnikLHS (N M : ℕ) (f : Fin N → ℂ) : ℝ

Left-hand side of Linnik's large sieve inequality: $\sum_{p \in P_M} \|(\pi_p f)_H\|_{L^2}^2$.

noncomputable def LinnikLargeSieve.fourierZ (N : ℕ) (f : Fin N → ℂ) (ξ : ℝ) : ℂ

Fourier transform on $\mathbb{Z}$: $\hat f(\xi) = \sum_n f(n) e^{-2\pi i \xi n}$.

theorem LinnikLargeSieve.bombieri_davenport_bound (N : ℕ) (hN : 0 < N) (S : Finset ℝ) (hrange : ∀ x ∈ S, 0 ≤ x ∧ x < 1) (hsep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 / ↑N ≤ |x - y|) (f : Fin N → ℂ) : ∑ ξ ∈ S, ‖fourierZ N f ξ‖ ^ 2 ≤ (2 * ↑N - 1) * ∑ n : Fin N, ‖f n‖ ^ 2

Bombieri–Davenport form of the analytic large sieve: for any 1/N-separated set S ⊆ [0, 1), $\sum_{\xi \in S} |\hat f(\xi)|^2 \le (2N - 1) \sum_n |f(n)|^2$.

theorem LinnikLargeSieve.classical_large_sieve : ∃ C > 0, ∀ (N : ℕ), 0 < N → ∀ (S : Finset ℝ), (∀ x ∈ S, 0 ≤ x ∧ x < 1) → (∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 / ↑N ≤ |x - y|) → ∀ (f : Fin N → ℂ), ∑ ξ ∈ S, ‖fourierZ N f ξ‖ ^ 2 ≤ C * ↑N * ∑ n : Fin N, ‖f n‖ ^ 2

Classical large sieve inequality (existence form): there exists a constant C > 0 such that for any 1/N-separated S ⊆ [0, 1), $\sum_{\xi \in S} |\hat f(\xi)|^2 \le C N \sum_n |f(n)|^2$.

noncomputable def LinnikLargeSieve.fareySet (M : ℕ) : Finset ℝ

The Farey set $Q_M = \{\alpha/p : p \in P_M, 1 \le \alpha \le p - 1\}$ of reduced fractions with prime denominator in P_M.

theorem LinnikLargeSieve.fareySet_range (M : ℕ) (x : ℝ) : x ∈ fareySet M → 0 ≤ x ∧ x < 1

Every element of fareySet M lies in [0, 1).

theorem LinnikLargeSieve.fareySet_separated (M : ℕ) (x : ℝ) : x ∈ fareySet M → ∀ y ∈ fareySet M, x ≠ y → 1 / ↑M ^ 2 ≤ |x - y|

Separation property of the Farey set: any two distinct $\alpha_1/p_1, \alpha_2/p_2 \in Q_M$ satisfy $|\alpha_1/p_1 - \alpha_2/p_2| \ge 1/M^2$.

theorem LinnikLargeSieve.projHighFreq_le_farey_term (N M p : ℕ) [NeZero p] (hp : Nat.Prime p) (hpM : p ∈ primesInRange M) (hM : 0 < M) (f : Fin N → ℂ) : projHighFreqL2Sq N p f ≤ 2 / ↑M * ∑ α ∈ Finset.Icc 1 (p - 1), ‖fourierZ N (highFreqPart N f) (↑α / ↑p)‖ ^ 2

Per-prime bound expressing $\|(\pi_p f)_H\|_{L^2}^2$ via Fourier coefficients of f_H at fractions α/p for $\alpha = 1, \ldots, p - 1$.

theorem LinnikLargeSieve.fareySet_pairwiseDisjoint (M : ℕ) : (↑(primesInRange M)).PairwiseDisjoint fun (p : ℕ) => Finset.image (fun (α : ℕ) => ↑α / ↑p) (Finset.Icc 1 (p - 1))

For distinct primes p₁, p₂ ∈ P_M, the corresponding sets of fractions {α/p : 1 ≤ α ≤ p - 1} are disjoint.

theorem LinnikLargeSieve.sum_over_fareySet (M : ℕ) (g : ℝ → ℝ) : ∑ ξ ∈ fareySet M, g ξ = ∑ p ∈ primesInRange M, ∑ α ∈ Finset.Icc 1 (p - 1), g (↑α / ↑p)

Sums over the Farey set decompose into double sums over (p, α) with p ∈ P_M and 1 ≤ α ≤ p - 1.

theorem LinnikLargeSieve.linnikLHS_le_farey_sum (N M : ℕ) : 0 < N → ∀ (hM : 0 < M) (f : Fin N → ℂ), ∃ (S : Finset ℝ), (∀ x ∈ S, 0 ≤ x ∧ x < 1) ∧ (∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 / ↑M ^ 2 ≤ |x - y|) ∧ linnikLHS N M f ≤ 2 / ↑M * ∑ ξ ∈ S, ‖fourierZ N (highFreqPart N f) ξ‖ ^ 2

Reduction step: there exists a 1/M^2-separated set S ⊆ [0, 1) (namely the Farey set Q_M) such that linnikLHS N M f ≤ (2/M) ∑_{ξ ∈ S} |\widehat{f_H}(ξ)|².

theorem LinnikLargeSieve.linnik_large_sieve : ∃ C > 0, ∀ (N M : ℕ), 0 < N → 0 < M → M ^ 2 ≤ N → ∀ (f : Fin N → ℂ), linnikLHS N M f ≤ C * (↑N / ↑M) * ∑ n : Fin N, ‖highFreqPart N f n‖ ^ 2

Linnik's large sieve inequality: there exists C > 0 such that for any f : [N] → ℂ and any M ≤ N^{1/2}, $$\sum_{p \in P_M} \|(\pi_p f)_H\|_{L^2}^2 \lesssim \frac{N}{M} \sum_n |f_H(n)|^2.$$