Mathlib.Data.Nat.Factorial.Basic

Nat.factorial definition

: ℕ → ℕ

Full source

/-- `Nat.factorial n` is the factorial of `n`. -/
def factorial : ℕ → ℕ
  | 0 => 1
  | succ n => succ n * factorial n

Factorial of a natural number

Informal description

The factorial of a natural number $ n $, denoted $ n! $, is defined recursively as: \[ 0! = 1 \] \[ (n + 1)! = (n + 1) \times n! \]

Nat.term_! definition

: Lean.TrailingParserDescr✝

Full source

/-- 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. -/
scoped notation:10000 n "!" => Nat.factorial n

Factorial notation

Informal description

The notation `(n)!` denotes the factorial of a natural number `n`, defined as the product of all positive integers up to `n`. For numerals, the parentheses can be omitted, allowing notations like `0!` or `1!`.

Nat.factorial_zero theorem

: 0! = 1

Full source

@[simp] theorem factorial_zero : 0! = 1 :=
  rfl

Factorial of Zero: $0! = 1$

Informal description

The factorial of zero is equal to one, i.e., $0! = 1$.

Nat.factorial_succ theorem

(n : ℕ) : (n + 1)! = (n + 1) * n !

Full source

theorem factorial_succ (n : ℕ) : (n + 1)! = (n + 1) * n ! :=
  rfl

Recursive Formula for Factorial: $(n+1)! = (n+1) \times n!$

Informal description

For any natural number $n$, the factorial of $n+1$ equals $(n+1)$ multiplied by the factorial of $n$, i.e., $(n+1)! = (n+1) \times n!$.

Nat.factorial_one theorem

: 1! = 1

Full source

@[simp] theorem factorial_one : 1! = 1 :=
  rfl

Factorial of One: $1! = 1$

Informal description

The factorial of the natural number $1$ is equal to $1$, i.e., $1! = 1$.

Nat.factorial_two theorem

: 2! = 2

Full source

@[simp] theorem factorial_two : 2! = 2 :=
  rfl

Factorial of Two: $2! = 2$

Informal description

The factorial of the natural number $2$ is equal to $2$, i.e., $2! = 2$.

Nat.mul_factorial_pred theorem

(hn : n ≠ 0) : n * (n - 1)! = n !

Full source

theorem mul_factorial_pred (hn : n ≠ 0) : n * (n - 1)! = n ! :=
  Nat.sub_add_cancel (one_le_iff_ne_zero.mpr hn) ▸ rfl

Factorial Recursion: $n \cdot (n-1)! = n!$ for $n \neq 0$

Informal description

For any natural number $n \neq 0$, the product of $n$ and the factorial of $n-1$ equals the factorial of $n$, i.e., $n \cdot (n-1)! = n!$.

Nat.factorial_pos theorem

: ∀ n, 0 < n !

Full source

theorem factorial_pos : ∀ n, 0 < n !
  | 0 => Nat.zero_lt_one
  | succ n => Nat.mul_pos (succ_pos _) (factorial_pos n)

Positivity of Factorial

Informal description

For every natural number $n$, the factorial $n!$ is strictly positive, i.e., $0 < n!$.

Nat.factorial_ne_zero theorem

(n : ℕ) : n ! ≠ 0

Full source

theorem factorial_ne_zero (n : ℕ) : n !n ! ≠ 0 :=
  ne_of_gt (factorial_pos _)

Nonzero Property of Factorial: $n! \neq 0$

Informal description

For any natural number $n$, the factorial $n!$ is nonzero.

Nat.factorial_dvd_factorial theorem

{m n} (h : m ≤ n) : m ! ∣ n !

Full source

theorem factorial_dvd_factorial {m n} (h : m ≤ n) : m !m ! ∣ n ! := by
  induction h with
  | refl => exact Nat.dvd_refl _
  | step _ ih => exact Nat.dvd_trans ih (Nat.dvd_mul_left _ _)

Factorial Divisibility: $m! \mid n!$ for $m \leq n$

Informal description

For any natural numbers $m$ and $n$ such that $m \leq n$, the factorial of $m$ divides the factorial of $n$, i.e., $m! \mid n!$.

Nat.dvd_factorial theorem

: ∀ {m n}, 0 < m → m ≤ n → m ∣ n !

Full source

theorem dvd_factorial : ∀ {m n}, 0 < m → m ≤ n → m ∣ n !
  | succ _, _, _, h => Nat.dvd_trans (Nat.dvd_mul_right _ _) (factorial_dvd_factorial h)

Divisibility of Factorial: $m \mid n!$ for $0 < m \leq n$

Informal description

For any natural numbers $m$ and $n$ such that $0 < m$ and $m \leq n$, $m$ divides the factorial of $n$, i.e., $m \mid n!$.

Nat.factorial_le theorem

{m n} (h : m ≤ n) : m ! ≤ n !

Full source

@[mono, gcongr]
theorem factorial_le {m n} (h : m ≤ n) : m ! ≤ n ! :=
  le_of_dvd (factorial_pos _) (factorial_dvd_factorial h)

Monotonicity of Factorial: $m! \leq n!$ for $m \leq n$

Informal description

For any natural numbers $m$ and $n$ such that $m \leq n$, the factorial of $m$ is less than or equal to the factorial of $n$, i.e., $m! \leq n!$.

Nat.factorial_mul_pow_le_factorial theorem

: ∀ {m n : ℕ}, m ! * (m + 1) ^ n ≤ (m + n)!

Full source

theorem factorial_mul_pow_le_factorial : ∀ {m n : ℕ}, m ! * (m + 1) ^ n ≤ (m + n)!
  | m, 0 => by simp
  | m, n + 1 => by
    rw [← Nat.add_assoc, factorial_succ, Nat.mul_comm (_ + 1), Nat.pow_succ, ← Nat.mul_assoc]
    exact Nat.mul_le_mul factorial_mul_pow_le_factorial (succ_le_succ (le_add_right _ _))

Factorial-Power Inequality: $m! \cdot (m+1)^n \leq (m+n)!$

Informal description

For any natural numbers $m$ and $n$, the product of the factorial of $m$ and $(m + 1)$ raised to the power of $n$ is less than or equal to the factorial of $m + n$, i.e., \[ m! \cdot (m + 1)^n \leq (m + n)! \]

Nat.factorial_lt theorem

(hn : 0 < n) : n ! < m ! ↔ n < m

Full source

