Factorial and variants

This file defines the factorial, along with the ascending and descending variants. For the proof that the factorial of n counts the permutations of an n-element set, see Fintype.card_perm.

Main declarations

• Nat.factorial: The factorial.
• Nat.ascFactorial: The ascending factorial. It is the product of natural numbers from n to n + k - 1.
• Nat.descFactorial: The descending factorial. It is the product of natural numbers from n - k + 1 to n.

def Nat.factorial : ℕ → ℕ

Nat.factorial n is the factorial of n.

Equations

• Nat.factorial 0 = 1
• n.succ.factorial = n.succ * n.factorial

def Nat.term_! : Lean.TrailingParserDescr

factorial notation (n)! for Nat.factorial n. In Lean, names can end with exclamation marks (e.g. List.get!), so you cannot write n! in Lean, but must write (n)! or n ! instead. The former is preferred, since Lean can confuse the ! in n ! as the (prefix) boolean negation operation in some cases. For numerals the parentheses are not required, so e.g. 0! or 1! work fine. Todo: replace occurrences of n ! with (n)! in Mathlib.

Equations

• Nat.term_! = Lean.ParserDescr.trailingNode `Nat.term_! 10000 0 (Lean.ParserDescr.symbol "!")

@[simp]

theorem Nat.factorial_zero : factorial 0 = 1

theorem Nat.factorial_succ (n : ℕ) : (n + 1).factorial = (n + 1) * n.factorial

@[simp]

theorem Nat.factorial_one : factorial 1 = 1

@[simp]

theorem Nat.factorial_two : factorial 2 = 2

theorem Nat.mul_factorial_pred {n : ℕ} (hn : n ≠ 0) : n * (n - 1).factorial = n.factorial

theorem Nat.factorial_pos (n : ℕ) : 0 < n.factorial

theorem Nat.factorial_ne_zero (n : ℕ) : n.factorial ≠ 0

theorem Nat.factorial_dvd_factorial {m n : ℕ} (h : m ≤ n) : m.factorial ∣ n.factorial

theorem Nat.dvd_factorial {m n : ℕ} : 0 < m → m ≤ n → m ∣ n.factorial

theorem Nat.factorial_le {m n : ℕ} (h : m ≤ n) : m.factorial ≤ n.factorial

theorem Nat.factorial_mul_pow_le_factorial {m n : ℕ} : m.factorial * (m + 1) ^ n ≤ (m + n).factorial

theorem Nat.factorial_lt {m n : ℕ} (hn : 0 < n) : n.factorial < m.factorial ↔ n < m

theorem Nat.factorial_lt_of_lt {m n : ℕ} (hn : 0 < n) (h : n < m) : n.factorial < m.factorial

@[simp]

theorem Nat.one_lt_factorial {n : ℕ} : 1 < n.factorial ↔ 1 < n

@[simp]

theorem Nat.factorial_eq_one {n : ℕ} : n.factorial = 1 ↔ n ≤ 1

theorem Nat.factorial_inj {m n : ℕ} (hn : 1 < n) : n.factorial = m.factorial ↔ n = m

theorem Nat.factorial_inj' {m n : ℕ} (h : 1 < n ∨ 1 < m) : n.factorial = m.factorial ↔ n = m

theorem Nat.self_le_factorial (n : ℕ) : n ≤ n.factorial

theorem Nat.lt_factorial_self {n : ℕ} (hi : 3 ≤ n) : n < n.factorial

theorem Nat.add_factorial_succ_lt_factorial_add_succ {i : ℕ} (n : ℕ) (hi : 2 ≤ i) : i + (n + 1).factorial < (i + n + 1).factorial

theorem Nat.add_factorial_lt_factorial_add {i n : ℕ} (hi : 2 ≤ i) (hn : 1 ≤ n) : i + n.factorial < (i + n).factorial

theorem Nat.add_factorial_succ_le_factorial_add_succ (i n : ℕ) : i + (n + 1).factorial ≤ (i + (n + 1)).factorial

theorem Nat.add_factorial_le_factorial_add (i : ℕ) {n : ℕ} (n1 : 1 ≤ n) : i + n.factorial ≤ (i + n).factorial

theorem Nat.factorial_mul_pow_sub_le_factorial {n m : ℕ} (hnm : n ≤ m) : n.factorial * n ^ (m - n) ≤ m.factorial

theorem Nat.factorial_le_pow (n : ℕ) : n.factorial ≤ n ^ n

Ascending and descending factorials

def Nat.ascFactorial (n : ℕ) : ℕ → ℕ

n.ascFactorial k = n (n + 1) ⋯ (n + k - 1). This is closely related to ascPochhammer, but much less general.

Equations

• n.ascFactorial 0 = 1
• n.ascFactorial n_1.succ = (n + n_1) * n.ascFactorial n_1

@[simp]

theorem Nat.ascFactorial_zero (n : ℕ) : n.ascFactorial 0 = 1

theorem Nat.ascFactorial_succ {n k : ℕ} : n.ascFactorial k.succ = (n + k) * n.ascFactorial k

theorem Nat.zero_ascFactorial (k : ℕ) : ascFactorial 0 k.succ = 0

@[simp]

theorem Nat.one_ascFactorial (k : ℕ) : ascFactorial 1 k = k.factorial

theorem Nat.succ_ascFactorial (n k : ℕ) : n * n.succ.ascFactorial k = (n + k) * n.ascFactorial k

theorem Nat.factorial_mul_ascFactorial (n k : ℕ) : n.factorial * (n + 1).ascFactorial k = (n + k).factorial

(n + 1).ascFactorial k = (n + k) ! / n ! but without ℕ-division. See Nat.ascFactorial_eq_div for the version with ℕ-division.

theorem Nat.factorial_mul_ascFactorial' (n k : ℕ) (h : 0 < n) : (n - 1).factorial * n.ascFactorial k = (n + k - 1).factorial

n.ascFactorial k = (n + k - 1)! / (n - 1)! for n > 0 but without ℕ-division. See Nat.ascFactorial_eq_div for the version with ℕ-division. Consider using factorial_mul_ascFactorial to avoid complications of ℕ-subtraction.

theorem Nat.ascFactorial_mul_ascFactorial (n l k : ℕ) : n.ascFactorial l * (n + l).ascFactorial k = n.ascFactorial (l + k)

theorem Nat.ascFactorial_eq_div (n k : ℕ) : (n + 1).ascFactorial k = (n + k).factorial / n.factorial

Avoid in favor of Nat.factorial_mul_ascFactorial if you can. ℕ-division isn't worth it.

theorem Nat.ascFactorial_eq_div' (n k : ℕ) (h : 0 < n) : n.ascFactorial k = (n + k - 1).factorial / (n - 1).factorial

Avoid in favor of Nat.factorial_mul_ascFactorial' if you can. ℕ-division isn't worth it.

theorem Nat.ascFactorial_of_sub {n k : ℕ} : (n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1)

theorem Nat.pow_succ_le_ascFactorial (n k : ℕ) : n ^ k ≤ n.ascFactorial k

theorem Nat.pow_lt_ascFactorial' (n k : ℕ) : (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)

theorem Nat.pow_lt_ascFactorial (n : ℕ) {k : ℕ} : 2 ≤ k → (n + 1) ^ k < (n + 1).ascFactorial k

theorem Nat.ascFactorial_le_pow_add (n k : ℕ) : (n + 1).ascFactorial k ≤ (n + k) ^ k

theorem Nat.ascFactorial_lt_pow_add (n : ℕ) {k : ℕ} : 2 ≤ k → (n + 1).ascFactorial k < (n + k) ^ k

theorem Nat.ascFactorial_pos (n k : ℕ) : 0 < (n + 1).ascFactorial k

def Nat.descFactorial (n : ℕ) : ℕ → ℕ

n.descFactorial k = n! / (n - k)! (as seen in Nat.descFactorial_eq_div), but implemented recursively to allow for "quick" computation when using norm_num. This is closely related to descPochhammer, but much less general.

Equations

• n.descFactorial 0 = 1
• n.descFactorial n_1.succ = (n - n_1) * n.descFactorial n_1

@[simp]

theorem Nat.descFactorial_zero (n : ℕ) : n.descFactorial 0 = 1

@[simp]

theorem Nat.descFactorial_succ (n k : ℕ) : n.descFactorial (k + 1) = (n - k) * n.descFactorial k

theorem Nat.zero_descFactorial_succ (k : ℕ) : descFactorial 0 (k + 1) = 0

theorem Nat.descFactorial_one (n : ℕ) : n.descFactorial 1 = n

theorem Nat.succ_descFactorial_succ (n k : ℕ) : (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k

theorem Nat.succ_descFactorial (n k : ℕ) : (n + 1 - k) * (n + 1).descFactorial k = (n + 1) * n.descFactorial k

theorem Nat.descFactorial_self (n : ℕ) : n.descFactorial n = n.factorial

@[simp]

theorem Nat.descFactorial_eq_zero_iff_lt {n k : ℕ} : n.descFactorial k = 0 ↔ n < k

theorem Nat.descFactorial_of_lt {n k : ℕ} : n < k → n.descFactorial k = 0

Alias of the reverse direction of Nat.descFactorial_eq_zero_iff_lt.

theorem Nat.add_descFactorial_eq_ascFactorial (n k : ℕ) : (n + k).descFactorial k = (n + 1).ascFactorial k

theorem Nat.add_descFactorial_eq_ascFactorial' (n k : ℕ) : (n + k - 1).descFactorial k = n.ascFactorial k

theorem Nat.factorial_mul_descFactorial {n k : ℕ} : k ≤ n → (n - k).factorial * n.descFactorial k = n.factorial

n.descFactorial k = n! / (n - k)! but without ℕ-division. See Nat.descFactorial_eq_div for the version using ℕ-division.

theorem Nat.descFactorial_mul_descFactorial {k m n : ℕ} (hkm : k ≤ m) : (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

theorem Nat.descFactorial_eq_div {n k : ℕ} (h : k ≤ n) : n.descFactorial k = n.factorial / (n - k).factorial

Avoid in favor of Nat.factorial_mul_descFactorial if you can. ℕ-division isn't worth it.

theorem Nat.descFactorial_le (n : ℕ) {k m : ℕ} (h : k ≤ m) : k.descFactorial n ≤ m.descFactorial n

theorem Nat.pow_sub_le_descFactorial (n k : ℕ) : (n + 1 - k) ^ k ≤ n.descFactorial k

theorem Nat.pow_sub_lt_descFactorial' {n k : ℕ} : k + 2 ≤ n → (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)

theorem Nat.pow_sub_lt_descFactorial {n k : ℕ} : 2 ≤ k → k ≤ n → (n + 1 - k) ^ k < n.descFactorial k

theorem Nat.descFactorial_le_pow (n k : ℕ) : n.descFactorial k ≤ n ^ k

theorem Nat.descFactorial_lt_pow {n : ℕ} (hn : 1 ≤ n) {k : ℕ} : 2 ≤ k → n.descFactorial k < n ^ k

theorem Nat.factorial_two_mul_le (n : ℕ) : (2 * n).factorial ≤ (2 * n) ^ n * n.factorial

theorem Nat.two_pow_mul_factorial_le_factorial_two_mul (n : ℕ) : 2 ^ n * n.factorial ≤ (2 * n).factorial

Factorial via binary splitting.

We prove this is equal to the standard factorial and mark it @[csimp].

We could proceed further, with either Legendre or Luschny methods.

This is the highest factorial I can #eval using the naive implementation without a stack overflow:

/-- info: 114716 -/
#guard_msgs in
#eval 9718 ! |>.log2

We could implement a tail-recursive version (or just use Nat.fold), but instead let's jump straight to binary splitting.

def Nat.factorialBinarySplitting (n : ℕ) : ℕ

Factorial implemented using binary splitting.

While this still performs the same number of multiplications, the big-integer operands to each are much smaller.

Equations

• n.factorialBinarySplitting = if x : n = 0 then 1 else Nat.factorialBinarySplitting.prodRange 1 (n + 1) ⋯

@[irreducible]

def Nat.factorialBinarySplitting.prodRange (lo hi : ℕ) (h : lo < hi := by grind) : ℕ

prodRange lo hi is the product of the range lo to hi (exclusive), computed by binary splitting.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

theorem Nat.factorialBinarySplitting.factorial_mul_prodRange (lo hi : ℕ) (h : lo < hi) : lo.factorial * prodRange (lo + 1) (hi + 1) ⋯ = hi.factorial

@[csimp]

theorem Nat.factorialBinarySplitting_eq_factorial : factorial = factorialBinarySplitting

We are now limited by time, not stack space, and this is much faster than even the tail-recursive version.

#time -- Less than 1s. (Tail-recursive version takes longer for `(10^5) !`.)
#eval (10^6) ! |>.log2