Generalized Fibonacci polynomials

DefinitionGeneralized Fibonacci polynomials#✓fully proved

Given polynomials \(p_0, p_1, d, g \in \mathbb{Z}[X]\), the generalized Fibonacci polynomial sequence \((G_n)_{n \ge 0}\) in \(\mathbb{Z}[X]\) is defined by \(G_0 = p_0\), \(G_1 = p_1\) and \(G_{n+2} = d \, G_{n+1} + g \, G_n\) for every natural number \(n\).

noncomputable def generalizedFibonacciPolynomial
    (p0 p1 d g : Polynomial ℤ) : ℕ → Polynomial ℤ
  | 0 => p0
  | 1 => p1
  | (n + 2) =>
    d * generalizedFibonacciPolynomial p0 p1 d g (n + 1) +
      g * generalizedFibonacciPolynomial p0 p1 d g n

Used by 48

Used byBinomial sum of generalized Fibonacci polynomials as an integral · Catalan identity for Fibonacci-type generalized Fibonacci polynomials · Explicit formula for Fibonacci-type generalized Fibonacci polynomials · Integral representation of Fibonacci-type generalized Fibonacci polynomials · Catalan identity for Lucas-type generalized Fibonacci polynomials · Explicit formula for Lucas-type generalized Fibonacci polynomials · Recurrence for generalized Fibonacci polynomials · Index-one term of a generalized Fibonacci polynomial sequence · Index-zero term of a generalized Fibonacci polynomial sequence · Pell-type solutions as rescaled odd Fibonacci–Lucas values · Pell-type solutions as rescaled odd Fibonacci–Lucas values, squarefree case · Polynomial Pell-type solutions as rescaled Fibonacci–Lucas polynomials · Integer values of the generalized Fibonacci generating function at rationals · Integer values of the generalized Fibonacci generating function in its interval of convergence · Integer-polynomial values of the Fibonacci polynomial generating function · Integer values of the generalized Lucas generating function at rationals · Integer values of the generalized Lucas generating function in its interval of convergence · Integer-polynomial values of the Lucas polynomial generating function · Series over a family of Fibonacci polynomial squares · A telescoping series of powers of gibonacci polynomial ratios · Series over a family of Lucas polynomial squares · Reciprocal sums of shifted squares of Fibonacci and Lucas polynomials (Koshy–Gao, Theorem 2.1) · Reciprocal sums of shifted squares of Jacobsthal and Jacobsthal–Lucas polynomials (Koshy–Gao, Theorem 3.1) · Even powers of Fibonacci polynomials at \(n \pm k\) · Odd powers of Fibonacci polynomials at \(n \pm k\) · Catalan-type identities for Fibonacci and Lucas polynomials · Even powers of Lucas polynomials at \(n \pm k\) · Odd powers of Lucas polynomials at \(n \pm k\) · Gibonacci polynomial square sums at shifted even multiples of the index · Gibonacci polynomial square sums at even multiples of the index · Cubic-denominator series for even-index Fibonacci polynomials · Cubic-denominator series for odd-index Fibonacci polynomials · Series of even powers of Fibonacci polynomials at even indices · Even-power series over odd-indexed Fibonacci polynomials · Odd-power series over even-indexed Fibonacci polynomials · Odd-power series over odd-indexed Fibonacci polynomials · Telescoping sum of powers of inverse gibonacci polynomial ratios · Telescoping sum of powers of gibonacci polynomial ratios · Telescoping inverse-power series of gibonacci polynomials at even indices, even shift · Telescoping inverse-power series of gibonacci polynomials at odd indices, odd shift · Telescoping inverse-power series of gibonacci polynomials at odd indices, even shift · Telescoping inverse-power series of gibonacci polynomials at even indices, odd shift · Cubic series over even-indexed Lucas polynomials · Cubic sums with odd-index Lucas polynomial denominators · Even-power sums with even-index Lucas polynomial denominators · Even-power sums with odd-index Lucas polynomial denominators · Odd-power sums with even-index Lucas polynomial denominators · Odd-power sums with odd-index Lucas polynomial denominators

TheoremIndex-zero term of a generalized Fibonacci polynomial sequence#✓fully proved

For all polynomials \(p_0, p_1, d, g \in \mathbb{Z}[X]\), the generalized Fibonacci polynomial sequence \((G_n)\) with initial terms \(p_0, p_1\) and recurrence coefficients \(d, g\) has \(G_0 = p_0\).

@[simp]
theorem generalizedFibonacciPolynomial_zero
    (p0 p1 d g : Polynomial ℤ) :
    generalizedFibonacciPolynomial p0 p1 d g 0 = p0

Uses 1

Statement usesGeneralized Fibonacci polynomials

TheoremIndex-one term of a generalized Fibonacci polynomial sequence#✓fully proved

For all polynomials \(p_0, p_1, d, g \in \mathbb{Z}[X]\), the generalized Fibonacci polynomial sequence \((G_n)\) with initial terms \(p_0, p_1\) and recurrence coefficients \(d, g\) has \(G_1 = p_1\).

@[simp]
theorem generalizedFibonacciPolynomial_one
    (p0 p1 d g : Polynomial ℤ) :
    generalizedFibonacciPolynomial p0 p1 d g 1 = p1

Uses 1

Statement usesGeneralized Fibonacci polynomials

TheoremRecurrence for generalized Fibonacci polynomials#✓fully proved

For all polynomials \(p_0, p_1, d, g\) in \(\mathbb{Z}[X]\) and every natural number \(n\), the generalized Fibonacci polynomial sequence \((G_m)\) with initial terms \(p_0, p_1\) and recurrence coefficients \(d, g\) satisfies \(G_{n+2} = d \, G_{n+1} + g \, G_n\).

@[simp]
theorem generalizedFibonacciPolynomial_add_two
    (p0 p1 d g : Polynomial ℤ) (n : ℕ) :
    generalizedFibonacciPolynomial p0 p1 d g (n + 2) =
      d * generalizedFibonacciPolynomial p0 p1 d g (n + 1) +
        g * generalizedFibonacciPolynomial p0 p1 d g n

Uses 1

Statement usesGeneralized Fibonacci polynomials

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.