mathlib3 documentation

number_theory.prime_counting

The Prime Counting Function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define the prime counting function: the function on natural numbers that returns the number of primes less than or equal to its input.

Main Results #

The main definitions for this file are

We then prove that these are monotone in nat.monotone_prime_counting and nat.monotone_prime_counting'. The last main theorem nat.prime_counting'_add_le is an upper bound on π' which arises by observing that all numbers greater than k and not coprime to k are not prime, and so only at most φ(k)/k fraction of the numbers from k to n are prime.

Notation #

We use the standard notation π to represent the prime counting function (and π' to represent the reindexed version).

source
def nat.prime_counting'  :
ℕ → ℕ

A variant of the traditional prime counting function which gives the number of primes strictly less than the input. More convenient for avoiding off-by-one errors.

Equations
source
def nat.prime_counting (n : ℕ) :
ℕ

The prime counting function: Returns the number of primes less than or equal to the input.

Equations
source
theorem nat.monotone_prime_counting'  :
monotone nat.prime_counting'
source
theorem nat.monotone_prime_counting  :
monotone nat.prime_counting
source
@[simp]
theorem nat.prime_counting'_nth_eq (n : ℕ) :
(nat.nth nat.prime n).prime_counting' = n
source
@[simp]
theorem nat.prime_nth_prime (n : ℕ) :
nat.prime (nat.nth nat.prime n)
source
theorem nat.prime_counting'_add_le {a k : ℕ} (h0 : 0 < a) (h1 : a < k) (n : ℕ) :
(k + n).prime_counting' ≤ k.prime_counting' + a.totient * (n / a + 1)

A linear upper bound on the size of the prime_counting' function