theorem factorial_lt (hn : 0 < n) : n !n ! < m ! ↔ n < m := by
  refine ⟨fun h => not_le.mp fun hmn => Nat.not_le_of_lt h (factorial_le hmn), fun h => ?_⟩
  have : ∀ {n}, 0 < n → n ! < (n + 1)! := by
    intro k hk
    rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]
    exact Nat.mul_pos hk k.factorial_pos
  induction h generalizing hn with
  | refl => exact this hn
  | step hnk ih => exact lt_trans (ih hn) <| this <| lt_trans hn <| lt_of_succ_le hnk

Factorial Strict Monotonicity: $n! < m! \leftrightarrow n < m$ for $n > 0$

Informal description

For any natural numbers $n$ and $m$ with $n > 0$, the factorial of $n$ is strictly less than the factorial of $m$ if and only if $n$ is strictly less than $m$, i.e., $n! < m! \leftrightarrow n < m$.

Nat.factorial_lt_of_lt theorem

{m n : ℕ} (hn : 0 < n) (h : n < m) : n ! < m !

Full source

@[gcongr]
lemma factorial_lt_of_lt {m n : ℕ} (hn : 0 < n) (h : n < m) : n ! < m ! := (factorial_lt hn).mpr h

Factorial Strict Monotonicity: $n < m \Rightarrow n! < m!$ for $n > 0$

Informal description

For any natural numbers $n$ and $m$ with $n > 0$, if $n < m$ then the factorial of $n$ is strictly less than the factorial of $m$, i.e., $n! < m!$.

Nat.one_lt_factorial theorem

: 1 < n ! ↔ 1 < n

Full source

@[simp] lemma one_lt_factorial : 1 < n ! ↔ 1 < n := factorial_lt Nat.one_pos

Factorial Greater Than One Criterion: $1 < n! \leftrightarrow 1 < n$

Informal description

For any natural number $n$, the factorial of $n$ is greater than $1$ if and only if $n$ is greater than $1$, i.e., $1 < n! \leftrightarrow 1 < n$.

Nat.factorial_eq_one theorem

: n ! = 1 ↔ n ≤ 1

Full source

@[simp]
theorem factorial_eq_one : n !n ! = 1 ↔ n ≤ 1 := by
  constructor
  · intro h
    rw [← not_lt, ← one_lt_factorial, h]
    apply lt_irrefl
  · rintro (_|_|_) <;> rfl

Factorial Equals One Criterion: $n! = 1 \leftrightarrow n \leq 1$

Informal description

For any natural number $n$, the factorial $n!$ equals $1$ if and only if $n \leq 1$.

Nat.factorial_inj theorem

(hn : 1 < n) : n ! = m ! ↔ n = m

Full source

theorem factorial_inj (hn : 1 < n) : n !n ! = m ! ↔ n = m := by
  refine ⟨fun h => ?_, congr_arg _⟩
  obtain hnm | rfl | hnm := lt_trichotomy n m
  · rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
    cases lt_irrefl _ hnm
  · rfl
  rw [← one_lt_factorial, h, one_lt_factorial] at hn
  rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
  cases lt_irrefl _ hnm

Factorial Injectivity for $n > 1$: $n! = m! \leftrightarrow n = m$

Informal description

For any natural numbers $n$ and $m$ with $n > 1$, the factorial of $n$ equals the factorial of $m$ if and only if $n = m$, i.e., $n! = m! \leftrightarrow n = m$.

Nat.factorial_inj' theorem

(h : 1 < n ∨ 1 < m) : n ! = m ! ↔ n = m

Full source

theorem factorial_inj' (h : 1 < n ∨ 1 < m) : n !n ! = m ! ↔ n = m := by
  obtain hn|hm := h
  · exact factorial_inj hn
  · rw [eq_comm, factorial_inj hm, eq_comm]

Factorial Injectivity for $n > 1$ or $m > 1$: $n! = m! \leftrightarrow n = m$

Informal description

For any natural numbers $n$ and $m$ such that either $n > 1$ or $m > 1$, the equality of their factorials $n! = m!$ holds if and only if $n = m$.

Nat.self_le_factorial theorem

: ∀ n : ℕ, n ≤ n !

Full source

theorem self_le_factorial : ∀ n : ℕ, n ≤ n !
  | 0 => Nat.zero_le _
  | k + 1 => Nat.le_mul_of_pos_right _ (Nat.one_le_of_lt k.factorial_pos)

Natural number is less than or equal to its factorial

Informal description

For every natural number $n$, we have $n \leq n!$.

Nat.lt_factorial_self theorem

{n : ℕ} (hi : 3 ≤ n) : n < n !

Full source

theorem lt_factorial_self {n : ℕ} (hi : 3 ≤ n) : n < n ! := by
  have : 0 < n := by omega
  have hn : 1 < pred n := le_pred_of_lt (succ_le_iff.mp hi)
  rw [← succ_pred_eq_of_pos ‹0 < n›, factorial_succ]
  exact (Nat.lt_mul_iff_one_lt_right (pred n).succ_pos).2
    ((Nat.lt_of_lt_of_le hn (self_le_factorial _)))

Factorial exceeds its argument for $n \geq 3$

Informal description

For any natural number $n \geq 3$, we have $n < n!$.

Nat.add_factorial_succ_lt_factorial_add_succ theorem

{i : ℕ} (n : ℕ) (hi : 2 ≤ i) : i + (n + 1)! < (i + n + 1)!

Full source

theorem add_factorial_succ_lt_factorial_add_succ {i : ℕ} (n : ℕ) (hi : 2 ≤ i) :
    i + (n + 1)! < (i + n + 1)! := by
  rw [factorial_succ (i + _), Nat.add_mul, Nat.one_mul]
  have := (i + n).self_le_factorial
  refine Nat.add_lt_add_of_lt_of_le (Nat.lt_of_le_of_lt ?_ ((Nat.lt_mul_iff_one_lt_right ?_).2 ?_))
    (factorial_le ?_) <;> omega

Inequality Relating Sum and Factorial: $i + (n+1)! < (i + n + 1)!$ for $i \geq 2$

Informal description

For any natural numbers $i \geq 2$ and $n$, the sum of $i$ and the factorial of $n+1$ is strictly less than the factorial of $i + n + 1$, i.e., $i + (n+1)! < (i + n + 1)!$.

Nat.add_factorial_lt_factorial_add theorem

{i n : ℕ} (hi : 2 ≤ i) (hn : 1 ≤ n) : i + n ! < (i + n)!

Full source

theorem add_factorial_lt_factorial_add {i n : ℕ} (hi : 2 ≤ i) (hn : 1 ≤ n) :
    i + n ! < (i + n)! := by
  cases hn
  · rw [factorial_one]
    exact lt_factorial_self (succ_le_succ hi)
  exact add_factorial_succ_lt_factorial_add_succ _ hi

