FiboCatalan numbers

DefinitionFibonacci factorial#✓fully proved

For a natural number \(n\), the Fibonacci factorial \(F_n!\) is the rational number \(F_n! = F_1 F_2 \cdots F_n\), the product of the first \(n\) Fibonacci numbers (where \(F_1 = F_2 = 1\) and \(F_{k+2} = F_{k+1} + F_k\)); in particular \(F_0! = 1\), the empty product.

Values are taken in \(\mathbb{Q}\) so that quotients of Fibonacci factorials are exact rather than truncated by natural-number division.

def fibonacciFactorial : ℕ → ℚ
  | 0 => 1
  | n + 1 => fibonacciFactorial n * (Nat.fib (n + 1) : ℚ)

Used by 21

TheoremFibonacci factorial at zero#✓fully proved

The Fibonacci factorial \(F_0!\) equals \(1\), by the empty-product convention.

theorem fibonacciFactorial_zero :
    fibonacciFactorial 0 = 1

Uses 1 · Used by 2

Statement usesFibonacci factorial

Used byFibonacci factorial at one · Fibonacci Jordan quotient at zero

TheoremFibonacci factorials are positive#✓fully proved

For every natural number \(n\), the Fibonacci factorial \(F_n!\) is a strictly positive rational number.

theorem fibonacciFactorial_pos (n : ℕ) :
    0 < fibonacciFactorial n

Uses 1 · Used by 3

Statement usesFibonacci factorial

Used byFibonacci factorials are nonzero · Fibonacci Jordan quotient is positive · Positivity of generalized FiboCatalan numbers

TheoremFibonacci factorials are nonzero#✓fully proved

For every natural number \(n\), the Fibonacci factorial \(F_n!\) is a nonzero rational number.

theorem fibonacciFactorial_ne (n : ℕ) :
    fibonacciFactorial n ≠ 0

Uses 2

Statement usesFibonacci factorial

Proof usesFibonacci factorials are positive

TheoremFibonacci factorial at one#✓fully proved

The Fibonacci factorial \(F_1!\) equals \(1\), since the first Fibonacci number is \(F_1 = 1\).

theorem fibonacciFactorial_one :
    fibonacciFactorial 1 = 1

Uses 2 · Used by 3

Statement usesFibonacci factorial

Proof usesFibonacci factorial at zero

Used byFibonacci factorial at two · Fibonacci Jordan quotient at zero · Fibonacci Jordan quotient at one

TheoremFibonacci factorial at two#✓fully proved

The Fibonacci factorial \(F_2! = F_1 F_2\) of the Fibonacci numbers \(F_1, F_2\) equals \(1\), since \(F_1 = F_2 = 1\).

theorem fibonacciFactorial_two :
    fibonacciFactorial 2 = 1

Uses 2 · Used by 1

Statement usesFibonacci factorial

Proof usesFibonacci factorial at one

Used byFibonacci factorial at three

TheoremFibonacci factorial at three#✓fully proved

The Fibonacci factorial \(F_3! = F_1 F_2 F_3\) of the Fibonacci numbers \(F_1, F_2, F_3\) equals \(2\), since \(F_1 = F_2 = 1\) and \(F_3 = 2\).

theorem fibonacciFactorial_three :
    fibonacciFactorial 3 = 2

Uses 2 · Used by 1

Statement usesFibonacci factorial

Proof usesFibonacci factorial at two

Used byFibonacci Jordan quotient at one

DefinitionFibonacci Jordan quotient#✓fully proved

For a natural number \(r\), the Jordan-type quotient is the rational number \(J_{r,F} = F_{2r+1}! / F_r!\), where \(F_m! = F_1 F_2 \cdots F_m\) is the Fibonacci factorial of the Fibonacci numbers \(F_1 = F_2 = 1\), \(F_{k+2} = F_{k+1} + F_k\) (so \(F_0! = 1\)).

def fibonacciJordanQuotient (r : ℕ) : ℚ :=
  fibonacciFactorial (2 * r + 1) / fibonacciFactorial r

Uses 1 · Used by 8

Statement usesFibonacci factorial

Used byFibonacci Jordan quotient is positive · Fibonacci Jordan quotient at zero · Fibonacci Jordan quotient at one · Generalized FiboCatalan numbers · Generalized FiboCatalan numbers are positive integers · Positivity of generalized FiboCatalan numbers · Generalized FiboCatalan numbers at r = 0 · Generalized FiboCatalan numbers at r = 1

