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
We then prove that these are monotone in
Nat.monotone_primeCounting'. The last main theorem
Nat.primeCounting'_add_le is an upper
π' which arises by observing that all numbers greater than
k and not coprime to
are not prime, and so only at most
φ(k)/k fraction of the numbers from
n are prime.
We use the standard notation
π to represent the prime counting function (and
π' to represent
the reindexed version).