def LargeSieveSize.projImage (A : Finset ℕ) (p : ℕ) [NeZero p] : Finset (ZMod p)

The image $\pi_p(A) \subseteq \mathbb{Z}_p$ of A ⊆ ℕ under reduction modulo p.

def LargeSieveSize.hasSmallProjections (A : Finset ℕ) (N : ℕ) : Prop

Predicate: A has small projections, meaning |π_p(A)| ≤ 0.99 p for every prime p ∈ P_{N^{1/2}}. This is the hypothesis of Corollary 5.

def LargeSieveSize.indicatorFn (A : Finset ℕ) (N : ℕ) : Fin N → ℂ

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

theorem LargeSieveSize.primes_in_dyadic_range_lower_bound : ∃ (N₀ : ℕ), ∀ (M : ℕ), N₀ ≤ M → ↑M / (4 * Real.log ↑M) ≤ ↑(LinnikLargeSieve.primesInRange M).card

Lower bound on the number of primes in the dyadic range [M/2, M]: for M large, |P_M| ≥ M / (4 log M). (A quantitative form of PNT.)

theorem LargeSieveSize.norm_sq_sub_mean_eq (N : ℕ) (hN : 0 < N) (f : Fin N → ℂ) : ∑ n : Fin N, ‖f n - (∑ i : Fin N, f i) / ↑N‖ ^ 2 = ∑ n : Fin N, ‖f n‖ ^ 2 - ‖∑ i : Fin N, f i‖ ^ 2 / ↑N

Centering identity in $L^2$: for f : Fin N → ℂ, $\sum_n |f(n) - \bar f|^2 = \sum_n |f(n)|^2 - |\sum_i f(i)|^2/N$, where $\bar f = (\sum_i f(i))/N$ is the mean.

theorem LargeSieveSize.indicator_l2_eq_card (N : ℕ) (A : Finset ℕ) (hN : 0 < N) (hA : A ⊆ Finset.Icc 1 N) : ∑ n : Fin N, ‖indicatorFn A N n‖ ^ 2 = ↑A.card

The squared $L^2$ norm of an indicator function indicatorFn A N equals |A|.

theorem LargeSieveSize.highFreqPart_eq_sub_div (N : ℕ) (f : Fin N → ℂ) (n : Fin N) : LinnikLargeSieve.highFreqPart N f n = f n - (∑ i : Fin N, f i) / ↑N

Unfolds the high-frequency part as f n - (mean of f).

theorem LargeSieveSize.indicator_highfreq_l2_le (N : ℕ) (A : Finset ℕ) (hN : 0 < N) (hA : A ⊆ Finset.Icc 1 N) : ∑ n : Fin N, ‖LinnikLargeSieve.highFreqPart N (indicatorFn A N) n‖ ^ 2 ≤ ↑A.card

The squared $L^2$ norm of the high-frequency part of an indicator function is at most |A| (since the variance is bounded by the second moment).

theorem LargeSieveSize.norm_sq_sub_mean_zmod (p : ℕ) [NeZero p] (g : ZMod p → ℂ) : ∑ a : ZMod p, ‖g a - (∑ b : ZMod p, g b) / ↑p‖ ^ 2 = ∑ a : ZMod p, ‖g a‖ ^ 2 - ‖∑ b : ZMod p, g b‖ ^ 2 / ↑p

Centering identity in $L^2(\mathbb{Z}_p)$: subtracting the mean from g : ZMod p → ℂ reduces the squared $L^2$ norm by |∑ g|² / p.

theorem LargeSieveSize.projHighFreqL2Sq_eq_sub (N p : ℕ) [NeZero p] (f : Fin N → ℂ) : LinnikLargeSieve.projHighFreqL2Sq N p f = ∑ a : ZMod p, ‖LinnikLargeSieve.modProjection N p f a‖ ^ 2 - ‖∑ a : ZMod p, LinnikLargeSieve.modProjection N p f a‖ ^ 2 / ↑p

Rewrites the high-frequency $L^2$ norm of the mod-p projection as ∑ |π_p f(a)|² - |∑ π_p f(a)|² / p.

theorem LargeSieveSize.sum_modProjection_eq (N p : ℕ) [NeZero p] (f : Fin N → ℂ) : ∑ a : ZMod p, LinnikLargeSieve.modProjection N p f a = ∑ n : Fin N, f n

The sum of the mod-p projection over ZMod p equals the full sum of f.

theorem LargeSieveSize.indicator_sum_eq_card (N : ℕ) (A : Finset ℕ) (hN : 0 < N) (hA : A ⊆ Finset.Icc 1 N) : ∑ n : Fin N, indicatorFn A N n = ↑A.card

The sum of the indicator function 1_A : Fin N → ℂ over Fin N equals |A|.

theorem LargeSieveSize.high_freq_energy_lower_bound (N : ℕ) (A : Finset ℕ) (hN : 4 ≤ N) (hA : A ⊆ Finset.Icc 1 N) (hSmall : hasSmallProjections A N) : 1 / 100 * ↑(LinnikLargeSieve.primesInRange N.sqrt).card * (↑A.card ^ 2 / ↑N.sqrt) ≤ LinnikLargeSieve.linnikLHS N N.sqrt (indicatorFn A N)

Lower bound on the Linnik LHS for indicator functions of sets with small projections: if |π_p(A)| ≤ 0.99 p for each p ∈ P_{N^{1/2}}, then (1/100) · |P_{N^{1/2}}| · |A|² / N^{1/2} ≤ linnikLHS N (N^{1/2}) 1_A.

theorem LargeSieveSize.corollary5_large_sieve_size : ∃ C > 0, ∃ (N₀ : ℕ), ∀ (N : ℕ) (A : Finset ℕ), N₀ ≤ N → A ⊆ Finset.Icc 1 N → hasSmallProjections A N → ↑A.card ≤ C * √↑N * Real.log ↑N

Corollary 5 (Large sieve, size bound): if A ⊆ [N] and |π_p(A)| ≤ 0.99 p for every prime p ∈ P_{N^{1/2}}, then |A| ≲ N^{1/2} (up to logarithmic factors: |A| ≤ C · √N · log N).