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

With open scoped Nat.Prime, 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.

With open scoped Nat.Prime, this has notation π'.

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.

With open scoped Nat.Prime, this has notation π.

Equations

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

def Nat.Prime.termπ : Lean.ParserDescr

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

With open scoped Nat.Prime, this has notation π.

Equations

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

def Nat.Prime.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.

With open scoped Nat.Prime, this has notation π'.

Equations

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

@[simp]

theorem Nat.primeCounting_sub_one (n : ℕ) : (n - 1).primeCounting = n.primeCounting'

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

theorem Nat.add_two_le_nth_prime (n : ℕ) : n + 2 ≤ Nat.nth Nat.Prime n

The nth prime is greater or equal to n + 2.

theorem Nat.surjective_primeCounting' : Function.Surjective Nat.primeCounting'

theorem Nat.surjective_primeCounting : Function.Surjective Nat.primeCounting

theorem Nat.tendsto_primeCounting' : Filter.Tendsto Nat.primeCounting' Filter.atTop Filter.atTop

theorem Nat.tensto_primeCounting : Filter.Tendsto Nat.primeCounting Filter.atTop Filter.atTop

@[simp]

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

@[simp]

theorem Nat.primeCounting'_eq_zero_iff {n : ℕ} : n.primeCounting' = 0 ↔ n ≤ 2

@[simp]

theorem Nat.primeCounting_eq_zero_iff {n : ℕ} : n.primeCounting = 0 ↔ n ≤ 1

@[simp]

theorem Nat.primeCounting_zero : Nat.primeCounting 0 = 0

@[simp]

theorem Nat.primeCounting_one : Nat.primeCounting 1 = 0

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