Factorial and variants #

This file defines the factorial, along with the ascending and descending variants.

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.

Nat.factorial n is the factorial of n.

Equations
• n.succ.factorial = n.succ * n.factorial
Instances For

factorial notation n!

Equations
Instances For
@[simp]
theorem Nat.factorial_succ (n : ) :
(n + 1).factorial = (n + 1) * n.factorial
@[simp]
@[simp]
theorem Nat.mul_factorial_pred {n : } (hn : 0 < n) :
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 < mm nm 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
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
Instances For
@[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
@[simp]
theorem Nat.one_ascFactorial (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_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
Instances For
@[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.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 < kn.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 kk 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 kn.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