Primorial

This file defines the primorial function (the product of primes less than or equal to some bound), and proves that primorial n ≤ 4 ^ n.

Notations

We use the local notation n# for the primorial of n: that is, the product of the primes less than or equal to n.

def primorial (n : ℕ) : ℕ

The primorial n# of n is the product of the primes less than or equal to n.

Equations

• primorial n = ∏ p ∈ Finset.filter (fun (p : ℕ) => Nat.Prime p) (Finset.range (n + 1)), p

theorem primorial_pos (n : ℕ) : 0 < primorial n

theorem primorial_succ {n : ℕ} (hn1 : n ≠ 1) (hn : Odd n) : primorial (n + 1) = primorial n

theorem primorial_add (m : ℕ) (n : ℕ) : primorial (m + n) = primorial m * ∏ p ∈ Finset.filter (fun (p : ℕ) => Nat.Prime p) (Finset.Ico (m + 1) (m + n + 1)), p

theorem primorial_add_dvd {m : ℕ} {n : ℕ} (h : n ≤ m) : primorial (m + n) ∣ primorial m * (m + n).choose m

theorem primorial_add_le {m : ℕ} {n : ℕ} (h : n ≤ m) : primorial (m + n) ≤ primorial m * (m + n).choose m

theorem primorial_le_4_pow (n : ℕ) : primorial n ≤ 4 ^ n