TheoremFibonacci Jordan quotient is positive#✓fully proved

For every natural number \(r\), the Jordan-type quotient \(J_{r,F} = F_{2r+1}! / F_r!\) of Fibonacci factorials is a strictly positive rational number.

theorem fibonacciJordanQuotient_pos (r : ℕ) :
    0 < fibonacciJordanQuotient r

Uses 3 · Used by 1

Statement usesFibonacci Jordan quotient

Proof usesFibonacci factorial · Fibonacci factorials are positive

Used byPositivity of generalized FiboCatalan numbers

TheoremFibonacci Jordan quotient at zero#✓fully proved

The Jordan-type quotient \(J_{r,F} = F_{2r+1}! / F_r!\) of Fibonacci factorials takes the value \(J_{0,F} = F_1! / F_0! = 1\).

theorem fibonacciJordanQuotient_r0 :
    fibonacciJordanQuotient 0 = 1

Uses 4 · Used by 1

Statement usesFibonacci Jordan quotient

Proof usesFibonacci factorial · Fibonacci factorial at one · Fibonacci factorial at zero

Used byGeneralized FiboCatalan numbers at r = 0

TheoremFibonacci Jordan quotient at one#✓fully proved

The Jordan-type quotient \(J_{r,F} = F_{2r+1}! / F_r!\) of Fibonacci factorials takes the value \(J_{1,F} = F_3! / F_1! = 2\).

theorem fibonacciJordanQuotient_r1 :
    fibonacciJordanQuotient 1 = 2

Uses 4 · Used by 1

Statement usesFibonacci Jordan quotient

Proof usesFibonacci factorial · Fibonacci factorial at one · Fibonacci factorial at three

Used byGeneralized FiboCatalan numbers at r = 1

DefinitionGeneralized FiboCatalan numbers#✓fully proved

Let \(F_m! = F_1 F_2 \cdots F_m\) denote the Fibonacci factorial of the Fibonacci numbers \(F_1 = F_2 = 1\), \(F_{k+2} = F_{k+1} + F_k\) (so \(F_0! = 1\)), and let \(J_{r,F} = F_{2r+1}! / F_r!\) be the Fibonacci Jordan quotient. For natural numbers \(r\) and \(n\), the generalized FiboCatalan number with parameters \(r\) and \(n\) is the rational number \(J_{r,F} \, F_{2n}! / (F_n! \, F_{n+r+1}!)\).

def generalizedFibonacciCatalan (r n : ℕ) : ℚ :=
  fibonacciJordanQuotient r * fibonacciFactorial (2 * n) /
    (fibonacciFactorial n * fibonacciFactorial (n + r + 1))

def fibonacciJordanQuotient (r : ℕ) : ℚ :=
  fibonacciFactorial (2 * r + 1) / fibonacciFactorial r

MathlibExt/NumberTheory/GeneralizedFibocatalanNumber.lean:93

def fibonacciFactorial : ℕ → ℚ
  | 0 => 1
  | n + 1 => fibonacciFactorial n * (Nat.fib (n + 1) : ℚ)

MathlibExt/NumberTheory/GeneralizedFibocatalanNumber.lean:43

Uses 2 · Used by 4

Statement usesFibonacci factorial · Fibonacci Jordan quotient

Used byGeneralized FiboCatalan numbers are positive integers · Positivity of generalized FiboCatalan numbers · Generalized FiboCatalan numbers at r = 0 · Generalized FiboCatalan numbers at r = 1

TheoremPositivity of generalized FiboCatalan numbers#✓fully proved

For all natural numbers \(r\) and \(n\), the generalized FiboCatalan number with parameters \(r\) and \(n\) is a strictly positive rational number.

theorem generalizedFibonacciCatalan_pos (r n : ℕ) :
    0 < generalizedFibonacciCatalan r n

def generalizedFibonacciCatalan (r n : ℕ) : ℚ :=
  fibonacciJordanQuotient r * fibonacciFactorial (2 * n) /
    (fibonacciFactorial n * fibonacciFactorial (n + r + 1))

MathlibExt/NumberTheory/GeneralizedFibocatalanNumber.lean:122

Uses 5

Statement usesGeneralized FiboCatalan numbers

Proof usesFibonacci factorial · Fibonacci factorials are positive · Fibonacci Jordan quotient · Fibonacci Jordan quotient is positive

TheoremGeneralized FiboCatalan numbers are positive integers#✓fully proved