Factorial Growth Inequality: $i + n! < (i + n)!$ for $i \geq 2$, $n \geq 1$

Informal description

For any natural numbers $i \geq 2$ and $n \geq 1$, the sum of $i$ and the factorial of $n$ is strictly less than the factorial of $i + n$, i.e., $i + n! < (i + n)!$.

Nat.add_factorial_succ_le_factorial_add_succ theorem

(i : ℕ) (n : ℕ) : i + (n + 1)! ≤ (i + (n + 1))!

Full source

theorem add_factorial_succ_le_factorial_add_succ (i : ℕ) (n : ℕ) :
    i + (n + 1)! ≤ (i + (n + 1))! := by
  cases (le_or_lt (2 : ℕ) i)
  · rw [← Nat.add_assoc]
    apply Nat.le_of_lt
    apply add_factorial_succ_lt_factorial_add_succ
    assumption
  · match i with
    | 0 => simp
    | 1 =>
      rw [← Nat.add_assoc, factorial_succ (1 + n), Nat.add_mul, Nat.one_mul, Nat.add_comm 1 n,
        Nat.add_le_add_iff_right]
      exact Nat.mul_pos n.succ_pos n.succ.factorial_pos
    | succ (succ n) => contradiction

Sum and Factorial Inequality: $i + (n+1)! \leq (i + n + 1)!$

Informal description

For any natural numbers $i$ and $n$, the sum of $i$ and the factorial of $n+1$ is less than or equal to the factorial of $i + (n + 1)$, i.e., $i + (n+1)! \leq (i + n + 1)!$.

Nat.add_factorial_le_factorial_add theorem

(i : ℕ) {n : ℕ} (n1 : 1 ≤ n) : i + n ! ≤ (i + n)!

Full source

theorem add_factorial_le_factorial_add (i : ℕ) {n : ℕ} (n1 : 1 ≤ n) : i + n ! ≤ (i + n)! := by
  rcases n1 with - | @h
  · exact self_le_factorial _
  exact add_factorial_succ_le_factorial_add_succ i h

Sum-Factorial Inequality: $i + n! \leq (i + n)!$ for $n \geq 1$

Informal description

For any natural numbers $i$ and $n$ with $n \geq 1$, the sum of $i$ and the factorial of $n$ is less than or equal to the factorial of $i + n$, i.e., $i + n! \leq (i + n)!$.

Nat.factorial_mul_pow_sub_le_factorial theorem

{n m : ℕ} (hnm : n ≤ m) : n ! * n ^ (m - n) ≤ m !

Full source

theorem factorial_mul_pow_sub_le_factorial {n m : ℕ} (hnm : n ≤ m) : n ! * n ^ (m - n) ≤ m ! := by
  calc
    _ ≤ n ! * (n + 1) ^ (m - n) := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left n.le_succ _)
    _ ≤ _ := by simpa [hnm] using @Nat.factorial_mul_pow_le_factorial n (m - n)

Factorial-Power Inequality: $n! \cdot n^{m-n} \leq m!$ for $n \leq m$

Informal description

For any natural numbers $n$ and $m$ such that $n \leq m$, the product of the factorial of $n$ and $n$ raised to the power of $m - n$ is less than or equal to the factorial of $m$, i.e., \[ n! \cdot n^{m - n} \leq m! \]

Nat.factorial_le_pow theorem

: ∀ n, n ! ≤ n ^ n

Full source

lemma factorial_le_pow : ∀ n, n ! ≤ n ^ n
  | 0 => le_refl _
  | n + 1 =>
    calc
      _ ≤ (n + 1) * n ^ n := Nat.mul_le_mul_left _ n.factorial_le_pow
      _ ≤ (n + 1) * (n + 1) ^ n := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left n.le_succ _)
      _ = _ := by rw [pow_succ']

Factorial Bound: $n! \leq n^n$

Informal description

For every natural number $n$, the factorial of $n$ is less than or equal to $n$ raised to the power of $n$, i.e., $n! \leq n^n$.

Nat.ascFactorial definition

(n : ℕ) : ℕ → ℕ

Full source

/-- `n.ascFactorial k = n (n + 1) ⋯ (n + k - 1)`. This is closely related to `ascPochhammer`, but
much less general. -/
def ascFactorial (n : ℕ) : ℕ → ℕ
  | 0 => 1
  | k + 1 => (n + k) * ascFactorial n k

Ascending factorial

Informal description

The ascending factorial function $ n^{\overline{k}} $ is defined for natural numbers $ n $ and $ k $ as the product $ n (n + 1) \cdots (n + k - 1) $. It satisfies the recurrence relations: - $ n^{\overline{0}} = 1 $ - $ n^{\overline{k+1}} = (n + k) \cdot n^{\overline{k}} $

Nat.ascFactorial_zero theorem

(n : ℕ) : n.ascFactorial 0 = 1

Full source

@[simp]
theorem ascFactorial_zero (n : ℕ) : n.ascFactorial 0 = 1 :=
  rfl

Base case of ascending factorial: $n^{\overline{0}} = 1$

Informal description

For any natural number $n$, the ascending factorial $n^{\overline{0}}$ equals $1$.

Nat.ascFactorial_succ theorem

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

Full source

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

Recurrence Relation for Ascending Factorial: $n^{\overline{k+1}} = (n + k) \cdot n^{\overline{k}}$

Informal description

For any natural numbers $n$ and $k$, the ascending factorial satisfies the recurrence relation: $$ n^{\overline{k+1}} = (n + k) \cdot n^{\overline{k}} $$ where $n^{\overline{k}}$ denotes the ascending factorial of $n$ with parameter $k$.

Nat.zero_ascFactorial theorem

: ∀ (k : ℕ), (0 : ℕ).ascFactorial k.succ = 0

Full source

theorem zero_ascFactorial : ∀ (k : ℕ), (0 : ℕ).ascFactorial k.succ = 0
  | 0 => by
    rw [ascFactorial_succ, ascFactorial_zero, Nat.zero_add, Nat.zero_mul]
  | (k+1) => by
    rw [ascFactorial_succ, zero_ascFactorial k, Nat.mul_zero]

Ascending Factorial of Zero: $0^{\overline{k+1}} = 0$

Informal description

For any natural number $k$, the ascending factorial of $0$ with parameter $k+1$ is equal to $0$, i.e., $0^{\overline{k+1}} = 0$.

Nat.one_ascFactorial theorem

: ∀ (k : ℕ), (1 : ℕ).ascFactorial k = k.factorial

Full source

@[simp]
theorem one_ascFactorial : ∀ (k : ℕ), (1 : ℕ).ascFactorial k = k.factorial
  | 0 => ascFactorial_zero 1
  | (k+1) => by
    rw [ascFactorial_succ, one_ascFactorial k, Nat.add_comm, factorial_succ]

Ascending Factorial of One Equals Factorial: $1^{\overline{k}} = k!$

Informal description

For any natural number $k$, the ascending factorial of $1$ with parameter $k$ equals the factorial of $k$, i.e., $1^{\overline{k}} = k!$.

Nat.succ_ascFactorial theorem

(n : ℕ) : ∀ k, n * n.succ.ascFactorial k = (n + k) * n.ascFactorial k

Full source

theorem succ_ascFactorial (n : ℕ) :
    ∀ k, n * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
  | 0 => by rw [Nat.add_zero, ascFactorial_zero, ascFactorial_zero]
  | k + 1 => by rw [ascFactorial, Nat.mul_left_comm, succ_ascFactorial n k, ascFactorial, succ_add,
    ← Nat.add_assoc]

Recurrence relation for ascending factorials: $n \cdot (n+1)^{\overline{k}} = (n + k) \cdot n^{\overline{k}}$

Informal description

For any natural numbers $n$ and $k$, the following identity holds for ascending factorials: $$n \cdot (n+1)^{\overline{k}} = (n + k) \cdot n^{\overline{k}}$$ where $n^{\overline{k}}$ denotes the ascending factorial of $n$ with parameter $k$.

Nat.factorial_mul_ascFactorial theorem

(n : ℕ) : ∀ k, n ! * (n + 1).ascFactorial k = (n + k)!

Full source

/-- `(n + 1).ascFactorial k = (n + k) ! / n !` but without ℕ-division. See
`Nat.ascFactorial_eq_div` for the version with ℕ-division. -/
theorem factorial_mul_ascFactorial (n : ℕ) : ∀ k, n ! * (n + 1).ascFactorial k = (n + k)!
  | 0 => by rw [ascFactorial_zero, Nat.add_zero, Nat.mul_one]
  | k + 1 => by
    rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
      ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]

