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. Note that it runs from n + 1 to n + k and not from n to n + k - 1. We might want to change that in the future.
Nat.descFactorial: The descending factorial. It runs from n - k to n.

source

ink

def Nat.factorial :

ℕ → ℕ

Nat.factorial n is the factorial of n.

Equations

Nat.factorial 0 = 1
Nat.factorial (Nat.succ n) = Nat.succ n * Nat.factorial n

source

ink

def Nat.term_! :

Lean.TrailingParserDescr

factorial notation n!

Equations

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

source

ink

@[simp]

theorem Nat.factorial_zero :

Nat.factorial 0 = 1

source

ink

@[simp]

theorem Nat.factorial_succ (n : ℕ) :

Nat.factorial (Nat.succ n) = (n + 1) * Nat.factorial n

source

ink

theorem Nat.factorial_one :

Nat.factorial 1 = 1

source

ink

theorem Nat.factorial_two :

Nat.factorial 2 = 2

source

ink

theorem Nat.mul_factorial_pred {n : ℕ} (hn : 0 < n) :

n * Nat.factorial (n - 1) = Nat.factorial n

source

ink

theorem Nat.factorial_pos (n : ℕ) :

0 < Nat.factorial n

source

ink

theorem Nat.factorial_ne_zero (n : ℕ) :

Nat.factorial n ≠ 0

source

ink

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

Nat.factorial m ∣ Nat.factorial n

source

ink

theorem Nat.dvd_factorial {m : ℕ} {n : ℕ} :

0 < m → m ≤ n → m ∣ Nat.factorial n

source

ink

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

Nat.factorial m ≤ Nat.factorial n

source

ink

theorem Nat.factorial_mul_pow_le_factorial {m : ℕ} {n : ℕ} :

Nat.factorial m * Nat.succ m ^ n ≤ Nat.factorial (m + n)

source

ink

theorem Nat.monotone_factorial :

Monotone Nat.factorial

source

ink

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

Nat.factorial n < Nat.factorial m ↔ n < m

source

ink

theorem Nat.one_lt_factorial {n : ℕ} :

1 < Nat.factorial n ↔ 1 < n

source

ink

theorem Nat.factorial_eq_one {n : ℕ} :

Nat.factorial n = 1 ↔ n ≤ 1

source

ink

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

Nat.factorial n = Nat.factorial m ↔ n = m

source

ink

theorem Nat.self_le_factorial (n : ℕ) :

n ≤ Nat.factorial n

source

ink

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

n < Nat.factorial n

source

ink

theorem Nat.add_factorial_succ_lt_factorial_add_succ {i : ℕ} (n : ℕ) (hi : 2 ≤ i) :

i + Nat.factorial (n + 1) < Nat.factorial (i + n + 1)

source

ink

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

i + Nat.factorial n < Nat.factorial (i + n)

source

ink

theorem Nat.add_factorial_succ_le_factorial_add_succ (i : ℕ) (n : ℕ) :

i + Nat.factorial (n + 1) ≤ Nat.factorial (i + (n + 1))

source

ink

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

i + Nat.factorial n ≤ Nat.factorial (i + n)

source

ink

theorem Nat.factorial_mul_pow_sub_le_factorial {n : ℕ} {m : ℕ} (hnm : n ≤ m) :

Nat.factorial n * n ^ (m - n) ≤ Nat.factorial m

Ascending and descending factorials #

source

ink

def Nat.ascFactorial (n : ℕ) :

ℕ → ℕ

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

Equations

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

source

ink

@[simp]

theorem Nat.ascFactorial_zero (n : ℕ) :

Nat.ascFactorial n 0 = 1

source

ink

@[simp]

theorem Nat.zero_ascFactorial (k : ℕ) :

Nat.ascFactorial 0 k = Nat.factorial k

source

ink

theorem Nat.ascFactorial_succ {n : ℕ} {k : ℕ} :

Nat.ascFactorial n (Nat.succ k) = (n + k + 1) * Nat.ascFactorial n k

source

ink

theorem Nat.succ_ascFactorial (n : ℕ) (k : ℕ) :

(n + 1) * Nat.ascFactorial (Nat.succ n) k = (n + k + 1) * Nat.ascFactorial n k

source

ink

theorem Nat.factorial_mul_ascFactorial (n : ℕ) (k : ℕ) :

Nat.factorial n * Nat.ascFactorial n k = Nat.factorial (n + k)

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

source

ink

theorem Nat.ascFactorial_eq_div (n : ℕ) (k : ℕ) :

Nat.ascFactorial n k = Nat.factorial (n + k) / Nat.factorial n

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

source

ink

theorem Nat.ascFactorial_of_sub {n : ℕ} {k : ℕ} (h : k < n) :

(n - k) * Nat.ascFactorial (n - k) k = Nat.ascFactorial (n - (k + 1)) (k + 1)

source

ink

theorem Nat.pow_succ_le_ascFactorial (n : ℕ) (k : ℕ) :

(n + 1) ^ k ≤ Nat.ascFactorial n k

source

ink

theorem Nat.pow_lt_ascFactorial' (n : ℕ) (k : ℕ) :

(n + 1) ^ (k + 2) < Nat.ascFactorial n (k + 2)

source

ink

theorem Nat.pow_lt_ascFactorial (n : ℕ) {k : ℕ} :

2 ≤ k → (n + 1) ^ k < Nat.ascFactorial n k

source

ink

theorem Nat.ascFactorial_le_pow_add (n : ℕ) (k : ℕ) :

Nat.ascFactorial n k ≤ (n + k) ^ k

source

ink

theorem Nat.ascFactorial_lt_pow_add (n : ℕ) {k : ℕ} :

2 ≤ k → Nat.ascFactorial n k < (n + k) ^ k

source

ink

theorem Nat.ascFactorial_pos (n : ℕ) (k : ℕ) :

0 < Nat.ascFactorial n k

source

ink

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 pochhammer, but much less general.

Equations