For all natural numbers \(r\) and \(n\), the generalized FiboCatalan number with parameters \(r\) and \(n\) is a positive integer: it equals \(k\) for some natural number \(k \ge 1\).

theorem generalizedFibonacciCatalan_isPosInt (r n : ℕ) :
    ∃ k : ℕ, 0 < k ∧ (k : ℚ) = generalizedFibonacciCatalan r n

def generalizedFibonacciCatalan (r n : ℕ) : ℚ :=
  fibonacciJordanQuotient r * fibonacciFactorial (2 * n) /
    (fibonacciFactorial n * fibonacciFactorial (n + r + 1))

MathlibExt/NumberTheory/GeneralizedFibocatalanNumber.lean:122

Uses 3

Statement usesGeneralized FiboCatalan numbers

Proof usesFibonacci factorial · Fibonacci Jordan quotient

TheoremGeneralized FiboCatalan numbers at r = 0#✓fully proved

For every natural number \(n\), the generalized FiboCatalan number with parameters \(r = 0\) and \(n\) equals the FiboCatalan number \(F_{2n}! / (F_n! \, F_{n+1}!)\), where \(F_i\) is the \(i\)-th Fibonacci number (\(F_1 = F_2 = 1\)) and \(F_m! = F_1 F_2 \cdots F_m\) is the Fibonacci factorial (with \(F_0! = 1\)).

theorem generalizedFibonacciCatalan_r0 (n : ℕ) :
    generalizedFibonacciCatalan 0 n =
      fibonacciFactorial (2 * n) /
        (fibonacciFactorial n * fibonacciFactorial (n + 1))

def generalizedFibonacciCatalan (r n : ℕ) : ℚ :=
  fibonacciJordanQuotient r * fibonacciFactorial (2 * n) /
    (fibonacciFactorial n * fibonacciFactorial (n + r + 1))

MathlibExt/NumberTheory/GeneralizedFibocatalanNumber.lean:122

def fibonacciFactorial : ℕ → ℚ
  | 0 => 1
  | n + 1 => fibonacciFactorial n * (Nat.fib (n + 1) : ℚ)

MathlibExt/NumberTheory/GeneralizedFibocatalanNumber.lean:43

Uses 4

Statement usesFibonacci factorial · Generalized FiboCatalan numbers

Proof usesFibonacci Jordan quotient · Fibonacci Jordan quotient at zero

TheoremGeneralized FiboCatalan numbers at r = 1#✓fully proved

For every natural number \(n\), the generalized FiboCatalan number with parameters \(r = 1\) and \(n\) equals \(2 F_{2n}! / (F_{n+2}! \, F_n!)\), where \(F_i\) is the \(i\)-th Fibonacci number (\(F_1 = F_2 = 1\)) and \(F_m! = F_1 F_2 \cdots F_m\) is the Fibonacci factorial (with \(F_0! = 1\)).

theorem generalizedFibonacciCatalan_r1 (n : ℕ) :
    generalizedFibonacciCatalan 1 n =
      2 * fibonacciFactorial (2 * n) /
        (fibonacciFactorial (n + 2) * fibonacciFactorial n)

def generalizedFibonacciCatalan (r n : ℕ) : ℚ :=
  fibonacciJordanQuotient r * fibonacciFactorial (2 * n) /
    (fibonacciFactorial n * fibonacciFactorial (n + r + 1))

MathlibExt/NumberTheory/GeneralizedFibocatalanNumber.lean:122

def fibonacciFactorial : ℕ → ℚ
  | 0 => 1
  | n + 1 => fibonacciFactorial n * (Nat.fib (n + 1) : ℚ)

MathlibExt/NumberTheory/GeneralizedFibocatalanNumber.lean:43

Uses 4

Statement usesFibonacci factorial · Generalized FiboCatalan numbers

Proof usesFibonacci Jordan quotient · Fibonacci Jordan quotient at one

DefinitionFiboCatalan numbers#✓fully proved

For a natural number \(n\), the FiboCatalan number is the rational number \(C_{n,F} = F_{2n}!/(F_n! \, F_{n+1}!)\), where \(F_j\) is the \(j\)-th Fibonacci number and \(F_k! = F_1 F_2 \cdots F_k\) is the Fibonacci factorial.

noncomputable def fiboCatalan (n : ℕ) : ℚ :=
  fibonacciFactorial (2 * n) /
    (fibonacciFactorial n * fibonacciFactorial (n + 1))