Factorial-Ascending Factorial Product Identity: $n! \cdot (n+1)^{\overline{k}} = (n+k)!$

Informal description

For any natural numbers $n$ and $k$, the product of the factorial of $n$ and the ascending factorial of $n+1$ with parameter $k$ equals the factorial of $n+k$, i.e., $$n! \cdot (n+1)^{\overline{k}} = (n+k)!$$ where $(n+1)^{\overline{k}}$ denotes the ascending factorial $(n+1)(n+2)\cdots(n+k)$.

Nat.factorial_mul_ascFactorial' theorem

(n k : ℕ) (h : 0 < n) : (n - 1)! * n.ascFactorial k = (n + k - 1)!

Full source

/-- `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 factorial_mul_ascFactorial' (n k : ℕ) (h : 0 < n) :
    (n - 1) ! * n.ascFactorial k = (n + k - 1)! := by
  rw [Nat.sub_add_comm h, Nat.sub_one]
  nth_rw 2 [Nat.eq_add_of_sub_eq h rfl]
  rw [Nat.sub_one, factorial_mul_ascFactorial]

Factorial-Ascending Factorial Product Identity for Positive $n$: $(n-1)! \cdot n^{\overline{k}} = (n+k-1)!$

Informal description

For any natural numbers $n > 0$ and $k$, the product of the factorial of $n-1$ and the ascending factorial of $n$ with parameter $k$ equals the factorial of $n + k - 1$, i.e., $$(n-1)! \cdot n^{\overline{k}} = (n + k - 1)!$$ where $n^{\overline{k}}$ denotes the ascending factorial $n(n+1)\cdots(n+k-1)$.

Nat.ascFactorial_mul_ascFactorial theorem

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

Full source

theorem ascFactorial_mul_ascFactorial (n l k : ℕ) :
    n.ascFactorial l * (n + l).ascFactorial k = n.ascFactorial (l + k) := by
  cases n with
  | zero =>
    cases l
    · simp only [ascFactorial_zero, Nat.add_zero, Nat.one_mul, Nat.zero_add]
    · simp only [Nat.add_right_comm, zero_ascFactorial, Nat.zero_add, Nat.zero_mul]
  | succ n' =>
    apply Nat.mul_left_cancel (factorial_pos n')
    simp only [Nat.add_assoc, ← Nat.mul_assoc, factorial_mul_ascFactorial]
    rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]

Product of Ascending Factorials: $n^{\overline{l}} \cdot (n + l)^{\overline{k}} = n^{\overline{l + k}}$

Informal description

For any natural numbers $n$, $l$, and $k$, the product of the ascending factorial $n^{\overline{l}}$ and the ascending factorial $(n + l)^{\overline{k}}$ equals the ascending factorial $n^{\overline{l + k}}$, i.e., $$n^{\overline{l}} \cdot (n + l)^{\overline{k}} = n^{\overline{l + k}}$$ where $n^{\overline{k}}$ denotes the ascending factorial $n(n+1)\cdots(n+k-1)$.

Nat.ascFactorial_eq_div theorem

(n k : ℕ) : (n + 1).ascFactorial k = (n + k)! / n !

Full source

/-- Avoid in favor of `Nat.factorial_mul_ascFactorial` if you can. ℕ-division isn't worth it. -/
theorem ascFactorial_eq_div (n k : ℕ) : (n + 1).ascFactorial k = (n + k)! / n ! :=
  Nat.eq_div_of_mul_eq_right n.factorial_ne_zero (factorial_mul_ascFactorial _ _)

Ascending Factorial as Quotient of Factorials: $(n+1)^{\overline{k}} = \frac{(n+k)!}{n!}$

Informal description

For any natural numbers $n$ and $k$, the ascending factorial $(n+1)^{\overline{k}}$ equals the quotient of the factorial $(n+k)!$ divided by $n!$, i.e., $$(n+1)^{\overline{k}} = \frac{(n+k)!}{n!}$$ where $(n+1)^{\overline{k}}$ denotes the product $(n+1)(n+2)\cdots(n+k)$.

Nat.ascFactorial_eq_div' theorem

(n k : ℕ) (h : 0 < n) : n.ascFactorial k = (n + k - 1)! / (n - 1)!

Full source

/-- Avoid in favor of `Nat.factorial_mul_ascFactorial'` if you can. ℕ-division isn't worth it. -/
theorem ascFactorial_eq_div' (n k : ℕ) (h : 0 < n) :
    n.ascFactorial k = (n + k - 1)! / (n - 1) ! :=
  Nat.eq_div_of_mul_eq_right (n - 1).factorial_ne_zero (factorial_mul_ascFactorial' _ _ h)

Ascending Factorial as Quotient of Factorials for Positive $n$: $n^{\overline{k}} = \frac{(n+k-1)!}{(n-1)!}$

Informal description

For any natural numbers $n > 0$ and $k$, the ascending factorial $n^{\overline{k}}$ equals the quotient of the factorial $(n + k - 1)!$ divided by $(n - 1)!$, i.e., $$n^{\overline{k}} = \frac{(n + k - 1)!}{(n - 1)!}$$ where $n^{\overline{k}}$ denotes the product $n(n+1)\cdots(n+k-1)$.

Nat.ascFactorial_of_sub theorem

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

Full source

theorem ascFactorial_of_sub {n k : ℕ} :
    (n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1) := by
  rw [succ_ascFactorial, ascFactorial_succ]

Recurrence relation for shifted ascending factorials: $(n - k) \cdot (n - k + 1)^{\overline{k}} = (n - k)^{\overline{k+1}}$

Informal description

For any natural numbers $n$ and $k$, the following identity holds for ascending factorials: $$(n - k) \cdot (n - k + 1)^{\overline{k}} = (n - k)^{\overline{k+1}}$$ where $x^{\overline{m}}$ denotes the ascending factorial of $x$ with parameter $m$.

Nat.pow_succ_le_ascFactorial theorem

(n : ℕ) : ∀ k : ℕ, n ^ k ≤ n.ascFactorial k

Full source

theorem pow_succ_le_ascFactorial (n : ℕ) : ∀ k : ℕ, n ^ k ≤ n.ascFactorial k
  | 0 => by rw [ascFactorial_zero, Nat.pow_zero]
  | k + 1 => by
    rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, ← succ_ascFactorial]
    exact Nat.mul_le_mul (Nat.le_refl n)
      (Nat.le_trans (Nat.pow_le_pow_left (le_succ n) k) (pow_succ_le_ascFactorial n.succ k))

