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.

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 * Finset.prod (Finset.filter Nat.Prime (Finset.Ico (m + 1) (m + n + 1))) fun p => p

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

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

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