Uses 1 · Used by 1

Statement usesFibonacci factorial

Used byAn identity between consecutive FiboCatalan numbers

DefinitionFibonomial coefficients#✓fully proved

For natural numbers \(n\) and \(k\), the fibonomial coefficient \(\binom{n}{k}_F\) is the rational number \(F_n!/(F_k! \, F_{n-k}!)\) when \(k \le n\), where \(F_i\) is the \(i\)-th Fibonacci number and \(F_j! = F_1 F_2 \cdots F_j\) is the Fibonacci factorial, and \(0\) when \(k > n\).

noncomputable def fibonomial (n k : ℕ) : ℚ :=
  if k ≤ n then
    fibonacciFactorial n /
      (fibonacciFactorial k * fibonacciFactorial (n - k))
  else 0

Uses 1 · Used by 1

Statement usesFibonacci factorial

Used byIntegrality of \(F_{2n+1} F_{2n}!/(F_{n+2}! \, F_n!)\)

TheoremSuper FiboCatalan numbers are positive integers#●ready to prove

For all natural numbers \(m\) and \(n\), the super FiboCatalan number

\[S(m, n)_F = \frac{F_{2m}!\, F_{2n}!}{F_m!\, F_n!\, F_{m+n}!},\]

where \(F_j!\) denotes the Fibonacci factorial, is a positive integer: it equals \(k\) for some natural number \(k \ge 1\).

theorem_wanted superFibonacciCatalan_isPosInt (m n : ℕ) :
    ∃ k : ℕ, 0 < k ∧ (k : ℚ) =
      fibonacciFactorial (2 * m) * fibonacciFactorial (2 * n) /
        (fibonacciFactorial m * fibonacciFactorial n *
          fibonacciFactorial (m + n))

Sources

Kendra Killpatrick, "Super FiboCatalan Numbers and Their Lucas Analogues", Corollary 5.

Uses 1

Statement usesFibonacci factorial

TheoremFibonacci identity \(F_{2n} F_{n+2} - F_{2n+2} F_n = (-1)^n F_n\)#●ready to prove

For every natural number \(n\), the Fibonacci numbers (\(F_0 = 0\), \(F_1 = 1\), \(F_{k+2} = F_{k+1} + F_k\)) satisfy \(F_{2n} F_{n+2} - F_{2n+2} F_n = (-1)^n F_n\).

theorem_wanted fib_mul_sub_mul (n : ℕ) :
    (Nat.fib (2 * n) : ℤ) * (Nat.fib (n + 2) : ℤ) -
        (Nat.fib (2 * n + 2) : ℤ) * (Nat.fib n : ℤ) =
      (-1) ^ n * (Nat.fib n : ℤ)

Sources

Kendra Killpatrick, "Super FiboCatalan Numbers and Their Lucas Analogues", Lemma 6.

TheoremAn identity between consecutive FiboCatalan numbers#●ready to prove

Let \(F_k\) be the Fibonacci numbers, \(F_k! = F_1 F_2 \cdots F_k\) the Fibonacci factorial and \(C_{k,F} = F_{2k}!/(F_k! \, F_{k+1}!)\) the FiboCatalan number. For every natural number \(n\), in \(\mathbb{Q}\),

\[F_{2n+1} F_{2n} C_{n,F} - F_{n+1} F_n C_{n+1,F} = (-1)^n F_n F_{2n+1} \frac{F_{2n}!}{F_{n+2}! \, F_n!}.\]

theorem_wanted fiboCatalan_identity (n : ℕ) :
    (Nat.fib (2 * n + 1) : ℚ) * (Nat.fib (2 * n) : ℚ) *
          fiboCatalan n -
        (Nat.fib (n + 1) : ℚ) * (Nat.fib n : ℚ) *
          fiboCatalan (n + 1) =
      (-1) ^ n * (Nat.fib n : ℚ) * (Nat.fib (2 * n + 1) : ℚ) *
        (fibonacciFactorial (2 * n) /
          (fibonacciFactorial (n + 2) * fibonacciFactorial n))

noncomputable def fiboCatalan (n : ℕ) : ℚ :=
  fibonacciFactorial (2 * n) /
    (fibonacciFactorial n * fibonacciFactorial (n + 1))

WantedExt/NumberTheory/SuperFibocatalanWanted.lean:59

def fibonacciFactorial : ℕ → ℚ
  | 0 => 1
  | n + 1 => fibonacciFactorial n * (Nat.fib (n + 1) : ℚ)