Power Bound by Ascending Factorial: $n^k \leq n^{\overline{k}}$

Informal description

For any natural numbers $n$ and $k$, the $k$-th power of $n$ is less than or equal to the ascending factorial of $n$ with parameter $k$, i.e., $n^k \leq n^{\overline{k}}$.

Nat.pow_lt_ascFactorial' theorem

(n k : ℕ) : (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)

Full source

theorem pow_lt_ascFactorial' (n k : ℕ) : (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2) := by
  rw [Nat.pow_succ, ascFactorial, Nat.mul_comm]
  exact Nat.mul_lt_mul_of_lt_of_le' (Nat.lt_add_of_pos_right k.succ_pos)
    (pow_succ_le_ascFactorial n.succ _) (Nat.pow_pos n.succ_pos)

Strict Power Bound by Ascending Factorial: $(n + 1)^{k + 2} < (n + 1)^{\overline{k + 2}}$

Informal description

For any natural numbers $n$ and $k$, the $(k+2)$-th power of $n+1$ is strictly less than the ascending factorial of $n+1$ with parameter $k+2$, i.e., $(n + 1)^{k + 2} < (n + 1)^{\overline{k + 2}}$.

Nat.pow_lt_ascFactorial theorem

(n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1) ^ k < (n + 1).ascFactorial k

Full source

theorem pow_lt_ascFactorial (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1) ^ k < (n + 1).ascFactorial k
  | 0 => by rintro ⟨⟩
  | 1 => by intro; contradiction
  | k + 2 => fun _ => pow_lt_ascFactorial' n k

Strict Power Bound by Ascending Factorial: $(n + 1)^k < (n + 1)^{\overline{k}}$ for $k \geq 2$

Informal description

For any natural numbers $n$ and $k$ with $k \geq 2$, the $k$-th power of $n+1$ is strictly less than the ascending factorial of $n+1$ with parameter $k$, i.e., $(n + 1)^k < (n + 1)^{\overline{k}}$.

Nat.ascFactorial_le_pow_add theorem

(n : ℕ) : ∀ k : ℕ, (n + 1).ascFactorial k ≤ (n + k) ^ k

Full source

theorem ascFactorial_le_pow_add (n : ℕ) : ∀ k : ℕ, (n+1).ascFactorial k ≤ (n + k) ^ k
  | 0 => by rw [ascFactorial_zero, Nat.pow_zero]
  | k + 1 => by
    rw [ascFactorial_succ, Nat.pow_succ, Nat.mul_comm, ← Nat.add_assoc, Nat.add_right_comm n 1 k]
    exact Nat.mul_le_mul_right _
      (Nat.le_trans (ascFactorial_le_pow_add _ k) (Nat.pow_le_pow_left (le_succ _) _))

Upper bound for ascending factorial: $(n+1)^{\overline{k}} \leq (n + k)^k$

Informal description

For any natural numbers $n$ and $k$, the ascending factorial $(n+1)^{\overline{k}}$ satisfies the inequality: $$ (n+1)^{\overline{k}} \leq (n + k)^k $$ where $(n+1)^{\overline{k}}$ denotes the product $(n+1)(n+2)\cdots(n+k)$.

Nat.ascFactorial_lt_pow_add theorem

(n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1).ascFactorial k < (n + k) ^ k

Full source

theorem ascFactorial_lt_pow_add (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1).ascFactorial k < (n + k) ^ k
  | 0 => by rintro ⟨⟩
  | 1 => by intro; contradiction
  | k + 2 => fun _ => by
    rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, succ_add_eq_add_succ n (k + 1)]
    exact Nat.mul_lt_mul_of_le_of_lt (le_refl _) (Nat.lt_of_le_of_lt (ascFactorial_le_pow_add n _)
      (Nat.pow_lt_pow_left (Nat.lt_succ_self _) k.succ_ne_zero)) (succ_pos _)

Strict Upper Bound for Ascending Factorial: $(n+1)^{\overline{k}} < (n + k)^k$ when $k \geq 2$

Informal description

For any natural numbers $n$ and $k$ with $k \geq 2$, the ascending factorial $(n+1)^{\overline{k}}$ satisfies the strict inequality: $$ (n+1)^{\overline{k}} < (n + k)^k $$ where $(n+1)^{\overline{k}}$ denotes the product $(n+1)(n+2)\cdots(n+k)$.

Nat.ascFactorial_pos theorem

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

Full source

theorem ascFactorial_pos (n k : ℕ) : 0 < (n + 1).ascFactorial k :=
  Nat.lt_of_lt_of_le (Nat.pow_pos n.succ_pos) (pow_succ_le_ascFactorial (n + 1) k)

