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
• Nat.doubleFactorial (Nat.succ (Nat.succ k)) = (k + 2) * Nat.doubleFactorial k

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 < Nat.doubleFactorial n

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

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

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

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

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

theorem Nat.doubleFactorial_eq_prod_even (n : ℕ) : Nat.doubleFactorial (2 * n) = Finset.prod (Finset.range n) fun (i : ℕ) => 2 * (i + 1)

theorem Nat.doubleFactorial_eq_prod_odd (n : ℕ) : Nat.doubleFactorial (2 * n + 1) = Finset.prod (Finset.range n) fun (i : ℕ) => 2 * (i + 1) + 1

def Mathlib.Meta.Positivity.evalDoubleFactorial : Mathlib.Meta.Positivity.PositivityExt

Extension for Nat.doubleFactorial.