Documentation

Mathlib.NumberTheory.PrimeCounting

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 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).

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
Instances For

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

    Equations
    • n.primeCounting = (n + 1).primeCounting'
    Instances For

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

      Equations
      Instances For

        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
        Instances For
          @[simp]
          theorem Nat.primeCounting'_nth_eq (n : ) :
          (Nat.nth Nat.Prime n).primeCounting' = n
          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

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