Double factorials

This file defines the double factorial, n‼ := n * (n - 2) * (n - 4) * ....

Main declarations

• Nat.doubleFactorial: The double factorial.

def Nat.doubleFactorial : ℕ → ℕ

Nat.doubleFactorial n is the double factorial of n.

Equations

• Nat.doubleFactorial 0 = 1
• Nat.doubleFactorial 1 = 1
• k.succ.succ.doubleFactorial = (k + 2) * k.doubleFactorial

def Nat.«term_‼» : Lean.TrailingParserDescr

Nat.doubleFactorial n is the double factorial of n.

Equations

• Nat.«term_‼» = Lean.ParserDescr.trailingNode `Nat.«term_‼» 10000 0 (Lean.ParserDescr.symbol "‼")

theorem Nat.doubleFactorial_pos (n : ℕ) : 0 < n.doubleFactorial

theorem Nat.doubleFactorial_add_two (n : ℕ) : (n + 2).doubleFactorial = (n + 2) * n.doubleFactorial

theorem Nat.doubleFactorial_add_one (n : ℕ) : (n + 1).doubleFactorial = (n + 1) * (n - 1).doubleFactorial

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

theorem Nat.doubleFactorial_le_factorial (n : ℕ) : n.doubleFactorial ≤ n.factorial

theorem Nat.doubleFactorial_two_mul (n : ℕ) : (2 * n).doubleFactorial = 2 ^ n * n.factorial

theorem Nat.doubleFactorial_eq_prod_even (n : ℕ) : (2 * n).doubleFactorial = ∏ i ∈ Finset.range n, 2 * (i + 1)

theorem Nat.doubleFactorial_eq_prod_odd (n : ℕ) : (2 * n + 1).doubleFactorial = ∏ i ∈ Finset.range n, (2 * (i + 1) + 1)

def Mathlib.Meta.Positivity.evalDoubleFactorial : PositivityExt

Extension for Nat.doubleFactorial.