MathlibExt/NumberTheory/GeneralizedFibocatalanNumber.lean:43

Sources

Kendra Killpatrick, "Super FiboCatalan Numbers and Their Lucas Analogues", Theorem 7.

Uses 2

Statement usesFiboCatalan numbers · Fibonacci factorial

TheoremIntegrality of \(F_{2n+1} F_{2n}!/(F_{n+2}! \, F_n!)\)#●ready to prove

Let \(F_k\) be the Fibonacci numbers, \(F_k! = F_1 F_2 \cdots F_k\) the Fibonacci factorial and, for \(k \le m\), \(\binom{m}{k}_F = F_m!/(F_k! \, F_{m-k}!)\) the fibonomial coefficient. For every natural number \(n \ge 1\),

\[F_{2n+1} \frac{F_{2n}!}{F_{n+2}! \, F_n!} = \frac{1}{F_{n+2}} \binom{2n+1}{n}_F,\]

and this rational number is an integer.

theorem_wanted fib_mul_factorialQuotient_eq_and_isInt
    (n : ℕ) (hn : 1 ≤ n) :
    (Nat.fib (2 * n + 1) : ℚ) *
          (fibonacciFactorial (2 * n) /
            (fibonacciFactorial (n + 2) * fibonacciFactorial n)) =
        fibonomial (2 * n + 1) n / (Nat.fib (n + 2) : ℚ) ∧
      ∃ k : ℤ, (k : ℚ) =
        (Nat.fib (2 * n + 1) : ℚ) *
          (fibonacciFactorial (2 * n) /
            (fibonacciFactorial (n + 2) * fibonacciFactorial n))

def fibonacciFactorial : ℕ → ℚ
  | 0 => 1
  | n + 1 => fibonacciFactorial n * (Nat.fib (n + 1) : ℚ)

MathlibExt/NumberTheory/GeneralizedFibocatalanNumber.lean:43

noncomputable def fibonomial (n k : ℕ) : ℚ :=
  if k ≤ n then
    fibonacciFactorial n /
      (fibonacciFactorial k * fibonacciFactorial (n - k))
  else 0

WantedExt/NumberTheory/SuperFibocatalanWanted.lean:67

Sources

Kendra Killpatrick, "Super FiboCatalan Numbers and Their Lucas Analogues", Corollary 8.

Uses 2

Statement usesFibonomial coefficients · Fibonacci factorial

DefinitionLucas polynomials in \(s\) and \(t\)#✓fully proved

The Lucas polynomials \(\{n\}\), for natural numbers \(n\), are the polynomials in two variables \(s\) and \(t\) with integer coefficients defined by \(\{0\} = 0\), \(\{1\} = 1\) and \(\{n + 2\} = s\{n + 1\} + t\{n\}\) for every \(n \ge 0\).

noncomputable def lucasPoly : ℕ → MvPolynomial (Fin 2) ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => MvPolynomial.X 0 * lucasPoly (n + 1) +
      MvPolynomial.X 1 * lucasPoly n

Used by 5

Used byThe Lucas quotient \(\{2n+1\} \{2\} \{2n\}!/(\{n+2\}! \, \{n\}!)\) has non-negative coefficients · Lucas analogue of the FiboCatalan identity, cleared of denominators · Lucas factorial · \(k\)-divisible Lucas factorial · Cross-product identity for Lucas polynomials

DefinitionLucas factorial#✓fully proved

For a natural number \(n\), the Lucas factorial \(\{n\}!\) is the product \(\{n\}! = \{1\}\{2\} \cdots \{n\}\) of the Lucas polynomials \(\{i\}\) in \(s\) and \(t\) for \(1 \le i \le n\), a polynomial with integer coefficients; in particular \(\{0\}! = 1\), the empty product.

noncomputable def lucasFactorial (n : ℕ) : MvPolynomial (Fin 2) ℤ :=
  ∏ i ∈ Finset.Icc 1 n, lucasPoly i

noncomputable def lucasPoly : ℕ → MvPolynomial (Fin 2) ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => MvPolynomial.X 0 * lucasPoly (n + 1) +
      MvPolynomial.X 1 * lucasPoly n

WantedExt/NumberTheory/SuperFibocatalanWanted.lean:131

Uses 1 · Used by 4

Statement usesLucas polynomials in \(s\) and \(t\)

