theorem LinnikLargeSieve.primesInRange_card_lower_bound : ∃ (c : ℝ) (M₀ : ℕ), c > 0 ∧ 2 ≤ M₀ ∧ ∀ (M : ℕ), M₀ ≤ M → c * ↑M ≤ ↑(primesInRange M).card

Lower bound on the number of primes in a dyadic interval: there exists c > 0 and M₀ ≥ 2 such that for all M ≥ M₀, the count |P_M| of primes in [M/2, M] satisfies c · M ≤ |P_M|. (This is essentially a quantitative form of the Prime Number Theorem.)

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

Average over primes p ∈ P_M of the squared $L^2$ norm of the high-frequency part of the mod-p projection: Avg_{p ∈ P_M} ‖(π_p f)_H‖_{L^2}^2 = (1/|P_M|) · linnikLHS N M f.

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

Corollary 4 (Large sieve average): for f : [N] → ℂ and M ≤ N^{1/2}, $$\operatorname{Avg}_{p \in P_M} \|(\pi_p f)_H\|_{L^2}^2 \lesssim \frac{N}{M^2} \sum_n |f_H(n)|^2.$$