Positivity of Ascending Factorial: $(n+1)^{\overline{k}} > 0$

Informal description

For any natural numbers $n$ and $k$, the ascending factorial $(n+1)^{\overline{k}}$ is strictly positive, i.e., $(n+1)^{\overline{k}} > 0$.

Nat.descFactorial definition

(n : ℕ) : ℕ → ℕ

Full source

/-- `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. -/
def descFactorial (n : ℕ) : ℕ → ℕ
  | 0 => 1
  | k + 1 => (n - k) * descFactorial n k

Descending factorial of natural numbers

Informal description

The descending factorial of natural numbers $n$ and $k$, denoted $n^{\underline{k}}$, is defined recursively as: - $n^{\underline{0}} = 1$ - $n^{\underline{k+1}} = (n - k) \cdot n^{\underline{k}}$ This computes the product of the $k$ consecutive integers starting from $n$ and decreasing by 1 each time, i.e., $n \cdot (n-1) \cdot \ldots \cdot (n-k+1)$.

Nat.descFactorial_zero theorem

(n : ℕ) : n.descFactorial 0 = 1

Full source

@[simp]
theorem descFactorial_zero (n : ℕ) : n.descFactorial 0 = 1 :=
  rfl

Base case of descending factorial: $n^{\underline{0}} = 1$

Informal description

For any natural number $n$, the descending factorial $n^{\underline{0}}$ equals $1$.

Nat.descFactorial_succ theorem

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

Full source

@[simp]
theorem descFactorial_succ (n k : ℕ) : n.descFactorial (k + 1) = (n - k) * n.descFactorial k :=
  rfl

Recurrence relation for descending factorial: $n^{\underline{k+1}} = (n - k) \cdot n^{\underline{k}}$

Informal description

For any natural numbers $n$ and $k$, the descending factorial satisfies the recurrence relation: $$ n^{\underline{k+1}} = (n - k) \cdot n^{\underline{k}} $$ where $n^{\underline{k}}$ denotes the descending factorial of $n$ and $k$.

Nat.zero_descFactorial_succ theorem

(k : ℕ) : (0 : ℕ).descFactorial (k + 1) = 0

Full source

theorem zero_descFactorial_succ (k : ℕ) : (0 : ℕ).descFactorial (k + 1) = 0 := by
  rw [descFactorial_succ, Nat.zero_sub, Nat.zero_mul]

Descending factorial of zero: $0^{\underline{k+1}} = 0$

Informal description

For any natural number $k$, the descending factorial of $0$ and $k+1$ is equal to $0$, i.e., $0^{\underline{k+1}} = 0$.

Nat.descFactorial_one theorem

(n : ℕ) : n.descFactorial 1 = n

Full source

theorem descFactorial_one (n : ℕ) : n.descFactorial 1 = n := by simp

Descending factorial of order 1: $n^{\underline{1}} = n$

Informal description

For any natural number $n$, the descending factorial $n^{\underline{1}}$ equals $n$.

Nat.succ_descFactorial_succ theorem

(n : ℕ) : ∀ k : ℕ, (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k

Full source

theorem succ_descFactorial_succ (n : ℕ) :
    ∀ k : ℕ, (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k
  | 0 => by rw [descFactorial_zero, descFactorial_one, Nat.mul_one]
  | succ k => by
    rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ,
      Nat.mul_left_comm]

Recurrence for Successor Descending Factorial: $(n+1)^{\underline{k+1}} = (n+1) \cdot n^{\underline{k}}$

Informal description

For any natural numbers $n$ and $k$, the descending factorial satisfies the recurrence relation: $$(n + 1)^{\underline{k + 1}} = (n + 1) \cdot n^{\underline{k}}$$ where $n^{\underline{k}}$ denotes the descending factorial of $n$ and $k$.

Nat.succ_descFactorial theorem

(n : ℕ) : ∀ k, (n + 1 - k) * (n + 1).descFactorial k = (n + 1) * n.descFactorial k

Full source

theorem succ_descFactorial (n : ℕ) :
    ∀ k, (n + 1 - k) * (n + 1).descFactorial k = (n + 1) * n.descFactorial k
  | 0 => by rw [Nat.sub_zero, descFactorial_zero, descFactorial_zero]
  | k + 1 => by
    rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, Nat.mul_left_comm]

Recurrence Identity for Descending Factorials: $(n+1-k)(n+1)^{\underline{k}} = (n+1)n^{\underline{k}}$

Informal description

For any natural numbers $n$ and $k$, the following identity holds for descending factorials: $$(n + 1 - k) \cdot (n + 1)^{\underline{k}} = (n + 1) \cdot n^{\underline{k}}$$ where $n^{\underline{k}}$ denotes the descending factorial of $n$ and $k$.

Nat.descFactorial_self theorem

: ∀ n : ℕ, n.descFactorial n = n !

Full source

theorem descFactorial_self : ∀ n : ℕ, n.descFactorial n = n !
  | 0 => by rw [descFactorial_zero, factorial_zero]
  | succ n => by rw [succ_descFactorial_succ, descFactorial_self n, factorial_succ]

Descending Factorial Equals Factorial: $n^{\underline{n}} = n!$

Informal description

For any natural number $n$, the descending factorial $n^{\underline{n}}$ equals the factorial $n!$.

Nat.descFactorial_eq_zero_iff_lt theorem

{n : ℕ} : ∀ {k : ℕ}, n.descFactorial k = 0 ↔ n < k

Full source

@[simp]
theorem descFactorial_eq_zero_iff_lt {n : ℕ} : ∀ {k : ℕ}, n.descFactorial k = 0 ↔ n < k
  | 0 => by simp only [descFactorial_zero, Nat.one_ne_zero, Nat.not_lt_zero]
  | succ k => by
    rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, Nat.lt_succ_iff,
      Nat.sub_eq_zero_iff_le, Nat.lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]
    exact fun h _ => h

Zero Descending Factorial Criterion: $n^{\underline{k}} = 0 \leftrightarrow n < k$

Informal description

For any natural numbers $n$ and $k$, the descending factorial $n^{\underline{k}}$ equals zero if and only if $n < k$.

Nat.add_descFactorial_eq_ascFactorial theorem

(n : ℕ) : ∀ k : ℕ, (n + k).descFactorial k = (n + 1).ascFactorial k

Full source

theorem add_descFactorial_eq_ascFactorial (n : ℕ) : ∀ k : ℕ,
    (n + k).descFactorial k = (n + 1).ascFactorial k
  | 0 => by rw [ascFactorial_zero, descFactorial_zero]
  | succ k => by
    rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ,
      add_descFactorial_eq_ascFactorial _ k, Nat.add_right_comm]

Equality of Descending and Ascending Factorials: $(n + k)^{\underline{k}} = (n + 1)^{\overline{k}}$

Informal description

For any natural numbers $n$ and $k$, the descending factorial of $n + k$ with parameter $k$ equals the ascending factorial of $n + 1$ with parameter $k$. That is: $$(n + k)^{\underline{k}} = (n + 1)^{\overline{k}}$$ where $n^{\underline{k}}$ denotes the descending factorial and $n^{\overline{k}}$ denotes the ascending factorial.

Nat.add_descFactorial_eq_ascFactorial' theorem

(n : ℕ) : ∀ k : ℕ, (n + k - 1).descFactorial k = n.ascFactorial k

Full source

theorem add_descFactorial_eq_ascFactorial' (n : ℕ) :
    ∀ k : ℕ, (n + k - 1).descFactorial k = n.ascFactorial k
  | 0 => by rw [ascFactorial_zero, descFactorial_zero]
  | succ k => by
    rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ,
      add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
      Nat.add_sub_cancel]

Equality of Shifted Descending and Ascending Factorials: $(n + k - 1)^{\underline{k}} = n^{\overline{k}}$

Informal description

For any natural numbers $n$ and $k$, the descending factorial of $n + k - 1$ with parameter $k$ equals the ascending factorial of $n$ with parameter $k$. That is: $$(n + k - 1)^{\underline{k}} = n^{\overline{k}}$$ where $n^{\underline{k}}$ denotes the descending factorial and $n^{\overline{k}}$ denotes the ascending factorial.

Nat.factorial_mul_descFactorial theorem

: ∀ {n k : ℕ}, k ≤ n → (n - k)! * n.descFactorial k = n !

Full source

/-- `n.descFactorial k = n! / (n - k)!` but without ℕ-division. See `Nat.descFactorial_eq_div`
for the version using ℕ-division. -/
theorem factorial_mul_descFactorial : ∀ {n k : ℕ}, k ≤ n → (n - k)! * n.descFactorial k = n !
  | n, 0 => fun _ => by rw [descFactorial_zero, Nat.mul_one, Nat.sub_zero]
  | 0, succ k => fun h => by
    exfalso
    exact not_succ_le_zero k h
  | succ n, succ k => fun h => by
    rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!,
      Nat.mul_assoc, factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]

Factorial-Descending Factorial Product Identity: $(n-k)! \cdot n^{\underline{k}} = n!$

Informal description

For any natural numbers $n$ and $k$ with $k \leq n$, the product of the factorial of $n - k$ and the descending factorial $n^{\underline{k}}$ equals the factorial of $n$, i.e., $$(n - k)! \cdot n^{\underline{k}} = n!$$ where $n^{\underline{k}} = n \cdot (n-1) \cdot \ldots \cdot (n-k+1)$ is the descending factorial.

Nat.descFactorial_mul_descFactorial theorem

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

Full source

theorem descFactorial_mul_descFactorial {k m n : ℕ} (hkm : k ≤ m) :
    (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m := by
  by_cases hmn : m ≤ n
  · apply Nat.mul_left_cancel (n - m).factorial_pos
    rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by omega, ← Nat.mul_assoc,
      factorial_mul_descFactorial (show m - k ≤ n - k by omega),
      factorial_mul_descFactorial (le_trans hkm hmn)]
  · rw [descFactorial_eq_zero_iff_lt.mpr (show n < m by omega)]
    by_cases hkn : k ≤ n
    · rw [descFactorial_eq_zero_iff_lt.mpr (show n - k < m - k by omega), Nat.zero_mul]
    · rw [descFactorial_eq_zero_iff_lt.mpr (show n < k by omega), Nat.mul_zero]

Descending Factorial Product Identity: $(n - k)^{\underline{m - k}} \cdot n^{\underline{k}} = n^{\underline{m}}$

Informal description

For any natural numbers $k, m, n$ with $k \leq m$, the product of the descending factorial $(n - k)^{\underline{m - k}}$ and $n^{\underline{k}}$ equals $n^{\underline{m}}$, i.e., $$(n - k)^{\underline{m - k}} \cdot n^{\underline{k}} = n^{\underline{m}}$$ where $n^{\underline{k}}$ denotes the descending factorial of $n$ with parameter $k$.

Nat.descFactorial_eq_div theorem

{n k : ℕ} (h : k ≤ n) : n.descFactorial k = n ! / (n - k)!

Full source

/-- Avoid in favor of `Nat.factorial_mul_descFactorial` if you can. ℕ-division isn't worth it. -/
theorem descFactorial_eq_div {n k : ℕ} (h : k ≤ n) : n.descFactorial k = n ! / (n - k)! := by
  apply Nat.mul_left_cancel (n - k).factorial_pos
  rw [factorial_mul_descFactorial h]
  exact (Nat.mul_div_cancel' <| factorial_dvd_factorial <| Nat.sub_le n k).symm

Descending Factorial as Quotient of Factorials: $n^{\underline{k}} = \frac{n!}{(n - k)!}$

Informal description

For any natural numbers $n$ and $k$ with $k \leq n$, the descending factorial $n^{\underline{k}}$ equals the quotient of the factorial of $n$ divided by the factorial of $n - k$, i.e., $$ n^{\underline{k}} = \frac{n!}{(n - k)!} $$ where $n^{\underline{k}} = n \cdot (n-1) \cdot \ldots \cdot (n-k+1)$ is the descending factorial.

Nat.descFactorial_le theorem

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

Full source

theorem descFactorial_le (n : ℕ) {k m : ℕ} (h : k ≤ m) :
    k.descFactorial n ≤ m.descFactorial n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [descFactorial_succ, descFactorial_succ]
    exact Nat.mul_le_mul (Nat.sub_le_sub_right h n) ih

Monotonicity of Descending Factorial: $k^{\underline{n}} \leq m^{\underline{n}}$ for $k \leq m$

Informal description

For any natural numbers $n$, $k$, and $m$ such that $k \leq m$, the descending factorial satisfies the inequality: $$ k^{\underline{n}} \leq m^{\underline{n}} $$ where $k^{\underline{n}}$ denotes the descending factorial of $k$ and $n$.

Nat.pow_sub_le_descFactorial theorem

(n : ℕ) : ∀ k : ℕ, (n + 1 - k) ^ k ≤ n.descFactorial k

Full source

theorem pow_sub_le_descFactorial (n : ℕ) : ∀ k : ℕ, (n + 1 - k) ^ k ≤ n.descFactorial k
  | 0 => by rw [descFactorial_zero, Nat.pow_zero]
  | k + 1 => by
    rw [descFactorial_succ, Nat.pow_succ, succ_sub_succ, Nat.mul_comm]
    apply Nat.mul_le_mul_left
    exact (le_trans (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) k)
      (pow_sub_le_descFactorial n k))

Power bound for descending factorial: $(n+1-k)^k \leq n^{\underline{k}}$

Informal description

For any natural numbers $n$ and $k$, the descending factorial $n^{\underline{k}}$ satisfies the inequality: $$(n + 1 - k)^k \leq n^{\underline{k}}$$ where $n^{\underline{k}} = n \cdot (n-1) \cdot \ldots \cdot (n-k+1)$ is the descending factorial.

Nat.pow_sub_lt_descFactorial' theorem

{n : ℕ} : ∀ {k : ℕ}, k + 2 ≤ n → (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Full source

theorem pow_sub_lt_descFactorial' {n : ℕ} :
    ∀ {k : ℕ}, k + 2 ≤ n → (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
  | 0, h => by
    rw [descFactorial_succ, Nat.pow_succ, Nat.pow_one, descFactorial_one]
    exact Nat.mul_lt_mul_of_pos_left (by omega) (Nat.sub_pos_of_lt h)
  | k + 1, h => by
    rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm]
    refine Nat.mul_lt_mul_of_pos_left ?_ (Nat.sub_pos_of_lt h)
    refine Nat.lt_of_le_of_lt (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) _) ?_
    rw [succ_sub_succ]
    exact pow_sub_lt_descFactorial' (Nat.le_trans (le_succ _) h)

Strict power bound for descending factorial: $(n-k-1)^{k+2} < n^{\underline{k+2}}$

Informal description

For any natural numbers $n$ and $k$ such that $k + 2 \leq n$, we have the strict inequality: $$(n - (k + 1))^{k + 2} < n^{\underline{k + 2}}$$ where $n^{\underline{k}}$ denotes the descending factorial of $n$ and $k$.

Nat.pow_sub_lt_descFactorial theorem

{n : ℕ} : ∀ {k : ℕ}, 2 ≤ k → k ≤ n → (n + 1 - k) ^ k < n.descFactorial k

Full source

theorem pow_sub_lt_descFactorial {n : ℕ} :
    ∀ {k : ℕ}, 2 ≤ k → k ≤ n → (n + 1 - k) ^ k < n.descFactorial k
  | 0 => by rintro ⟨⟩
  | 1 => by intro; contradiction
  | k + 2 => fun _ h => by
    rw [succ_sub_succ]
    exact pow_sub_lt_descFactorial' h

Strict inequality: $(n+1-k)^k < n^{\underline{k}}$ for $2 \leq k \leq n$

Informal description

For any natural numbers $n$ and $k$ such that $2 \leq k \leq n$, the following strict inequality holds: $$(n + 1 - k)^k < n^{\underline{k}}$$ where $n^{\underline{k}}$ denotes the descending factorial of $n$ and $k$.

Nat.descFactorial_le_pow theorem

(n : ℕ) : ∀ k : ℕ, n.descFactorial k ≤ n ^ k

Full source

theorem descFactorial_le_pow (n : ℕ) : ∀ k : ℕ, n.descFactorial k ≤ n ^ k
  | 0 => by rw [descFactorial_zero, Nat.pow_zero]
  | k + 1 => by
    rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm _ n]
    exact Nat.mul_le_mul (Nat.sub_le _ _) (descFactorial_le_pow _ k)

Descending factorial bound: $n^{\underline{k}} \leq n^k$

Informal description

For any natural numbers $n$ and $k$, the descending factorial $n^{\underline{k}}$ is less than or equal to $n^k$, i.e., $$ n^{\underline{k}} \leq n^k. $$

Nat.descFactorial_lt_pow theorem

{n : ℕ} (hn : 1 ≤ n) : ∀ {k : ℕ}, 2 ≤ k → n.descFactorial k < n ^ k

Full source

theorem descFactorial_lt_pow {n : ℕ} (hn : 1 ≤ n) : ∀ {k : ℕ}, 2 ≤ k → n.descFactorial k < n ^ k
  | 0 => by rintro ⟨⟩
  | 1 => by intro; contradiction
  | k + 2 => fun _ => by
    rw [descFactorial_succ, pow_succ', Nat.mul_comm, Nat.mul_comm n]
    exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (Nat.sub_lt hn k.zero_lt_succ)
      (Nat.pow_pos (Nat.lt_of_succ_le hn))

Strict Inequality for Descending Factorial: $n^{\underline{k}} < n^k$ when $n \geq 1$ and $k \geq 2$

Informal description

For any natural number $n \geq 1$ and any natural number $k \geq 2$, the descending factorial $n^{\underline{k}}$ is strictly less than $n^k$, i.e., $$ n^{\underline{k}} < n^k. $$

Nat.factorial_two_mul_le theorem

(n : ℕ) : (2 * n)! ≤ (2 * n) ^ n * n !

Full source

lemma factorial_two_mul_le (n : ℕ) : (2 * n)! ≤ (2 * n) ^ n * n ! := by
  rw [Nat.two_mul, ← factorial_mul_ascFactorial, Nat.mul_comm]
  exact Nat.mul_le_mul_right _ (ascFactorial_le_pow_add _ _)

Upper bound for $(2n)!$: $(2n)! \leq (2n)^n \cdot n!$

Informal description

For any natural number $n$, the factorial of $2n$ satisfies the inequality: $$(2n)! \leq (2n)^n \cdot n!$$

Nat.two_pow_mul_factorial_le_factorial_two_mul theorem

(n : ℕ) : 2 ^ n * n ! ≤ (2 * n)!

Full source

lemma two_pow_mul_factorial_le_factorial_two_mul (n : ℕ) : 2 ^ n * n ! ≤ (2 * n) ! := by
  obtain _ | n := n
  · simp
  rw [Nat.mul_comm, Nat.two_mul]
  calc
    _ ≤ (n + 1)! * (n + 2) ^ (n + 1) :=
      Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (le_add_left _ _) _)
    _ ≤ _ := Nat.factorial_mul_pow_le_factorial

Factorial-Power Inequality: $2^n \cdot n! \leq (2n)!$

Informal description

For any natural number $n$, the product of $2^n$ and the factorial of $n$ is less than or equal to the factorial of $2n$, i.e., \[ 2^n \cdot n! \leq (2n)! \]

Main declarations