The Eratosthenes–Legendre sieve

For P ≠ 0, the number of n ∈ [1, x] coprime to P is Σ_{d ∣ P} μ(d) ⌊x/d⌋ (inclusion–exclusion by Möbius inversion; P need not be squarefree). With P the primorial of ⌊√x⌋, the integers in [1, x] with no prime factor ≤ √x are 1 and the primes in (√x, x], which gives Legendre's formula π(x) - π(√x) + 1 = Σ_{d ∣ P(√x)} μ(d) ⌊x/d⌋ for x ≥ 1.

Main results

• LegendreSieve.card_coprime_eq_sum_moebius: integers in [1, x] coprime to P counted by sum of mu(d) floor(x/d)
• LegendreSieve.primeCounting_sub_add_one: pi(x) - pi(sqrt x) + 1 = sum over d | primorial(sqrt x) of mu(d) floor(x/d)

References

• A.-M. Legendre, Essai sur la théorie des nombres, Paris, 1798 (2nd ed. 1808).

theorem LegendreSieve.sum_moebius_divisors (n : ℕ) : ∑ d ∈ n.divisors, ArithmeticFunction.moebius d = if n = 1 then 1 else 0

Möbius inversion: Σ_{d ∣ n} μ d = [n = 1].

theorem LegendreSieve.card_coprime_eq_sum_moebius (x P : ℕ) (hP : P ≠ 0) : ↑{n ∈ Finset.Ioc 0 x | n.Coprime P}.card = ∑ d ∈ P.divisors, ArithmeticFunction.moebius d * ↑(x / d)

Exact sieve. For P ≠ 0, the integers in [1, x] coprime to P are counted by inclusion–exclusion: Σ_{d ∣ P} μ(d) ⌊x/d⌋.

theorem LegendreSieve.coprime_primorial_iff (n z : ℕ) : n.Coprime (primorial z) ↔ ∀ (p : ℕ), Nat.Prime p → p ≤ z → ¬p ∣ n

Coprime to the primorial iff no prime factor ≤ z.

theorem LegendreSieve.sifted_eq (x : ℕ) (hx : 1 ≤ x) : {n ∈ Finset.Ioc 0 x | n.Coprime (primorial x.sqrt)} = insert 1 (Finset.filter Nat.Prime (Finset.Ioc x.sqrt x))

The sifted set is {1} ∪ {primes in (z, x]}.

theorem LegendreSieve.primeCounting_sub_add_one (x : ℕ) (hx : 1 ≤ x) : ↑(x.primeCounting - x.sqrt.primeCounting + 1) = ∑ d ∈ (primorial x.sqrt).divisors, ArithmeticFunction.moebius d * ↑(x / d)

Legendre's sieve. For x ≥ 1, π(x) - π(⌊√x⌋) + 1 = Σ_{d ∣ P(⌊√x⌋)} μ(d) ⌊x/d⌋.