Used byLucas generalized FiboCatalan numbers have non-negative coefficients · The Lucas quotient \(\{2n+1\} \{2\} \{2n\}!/(\{n+2\}! \, \{n\}!)\) has non-negative coefficients · Lucas super FiboCatalan numbers have non-negative coefficients · Lucas analogue of the FiboCatalan identity, cleared of denominators

Definition\(k\)-divisible Lucas factorial#✓fully proved

For natural numbers \(k\) and \(n\), the \(k\)-divisible Lucas factorial \(\{n : k\}!\) is the product \(\{n : k\}! = \{k\}\{2k\} \cdots \{nk\}\) of the Lucas polynomials \(\{ki\}\) in \(s\) and \(t\) for \(1 \le i \le n\); in particular \(\{0 : k\}! = 1\), the empty product.

noncomputable def lucasKDivFactorial (k n : ℕ) :
    MvPolynomial (Fin 2) ℤ :=
  ∏ i ∈ Finset.Icc 1 n, lucasPoly (k * i)

noncomputable def lucasPoly : ℕ → MvPolynomial (Fin 2) ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => MvPolynomial.X 0 * lucasPoly (n + 1) +
      MvPolynomial.X 1 * lucasPoly n

WantedExt/NumberTheory/SuperFibocatalanWanted.lean:131

Uses 1 · Used by 1

Statement usesLucas polynomials in \(s\) and \(t\)

Used by\(k\)-divisible Lucas super Catalan numbers have non-negative coefficients

TheoremLucas super FiboCatalan numbers have non-negative coefficients#●ready to prove

Let \(\{k\}\) be the Lucas polynomials in \(s\) and \(t\) (\(\{0\} = 0\), \(\{1\} = 1\), \(\{k+2\} = s\{k+1\} + t\{k\}\)) and let \(\{k\}! = \{1\}\{2\} \cdots \{k\}\) be the Lucas factorial. For all natural numbers \(m\) and \(n\) there is a polynomial \(p \in \mathbb{Z}[s, t]\) with non-negative coefficients such that \(p \, \{m\}! \, \{n\}! \, \{m+n\}! = \{2m\}! \, \{2n\}!\); that is, the Lucas analogue \(S\{m, n\} = \{2m\}! \, \{2n\}!/(\{m\}! \, \{n\}! \, \{m+n\}!)\) of the super FiboCatalan number is a polynomial in \(s\) and \(t\) with non-negative integer coefficients.

theorem_wanted exists_nonneg_poly_superLucasCatalan (m n : ℕ) :
    ∃ p : MvPolynomial (Fin 2) ℤ,
      (∀ σ : Fin 2 →₀ ℕ, 0 ≤ p.coeff σ) ∧
      p * (lucasFactorial m * lucasFactorial n *
          lucasFactorial (m + n)) =
        lucasFactorial (2 * m) * lucasFactorial (2 * n)

Sources

Kendra Killpatrick, "Super FiboCatalan Numbers and Their Lucas Analogues", Theorem 3.

Uses 1

Statement usesLucas factorial

TheoremLucas generalized FiboCatalan numbers have non-negative coefficients#●ready to prove

Let \(\{k\}\) be the Lucas polynomials in \(s\) and \(t\) (\(\{0\} = 0\), \(\{1\} = 1\), \(\{k+2\} = s\{k+1\} + t\{k\}\)) and let \(\{k\}! = \{1\}\{2\} \cdots \{k\}\) be the Lucas factorial. For all natural numbers \(r\) and \(n\) there is a polynomial \(p \in \mathbb{Z}[s, t]\) with non-negative coefficients such that \(p \, \{r\}! \, \{n\}! \, \{n+r+1\}! = \{2r+1\}! \, \{2n\}!\); that is, with \(J_{\{r\}} = \{2r+1\}!/\{r\}!\), the Lucas analogue \(J_{\{r\}} \, \{2n\}!/(\{n\}! \, \{n+r+1\}!)\) of the generalized FiboCatalan number is a polynomial in \(s\) and \(t\) with non-negative integer coefficients.

theorem_wanted exists_nonneg_poly_generalizedLucasCatalan
    (r n : ℕ) :
    ∃ p : MvPolynomial (Fin 2) ℤ,
      (∀ σ : Fin 2 →₀ ℕ, 0 ≤ p.coeff σ) ∧
      p * (lucasFactorial r * lucasFactorial n *
          lucasFactorial (n + r + 1)) =
        lucasFactorial (2 * r + 1) * lucasFactorial (2 * n)

