Counting the primes up to m, in natural numbers

Three elementary bounds on the number π(m) of primes up to m, the cardinality of Nat.primesLE m, together with elementary upper bounds on Nat.lcmUpto n.

• π(m) ≤ m (Nat.card_primesLE_le).
• m ≤ (⌊log₂ m⌋ + 1)(π(m) + 1) (Nat.le_log_mul_card_primesLE), from the bound 2^m ≤ (m + 1) lcm(1, …, m) of Mathlib: each prime power in the least common multiple is at most m.
• So there are at least w primes up to (w + 1)(2⌊log₂(w + 1)⌋ + 4) (Nat.le_card_primesLE_mul_log).
• For n ≤ m, Nat.lcmUpto (m + n) divides Nat.lcmUpto m * (m + n).choose m (Nat.lcmUpto_add_dvd), yielding 2 * Nat.lcmUpto n ≤ 4 ^ n (Nat.two_mul_lcmUpto_le_four_pow) and Nat.lcmUpto n < 4 ^ n (Nat.lcmUpto_lt_four_pow) for 1 ≤ n.

Adapted from PrimeCounting.lean in anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5 and lean/Proofs/PrimeCycles.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

Main results

• Nat.le_card_primesLE_mul_log: an explicit prime-counting lower bound.
• Nat.lcmUpto_add_dvd, Nat.lcmUpto_add_le: binomial divisibility and upper bound on Nat.lcmUpto (m + n).
• Nat.two_mul_lcmUpto_le_four_pow, Nat.lcmUpto_lt_four_pow: 2 * lcm(1, …, n) ≤ 4 ^ n and lcm(1, …, n) < 4 ^ n for 1 ≤ n.

theorem Nat.card_primesLE_le (m : ℕ) : m.primesLE.card ≤ m

There are at most m primes up to m.

theorem Nat.le_log_mul_card_primesLE (m : ℕ) : m ≤ (log 2 m + 1) * (m.primesLE.card + 1)

A lower bound of Chebyshev's type in natural numbers: m ≤ (⌊log₂ m⌋ + 1)(π(m) + 1).

theorem Nat.le_card_primesLE_mul_log (w : ℕ) : w ≤ ((w + 1) * (2 * log 2 (w + 1) + 4)).primesLE.card

There are at least w primes up to (w + 1)(2⌊log₂(w + 1)⌋ + 4).

theorem Nat.lcmUpto_add_dvd {m n : ℕ} (h : n ≤ m) : (m + n).lcmUpto ∣ m.lcmUpto * (m + n).choose m

For n ≤ m, Nat.lcmUpto (m + n) divides Nat.lcmUpto m * (m + n).choose m. Every prime power p ^ L ≤ m + n exceeding m satisfies m < p ^ L ≤ m + n, which forces a base-p carry at digit L when adding m and n.

theorem Nat.lcmUpto_add_le {m n : ℕ} (h : n ≤ m) : (m + n).lcmUpto ≤ m.lcmUpto * (m + n).choose m

For n ≤ m, Nat.lcmUpto (m + n) ≤ Nat.lcmUpto m * (m + n).choose m.

theorem Nat.two_mul_lcmUpto_le_four_pow (n : ℕ) (hn : 1 ≤ n) : 2 * n.lcmUpto ≤ 4 ^ n

Elementary upper bound 2 * lcm(1, …, n) ≤ 4 ^ n for all n ≥ 1.

theorem Nat.lcmUpto_lt_four_pow (n : ℕ) (hn : 1 ≤ n) : n.lcmUpto < 4 ^ n

For every n ≥ 1, lcm(1, …, n) < 4 ^ n.