The Prime Counting Function

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

• Nat.primeCounting: The prime counting function π
• Nat.primeCounting': π(n - 1)

We then prove that these are monotone in Nat.monotone_primeCounting and Nat.monotone_primeCounting'. The last main theorem Nat.primeCounting'_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).

def Nat.primeCounting' : ℕ → ℕ

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

• Nat.primeCounting' = Nat.count Nat.Prime

def Nat.primeCounting (n : ℕ) : ℕ

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

Equations

• n.primeCounting = (n + 1).primeCounting'

def Nat.termπ : Lean.ParserDescr

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

Equations

• Nat.termπ = Lean.ParserDescr.node `Nat.termπ 1024 (Lean.ParserDescr.symbol "π")

def Nat.termπ' : Lean.ParserDescr

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

• Nat.termπ' = Lean.ParserDescr.node `Nat.termπ' 1024 (Lean.ParserDescr.symbol "π'")

theorem Nat.monotone_primeCounting' : Monotone Nat.primeCounting'

theorem Nat.monotone_primeCounting : Monotone Nat.primeCounting

@[simp]

theorem Nat.primeCounting'_nth_eq (n : ℕ) : (Nat.nth Nat.Prime n).primeCounting' = n

@[simp]

theorem Nat.prime_nth_prime (n : ℕ) : (Nat.nth Nat.Prime n).Prime

theorem Nat.primesBelow_card_eq_primeCounting' (n : ℕ) : n.primesBelow.card = n.primeCounting'

The cardinality of the finset primesBelow n equals the counting function primeCounting' at n.

theorem Nat.primeCounting'_add_le {a : ℕ} {k : ℕ} (h0 : 0 < a) (h1 : a < k) (n : ℕ) : (k + n).primeCounting' ≤ k.primeCounting' + a.totient * (n / a + 1)

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