Sources

Kendra Killpatrick, "Super FiboCatalan Numbers and Their Lucas Analogues", Theorem 4.

Uses 1

Statement usesLucas factorial

TheoremCross-product identity for Lucas polynomials#●ready to prove

For every natural number \(n\), the Lucas polynomials \(\{k\}\) in \(s\) and \(t\) satisfy \(\{2n\}\{n + 2\} - \{2n + 2\}\{n\} = (-1)^n \{2\} t^n \{n\}\).

theorem_wanted lucasPoly_mul_sub_mul (n : ℕ) :
    lucasPoly (2 * n) * lucasPoly (n + 2) -
        lucasPoly (2 * n + 2) * lucasPoly n =
      (-1) ^ n * lucasPoly 2 * MvPolynomial.X 1 ^ n * lucasPoly n

noncomputable def lucasPoly : ℕ → MvPolynomial (Fin 2) ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => MvPolynomial.X 0 * lucasPoly (n + 1) +
      MvPolynomial.X 1 * lucasPoly n

WantedExt/NumberTheory/SuperFibocatalanWanted.lean:131

Sources

Kendra Killpatrick, "Super FiboCatalan Numbers and Their Lucas Analogues", Lemma 10.

Uses 1

Statement usesLucas polynomials in \(s\) and \(t\)

TheoremLucas analogue of the FiboCatalan identity, cleared of denominators#●ready to prove

Let \(\{k\}\) be the Lucas polynomials in \(s\) and \(t\) (\(\{0\} = 0\), \(\{1\} = 1\), \(\{k+2\} = s\{k+1\} + t\{k\}\)) and let \(\{k\}! = \{1\}\{2\} \cdots \{k\}\) be the Lucas factorial. For every natural number \(n\), in \(\mathbb{Z}[s, t]\),

\[(\{2n+1\} \{2n\} \{n+2\} - \{2n+2\} \{2n+1\} \{n\}) \, \{2n\}! = (-1)^n t^n \{2\} \{n\} \{2n+1\} \, \{2n\}!.\]

With the Lucas Catalan numbers \(C_{\{k\}} = \{2k\}!/(\{k\}! \, \{k+1\}!)\), this is the identity

\[\{2n+1\} \{2n\} C_{\{n\}} - \{n+1\} \{n\} C_{\{n+1\}} = (-1)^n t^n \{2\} \{n\} \{2n+1\} \frac{\{2n\}!}{\{n+2\}! \, \{n\}!}\]

multiplied through by \(\{n+2\}! \, \{n\}!\).

theorem_wanted lucasCatalan_identity_mul_factorial (n : ℕ) :
    (lucasPoly (2 * n + 1) * lucasPoly (2 * n) * lucasPoly (n + 2) -
        lucasPoly (2 * n + 2) * lucasPoly (2 * n + 1) *
          lucasPoly n) * lucasFactorial (2 * n) =
      (-1) ^ n * MvPolynomial.X 1 ^ n * lucasPoly 2 *
        lucasPoly n * lucasPoly (2 * n + 1) *
        lucasFactorial (2 * n)

noncomputable def lucasPoly : ℕ → MvPolynomial (Fin 2) ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => MvPolynomial.X 0 * lucasPoly (n + 1) +
      MvPolynomial.X 1 * lucasPoly n

WantedExt/NumberTheory/SuperFibocatalanWanted.lean:131

noncomputable def lucasFactorial (n : ℕ) : MvPolynomial (Fin 2) ℤ :=
  ∏ i ∈ Finset.Icc 1 n, lucasPoly i

WantedExt/NumberTheory/SuperFibocatalanWanted.lean:139

Sources

Kendra Killpatrick, "Super FiboCatalan Numbers and Their Lucas Analogues", Theorem 11.

Uses 2

Statement usesLucas factorial · Lucas polynomials in \(s\) and \(t\)

TheoremThe Lucas quotient \(\{2n+1\} \{2\} \{2n\}!/(\{n+2\}! \, \{n\}!)\) has non-negative coefficients#●ready to prove

The Lucas quotient \(\{2n+1\} \{2\} \{2n\}!/(\{n+2\}! \, \{n\}!)\) has non-negative coefficients. Let \(\{k\}\) be the Lucas polynomials in \(s\) and \(t\) (\(\{0\} = 0\), \(\{1\} = 1\), \(\{k+2\} = s\{k+1\} + t\{k\}\)) and let \(\{k\}! = \{1\}\{2\} \cdots \{k\}\) be the Lucas factorial. For every natural number \(n \ge 1\),

