theorem SieveTheory.sieve_theorem_1S (N S : ℕ) (X D : Finset ℕ) (hX : X ⊆ Finset.range N) (hD_prime : ∀ p ∈ D, Nat.Prime p) (hS : ∀ p ∈ D, (Finset.image (fun (x : ℕ) => x % p) X).card ≤ S) : X.card ≤ 2 * S ∨ D.card ≤ 2 * S * Nat.log 2 N

Sieve Theorem 1S. If $X \subseteq [N]$ and $D$ is a set of primes such that $|\pi_p(X)| \le S$ for every $p \in D$ (where $\pi_p$ is reduction modulo $p$), then either $|X| \le 2S$ or $|D| \lessapprox S \log N$.