\[\{n+2\} \, \{2n+1\} \, \{2n\}! \, \{n\}! \, \{n+1\}! = \{n+2\}! \, \{n\}! \, \{2n+1\}!,\]

and there is a polynomial \(p \in \mathbb{Z}[s, t]\) with non-negative coefficients such that \(p \, \{n+2\}! \, \{n\}! = \{2n+1\} \, \{2\} \, \{2n\}!\). That is, the quotient \(\{2n+1\} \{2\} \{2n\}!/(\{n+2\}! \, \{n\}!)\), which by the first identity equals \(\{2\} \, \frac{1}{\{n+2\}} \, \{2n+1\}!/(\{n\}! \, \{n+1\}!)\), is a polynomial in \(s\) and \(t\) with non-negative integer coefficients.

theorem_wanted exists_nonneg_poly_lucasQuotient (n : ℕ)
    (hn : 1 ≤ n) :
    lucasPoly (n + 2) *
          (lucasPoly (2 * n + 1) * lucasFactorial (2 * n)) *
        (lucasFactorial n * lucasFactorial (n + 1)) =
      (lucasFactorial (n + 2) * lucasFactorial n) *
        lucasFactorial (2 * n + 1) ∧
    ∃ p : MvPolynomial (Fin 2) ℤ,
      (∀ σ : Fin 2 →₀ ℕ, 0 ≤ p.coeff σ) ∧
      p * (lucasFactorial (n + 2) * lucasFactorial n) =
        lucasPoly (2 * n + 1) * lucasPoly 2 *
          lucasFactorial (2 * n)

noncomputable def lucasPoly : ℕ → MvPolynomial (Fin 2) ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => MvPolynomial.X 0 * lucasPoly (n + 1) +
      MvPolynomial.X 1 * lucasPoly n

WantedExt/NumberTheory/SuperFibocatalanWanted.lean:131

noncomputable def lucasFactorial (n : ℕ) : MvPolynomial (Fin 2) ℤ :=
  ∏ i ∈ Finset.Icc 1 n, lucasPoly i

WantedExt/NumberTheory/SuperFibocatalanWanted.lean:139

Sources

Kendra Killpatrick, "Super FiboCatalan Numbers and Their Lucas Analogues", Corollary 12.

Uses 2

Statement usesLucas factorial · Lucas polynomials in \(s\) and \(t\)

Theorem\(k\)-divisible Lucas super Catalan numbers have non-negative coefficients#●ready to prove

Let \(\{j\}\) be the Lucas polynomials in \(s\) and \(t\) (\(\{0\} = 0\), \(\{1\} = 1\), \(\{j+2\} = s\{j+1\} + t\{j\}\)) and let \(\{n : k\}! = \{k\}\{2k\} \cdots \{nk\}\) be the \(k\)-divisible Lucas factorial. For all natural numbers \(k\), \(m\) and \(n\) with \(k \ge 1\) there is a polynomial \(p \in \mathbb{Z}[s, t]\) with non-negative coefficients such that

\[p \, \{m : k\}! \, \{n : k\}! \, \{m+n : k\}! = \{2m : k\}! \, \{2n : k\}!;\]

that is, the \(k\)-divisible lucanomial analogue \(S\{m, n : k\} = \{2m : k\}! \, \{2n : k\}!/(\{m : k\}! \, \{n : k\}! \, \{m+n : k\}!)\) of the super Catalan numbers is a polynomial in \(s\) and \(t\) with non-negative integer coefficients.

theorem_wanted exists_nonneg_poly_kDivLucasCatalan
    (k m n : ℕ) (hk : 1 ≤ k) :
    ∃ p : MvPolynomial (Fin 2) ℤ,
      (∀ σ : Fin 2 →₀ ℕ, 0 ≤ p.coeff σ) ∧
      p * (lucasKDivFactorial k m * lucasKDivFactorial k n *
          lucasKDivFactorial k (m + n)) =
        lucasKDivFactorial k (2 * m) * lucasKDivFactorial k (2 * n)

Sources

Kendra Killpatrick, "Super FiboCatalan Numbers and Their Lucas Analogues", Theorem 13.

Uses 1

Statement uses\(k\)-divisible Lucas factorial

21 fully proved10 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.