Sums of powers of gibonacci polynomials

TheoremCatalan-type identities for Fibonacci and Lucas polynomials#●ready to prove

Let \(f_i\) and \(\ell_i\) be the Fibonacci and Lucas polynomials in \(\mathbb{Z}[x]\), defined by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and \(g_{i+2} = x g_{i+1} + g_i\) for \(g = f, \ell\). For all natural numbers \(k \le n\),

\[ f_{n+k} f_{n-k} - f_n^2 = (-1)^{n+k+1} f_k^2 \quad\text{and}\quad \ell_{n+k} \ell_{n-k} - \ell_n^2 = (-1)^{n+k} (x^2 + 4) f_k^2 \]

in \(\mathbb{Z}[x]\).

The source quotes this lemma from Koshy.

public theorem_wanted gibonacciPoly_mul_sub_sq {n k : ℕ} (hk : k ≤ n) :
    𝔣 (n + k) * 𝔣 (n - k) - 𝔣 n ^ 2 = (-1) ^ (n + k + 1) * 𝔣 k ^ 2 ∧
      𝔩 (n + k) * 𝔩 (n - k) - 𝔩 n ^ 2 = (-1) ^ (n + k) * (X ^ 2 + 4) * 𝔣 k ^ 2
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Lemma 2.1.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremTelescoping inverse-power series of gibonacci polynomials at odd indices, odd shift#●ready to prove

Let \(x > 0\) be real, and let \(g_n\) denote either the Fibonacci polynomials, given by \(g_0 = 0\) and \(g_1 = 1\), or the Lucas polynomials, given by \(g_0 = 2\) and \(g_1 = x\), both satisfying \(g_{n+2} = x g_{n+1} + g_n\) and evaluated at \(x\). Let \(k\) be an odd natural number and \(\lambda\) a positive integer. Then

\[\sum_{n=0}^{\infty} \left(\frac{1}{g_{2n+1}^{\lambda}} - \frac{1}{g_{2n+1+2k}^{\lambda}}\right) = \sum_{r=1}^{k} \frac{1}{g_{2r-1}^{\lambda}}.\]

The source quotes this lemma from Koshy as the sum over \(n \ge (k + 1)/2\) of \(1/g_{2n-k}^{\lambda} - 1/g_{2n+k}^{\lambda}\); here the summation index is shifted to start at \(0\).

public theorem_wanted tsum_inv_pow_gibonacciPoly_sub_odd {x : ℝ} (hx : 0 < x)
    {g : ℕ → ℤ[X]} (hg : g = 𝔣 ∨ g = 𝔩) {k lam : ℕ} (hk : Odd k) (hlam : 0 < lam) :
    ∑' n : ℕ, (1 / aeval x (g (2 * n + 1)) ^ lam - 1 / aeval x (g (2 * n + 1 + 2 * k)) ^ lam) =
      ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (g (2 * r - 1)) ^ lam
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Lemma 2.2.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremTelescoping inverse-power series of gibonacci polynomials at even indices, even shift#●ready to prove

Let \(x > 0\) be real, and let \(g_n\) denote either the Fibonacci polynomials, given by \(g_0 = 0\) and \(g_1 = 1\), or the Lucas polynomials, given by \(g_0 = 2\) and \(g_1 = x\), both satisfying \(g_{n+2} = x g_{n+1} + g_n\) and evaluated at \(x\). Let \(k\) be an even natural number and \(\lambda\) a positive integer. Then

\[\sum_{n=0}^{\infty} \left(\frac{1}{g_{2n+2}^{\lambda}} - \frac{1}{g_{2n+2+2k}^{\lambda}}\right) = \sum_{r=1}^{k} \frac{1}{g_{2r}^{\lambda}}.\]

The source quotes this lemma from Koshy as the sum over \(n \ge k/2 + 1\) of \(1/g_{2n-k}^{\lambda} - 1/g_{2n+k}^{\lambda}\); here the summation index is shifted to start at \(0\).

public theorem_wanted tsum_inv_pow_gibonacciPoly_sub_even {x : ℝ} (hx : 0 < x)
    {g : ℕ → ℤ[X]} (hg : g = 𝔣 ∨ g = 𝔩) {k lam : ℕ} (hk : Even k) (hlam : 0 < lam) :
    ∑' n : ℕ, (1 / aeval x (g (2 * n + 2)) ^ lam - 1 / aeval x (g (2 * n + 2 + 2 * k)) ^ lam) =
      ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (g (2 * r)) ^ lam
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Lemma 2.3.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremTelescoping inverse-power series of gibonacci polynomials at even indices, odd shift#●ready to prove

Let \(x > 0\) be real, and let \(g_n\) denote either the Fibonacci polynomials, given by \(g_0 = 0\) and \(g_1 = 1\), or the Lucas polynomials, given by \(g_0 = 2\) and \(g_1 = x\), both satisfying \(g_{n+2} = x g_{n+1} + g_n\) and evaluated at \(x\). Let \(k\) be an odd natural number and \(\lambda\) a positive integer. Then

\[\sum_{n=0}^{\infty} \left(\frac{1}{g_{2n+2}^{\lambda}} - \frac{1}{g_{2n+2+2k}^{\lambda}}\right) = \sum_{r=1}^{k} \frac{1}{g_{2r}^{\lambda}}.\]

The source quotes this lemma from Koshy as the sum over \(n \ge (k + 1)/2\) of \(1/g_{2n+1-k}^{\lambda} - 1/g_{2n+1+k}^{\lambda}\); here the summation index is shifted to start at \(0\).

public theorem_wanted tsum_inv_pow_gibonacciPoly_succ_sub_odd {x : ℝ} (hx : 0 < x)
    {g : ℕ → ℤ[X]} (hg : g = 𝔣 ∨ g = 𝔩) {k lam : ℕ} (hk : Odd k) (hlam : 0 < lam) :
    ∑' n : ℕ, (1 / aeval x (g (2 * n + 2)) ^ lam - 1 / aeval x (g (2 * n + 2 + 2 * k)) ^ lam) =
      ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (g (2 * r)) ^ lam
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Lemma 2.4.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremTelescoping inverse-power series of gibonacci polynomials at odd indices, even shift#●ready to prove

Let \(x > 0\) be real, and let \(g_n\) denote either the Fibonacci polynomials, given by \(g_0 = 0\) and \(g_1 = 1\), or the Lucas polynomials, given by \(g_0 = 2\) and \(g_1 = x\), both satisfying \(g_{n+2} = x g_{n+1} + g_n\) and evaluated at \(x\). Let \(k\) be an even natural number and \(\lambda\) a positive integer. Then

\[\sum_{n=0}^{\infty} \left(\frac{1}{g_{2n+1}^{\lambda}} - \frac{1}{g_{2n+1+2k}^{\lambda}}\right) = \sum_{r=1}^{k} \frac{1}{g_{2r-1}^{\lambda}}.\]

The source quotes this lemma from Koshy as the sum over \(n \ge k/2\) of \(1/g_{2n+1-k}^{\lambda} - 1/g_{2n+1+k}^{\lambda}\); here the summation index is shifted to start at \(0\).

public theorem_wanted tsum_inv_pow_gibonacciPoly_succ_sub_even {x : ℝ} (hx : 0 < x)
    {g : ℕ → ℤ[X]} (hg : g = 𝔣 ∨ g = 𝔩) {k lam : ℕ} (hk : Even k) (hlam : 0 < lam) :
    ∑' n : ℕ, (1 / aeval x (g (2 * n + 1)) ^ lam - 1 / aeval x (g (2 * n + 1 + 2 * k)) ^ lam) =
      ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (g (2 * r - 1)) ^ lam
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Lemma 2.5.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremEven powers of Fibonacci polynomials at \(n \pm k\)#●ready to prove

Let \(f_i \in \mathbb{Z}[x]\) be the Fibonacci polynomials, defined by \(f_0 = 0\), \(f_1 = 1\) and \(f_{i+2} = x f_{i+1} + f_i\). For all natural numbers \(k \le n\) and every natural number \(m\),

\[ (x^2 + 4)^{m-1} \bigl(f_{n+k}^{2m} - f_{n-k}^{2m}\bigr) = \sum_{j=0}^{m-1} \binom{2m}{j} (-1)^{(n+k+1)j} f_{2k(m-j)} f_{2n(m-j)} \]

in \(\mathbb{Z}[x]\), where for \(m = 0\) the exponent \(m - 1\) is read as \(0\) (both sides are then \(0\)).

public theorem_wanted fibPoly_pow_even_sub {n k : ℕ} (hk : k ≤ n) (m : ℕ) :
    (X ^ 2 + 4) ^ (m - 1) * (𝔣 (n + k) ^ (2 * m) - 𝔣 (n - k) ^ (2 * m)) =
      ∑ j ∈ Finset.range m, ((2 * m).choose j : ℤ[X]) * (-1) ^ ((n + k + 1) * j) *
        𝔣 (2 * k * (m - j)) * 𝔣 (2 * n * (m - j))
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Lemma 3.1.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremEven powers of Lucas polynomials at \(n \pm k\)#●ready to prove

Let \(f_i\) and \(\ell_i\) be the Fibonacci and Lucas polynomials in \(\mathbb{Z}[x]\), defined by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and \(g_{i+2} = x g_{i+1} + g_i\) for \(g = f, \ell\). For all natural numbers \(k \le n\) and every natural number \(m\),

\[ \ell_{n+k}^{2m} - \ell_{n-k}^{2m} = (x^2 + 4) \sum_{j=0}^{m-1} \binom{2m}{j} (-1)^{(n+k)j} f_{2k(m-j)} f_{2n(m-j)} \]

in \(\mathbb{Z}[x]\).

public theorem_wanted lucasPoly_pow_even_sub {n k : ℕ} (hk : k ≤ n) (m : ℕ) :
    𝔩 (n + k) ^ (2 * m) - 𝔩 (n - k) ^ (2 * m) =
      (X ^ 2 + 4) * ∑ j ∈ Finset.range m, ((2 * m).choose j : ℤ[X]) * (-1) ^ ((n + k) * j) *
        𝔣 (2 * k * (m - j)) * 𝔣 (2 * n * (m - j))
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Lemma 3.2.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremOdd powers of Fibonacci polynomials at \(n \pm k\)#●ready to prove

Let \(f_i\) and \(\ell_i\) be the Fibonacci and Lucas polynomials in \(\mathbb{Z}[x]\), defined by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and \(g_{i+2} = x g_{i+1} + g_i\) for \(g = f, \ell\). Let \(k \le n\) and \(m\) be natural numbers. In \(\mathbb{Z}[x]\), if \(k\) is odd then

\[ (x^2 + 4)^m \bigl(f_{n+k}^{2m+1} - f_{n-k}^{2m+1}\bigr) = \sum_{j=0}^{m} \binom{2m+1}{j} (-1)^{nj} f_{n(2m+1-2j)} \ell_{k(2m+1-2j)}, \]

and if \(k\) is even then

\[ (x^2 + 4)^m \bigl(f_{n+k}^{2m+1} - f_{n-k}^{2m+1}\bigr) = \sum_{j=0}^{m} \binom{2m+1}{j} (-1)^{(n+1)j} \ell_{n(2m+1-2j)} f_{k(2m+1-2j)}. \]
public theorem_wanted fibPoly_pow_odd_sub {n k : ℕ} (hk : k ≤ n) (m : ℕ) :
    (Odd k → (X ^ 2 + 4) ^ m * (𝔣 (n + k) ^ (2 * m + 1) - 𝔣 (n - k) ^ (2 * m + 1)) =
      ∑ j ∈ Finset.range (m + 1), ((2 * m + 1).choose j : ℤ[X]) * (-1) ^ (n * j) *
        𝔣 (n * (2 * m + 1 - 2 * j)) * 𝔩 (k * (2 * m + 1 - 2 * j))) ∧
    (Even k → (X ^ 2 + 4) ^ m * (𝔣 (n + k) ^ (2 * m + 1) - 𝔣 (n - k) ^ (2 * m + 1)) =
      ∑ j ∈ Finset.range (m + 1), ((2 * m + 1).choose j : ℤ[X]) * (-1) ^ ((n + 1) * j) *
        𝔩 (n * (2 * m + 1 - 2 * j)) * 𝔣 (k * (2 * m + 1 - 2 * j)))
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Lemma 4.1.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremOdd powers of Lucas polynomials at \(n \pm k\)#●ready to prove

Let \(f_i\) and \(\ell_i\) be the Fibonacci and Lucas polynomials in \(\mathbb{Z}[x]\), defined by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and \(g_{i+2} = x g_{i+1} + g_i\) for \(g = f, \ell\). Let \(k \le n\) and \(m\) be natural numbers. In \(\mathbb{Z}[x]\), if \(k\) is odd then

\[ \ell_{n+k}^{2m+1} - \ell_{n-k}^{2m+1} = \sum_{j=0}^{m} \binom{2m+1}{j} (-1)^{(n+1)j} \ell_{n(2m+1-2j)} \ell_{k(2m+1-2j)}, \]

and if \(k\) is even then

\[ \ell_{n+k}^{2m+1} - \ell_{n-k}^{2m+1} = (x^2 + 4) \sum_{j=0}^{m} \binom{2m+1}{j} (-1)^{nj} f_{n(2m+1-2j)} f_{k(2m+1-2j)}. \]
public theorem_wanted lucasPoly_pow_odd_sub {n k : ℕ} (hk : k ≤ n) (m : ℕ) :
    (Odd k → 𝔩 (n + k) ^ (2 * m + 1) - 𝔩 (n - k) ^ (2 * m + 1) =
      ∑ j ∈ Finset.range (m + 1), ((2 * m + 1).choose j : ℤ[X]) * (-1) ^ ((n + 1) * j) *
        𝔩 (n * (2 * m + 1 - 2 * j)) * 𝔩 (k * (2 * m + 1 - 2 * j))) ∧
    (Even k → 𝔩 (n + k) ^ (2 * m + 1) - 𝔩 (n - k) ^ (2 * m + 1) =
      (X ^ 2 + 4) * ∑ j ∈ Finset.range (m + 1), ((2 * m + 1).choose j : ℤ[X]) *
        (-1) ^ (n * j) * 𝔣 (n * (2 * m + 1 - 2 * j)) * 𝔣 (k * (2 * m + 1 - 2 * j)))
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Lemma 4.2.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremCubic-denominator series for even-index Fibonacci polynomials#●ready to prove

Let \(f_i\) and \(\ell_i\) be the Fibonacci and Lucas polynomials, defined by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and \(g_{i+2} = x g_{i+1} + g_i\) for \(g = f, \ell\). For every real \(x > 0\),

\[ \sum_{n \ge 1} \frac{(x^3 + 3x) f_{6n}(x) + 3x f_{2n}(x)}{(f_{2n}(x)^2 + 1)^3} = x^2 + 4 \]

and

\[ \sum_{n \ge 2} \frac{x(x^4 + 4x^2 + 3) \ell_{6n}(x) - 3x \ell_{2n}(x)}{(f_{2n}(x)^2 - x^2)^3} = \frac{(x^2 + 4)\bigl((x^2 + 2)^3 + 1\bigr)}{x^3 (x^2 + 2)^3}. \]
public theorem_wanted tsum_fibPoly_cube_even_index {x : ℝ} (hx : 0 < x) :
    ∑' n : ℕ, ((x ^ 3 + 3 * x) * aeval x (𝔣 (6 * (n + 1))) + 3 * x * aeval x (𝔣 (2 * (n + 1)))) /
        (aeval x (𝔣 (2 * (n + 1))) ^ 2 + 1) ^ 3 =
      x ^ 2 + 4 ∧
      ∑' n : ℕ, (x * (x ^ 4 + 4 * x ^ 2 + 3) * aeval x (𝔩 (6 * (n + 2))) -
          3 * x * aeval x (𝔩 (2 * (n + 2)))) /
          (aeval x (𝔣 (2 * (n + 2))) ^ 2 - x ^ 2) ^ 3 =
        (x ^ 2 + 4) * ((x ^ 2 + 2) ^ 3 + 1) / (x ^ 3 * (x ^ 2 + 2) ^ 3)
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Corollary 4.3.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremCubic series over even-indexed Lucas polynomials#●ready to prove

Let \(x > 0\) be real, and let \(f_n\) and \(\ell_n\) denote the Fibonacci and Lucas polynomials evaluated at \(x\), given by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and the recurrence \(z_{n+2} = x z_{n+1} + z_n\) for both. Then

\[\sum_{n=1}^{\infty} \frac{(x^3 + 3x) \ell_{6n} - 3x \ell_{2n}} {\left(\ell_{2n}^2 - (x^2 + 4)\right)^3} = \frac{1}{x^3}\]

and

\[\sum_{n=2}^{\infty} \frac{x(x^4 + 4x^2 + 3) f_{6n} + 3x f_{2n}} {\left(\ell_{2n}^2 + (x^2 + 4) x^2\right)^3} = \frac{1}{x^2 + 4} \left(\frac{1}{(x^2 + 2)^3} + \frac{1}{(x^4 + 4x^2 + 2)^3}\right).\]
public theorem_wanted tsum_lucasPoly_cube_even_index {x : ℝ} (hx : 0 < x) :
    ∑' n : ℕ, ((x ^ 3 + 3 * x) * aeval x (𝔩 (6 * (n + 1))) - 3 * x * aeval x (𝔩 (2 * (n + 1)))) /
        (aeval x (𝔩 (2 * (n + 1))) ^ 2 - (x ^ 2 + 4)) ^ 3 =
      1 / x ^ 3 ∧
      ∑' n : ℕ, (x * (x ^ 4 + 4 * x ^ 2 + 3) * aeval x (𝔣 (6 * (n + 2))) +
          3 * x * aeval x (𝔣 (2 * (n + 2)))) /
          (aeval x (𝔩 (2 * (n + 2))) ^ 2 + (x ^ 2 + 4) * x ^ 2) ^ 3 =
        1 / (x ^ 2 + 4) * (1 / (x ^ 2 + 2) ^ 3 + 1 / (x ^ 4 + 4 * x ^ 2 + 2) ^ 3)
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Corollary 4.5.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremCubic-denominator series for odd-index Fibonacci polynomials#●ready to prove

Let \(f_i\) and \(\ell_i\) be the Fibonacci and Lucas polynomials, defined by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and \(g_{i+2} = x g_{i+1} + g_i\) for \(g = f, \ell\). For every real \(x > 0\),

\[ \sum_{n \ge 1} \frac{(x^3 + 3x) f_{6n+3}(x) - 3x f_{2n+1}(x)}{(f_{2n+1}(x)^2 - 1)^3} = \frac{x^2 + 4}{x^3} \]

and

\[ \sum_{n \ge 1} \frac{x(x^4 + 4x^2 + 3) \ell_{6n+3}(x) + 3x \ell_{2n+1}(x)} {(f_{2n+1}(x)^2 + x^2)^3} = \frac{(x^2 + 4)\bigl((x^2 + 1)^3 + 1\bigr)}{(x^2 + 1)^3}. \]
public theorem_wanted tsum_fibPoly_cube_odd_index {x : ℝ} (hx : 0 < x) :
    ∑' n : ℕ, ((x ^ 3 + 3 * x) * aeval x (𝔣 (6 * (n + 1) + 3)) -
          3 * x * aeval x (𝔣 (2 * (n + 1) + 1))) /
        (aeval x (𝔣 (2 * (n + 1) + 1)) ^ 2 - 1) ^ 3 =
      (x ^ 2 + 4) / x ^ 3 ∧
      ∑' n : ℕ, (x * (x ^ 4 + 4 * x ^ 2 + 3) * aeval x (𝔩 (6 * (n + 1) + 3)) +
          3 * x * aeval x (𝔩 (2 * (n + 1) + 1))) /
          (aeval x (𝔣 (2 * (n + 1) + 1)) ^ 2 + x ^ 2) ^ 3 =
        (x ^ 2 + 4) * ((x ^ 2 + 1) ^ 3 + 1) / (x ^ 2 + 1) ^ 3
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Corollary 4.7.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremCubic sums with odd-index Lucas polynomial denominators#●ready to prove

Let \(f_n\) and \(\ell_n\) denote the Fibonacci and Lucas polynomials, given by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and \(g_{n+2} = x g_{n+1} + g_n\) for \(g \in \{f, \ell\}\), evaluated at a real number \(x > 0\). Then

\[\sum_{n \ge 1} \frac{(x^3 + 3x) \ell_{6n+3} + 3x \ell_{2n+1}}{(\ell_{2n+1}^2 + x^2 + 4)^3} = \frac{1}{(x^2 + 2)^3}\]

and

\[\sum_{n \ge 1} \frac{x (x^4 + 4x^2 + 3) f_{6n+3} - 3x f_{2n+1}}{(\ell_{2n+1}^2 - x^2 (x^2 + 4))^3} = \frac{(x^2 + 3)^3 + 1}{x^3 (x^2 + 4) (x^2 + 3)^3}.\]
public theorem_wanted tsum_lucasPoly_cube_odd_index {x : ℝ} (hx : 0 < x) :
    ∑' n : ℕ, ((x ^ 3 + 3 * x) * aeval x (𝔩 (6 * (n + 1) + 3)) +
          3 * x * aeval x (𝔩 (2 * (n + 1) + 1))) /
        (aeval x (𝔩 (2 * (n + 1) + 1)) ^ 2 + x ^ 2 + 4) ^ 3 =
      1 / (x ^ 2 + 2) ^ 3 ∧
      ∑' n : ℕ, (x * (x ^ 4 + 4 * x ^ 2 + 3) * aeval x (𝔣 (6 * (n + 1) + 3)) -
          3 * x * aeval x (𝔣 (2 * (n + 1) + 1))) /
          (aeval x (𝔩 (2 * (n + 1) + 1)) ^ 2 - x ^ 2 * (x ^ 2 + 4)) ^ 3 =
        ((x ^ 2 + 3) ^ 3 + 1) / (x ^ 3 * (x ^ 2 + 4) * (x ^ 2 + 3) ^ 3)
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Corollary 4.9.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremCubic-denominator series for even-index Fibonacci numbers#●ready to prove

Let \(F_n\) be the Fibonacci numbers (\(F_0 = 0\), \(F_1 = 1\), \(F_{n+2} = F_{n+1} + F_n\)) and \(L_n\) the Lucas numbers. Then, as series of real numbers,

\[ \sum_{n \ge 1} \frac{4F_{6n} + 3F_{2n}}{(F_{2n}^2 + 1)^3} = 5 \quad\text{and}\quad \sum_{n \ge 2} \frac{8L_{6n} - 3L_{2n}}{(F_{2n}^2 - 1)^3} = \frac{140}{27}. \]
public theorem_wanted tsum_fib_cube_even_index :
    ∑' n : ℕ, (4 * (Nat.fib (6 * (n + 1)) : ℝ) + 3 * (Nat.fib (2 * (n + 1)) : ℝ)) /
        ((Nat.fib (2 * (n + 1)) : ℝ) ^ 2 + 1) ^ 3 = 5 ∧
      ∑' n : ℕ, (8 * (lucasNumber (6 * (n + 2)) : ℝ) - 3 * (lucasNumber (2 * (n + 2)) : ℝ)) /
          ((Nat.fib (2 * (n + 2)) : ℝ) ^ 2 - 1) ^ 3 = 140 / 27
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Corollary 4.4.
Uses 1
Statement usesLucas numbers

TheoremCubic series over even-indexed Lucas numbers#●ready to prove

Let \(F_n\) and \(L_n\) denote the Fibonacci and Lucas numbers, given by \(F_0 = 0\), \(F_1 = 1\), \(L_0 = 2\), \(L_1 = 1\) and the recurrence \(z_{n+2} = z_{n+1} + z_n\) for both. Then

\[\sum_{n=1}^{\infty} \frac{4L_{6n} - 3L_{2n}}{(L_{2n}^2 - 5)^3} = 1\]

and

\[\sum_{n=2}^{\infty} \frac{8F_{6n} + 3F_{2n}}{(L_{2n}^2 + 5)^3} = \frac{74}{9261}.\]
public theorem_wanted tsum_lucas_cube_even_index :
    ∑' n : ℕ, (4 * (lucasNumber (6 * (n + 1)) : ℝ) - 3 * (lucasNumber (2 * (n + 1)) : ℝ)) /
        ((lucasNumber (2 * (n + 1)) : ℝ) ^ 2 - 5) ^ 3 = 1 ∧
      ∑' n : ℕ, (8 * (Nat.fib (6 * (n + 2)) : ℝ) + 3 * (Nat.fib (2 * (n + 2)) : ℝ)) /
          ((lucasNumber (2 * (n + 2)) : ℝ) ^ 2 + 5) ^ 3 = 74 / 9261
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Corollary 4.6.
Uses 1
Statement usesLucas numbers

TheoremCubic-denominator series for odd-index Fibonacci numbers#●ready to prove

Let \(F_n\) be the Fibonacci numbers (\(F_0 = 0\), \(F_1 = 1\), \(F_{n+2} = F_{n+1} + F_n\)) and \(L_n\) the Lucas numbers. Then, as series of real numbers,

\[ \sum_{n \ge 1} \frac{4F_{6n+3} - 3F_{2n+1}}{(F_{2n+1}^2 - 1)^3} = 5 \quad\text{and}\quad \sum_{n \ge 1} \frac{8L_{6n+3} + 3L_{2n+1}}{(F_{2n+1}^2 + 1)^3} = \frac{45}{8}. \]

These are the case \(x = 1\) of Corollary 4.7. The extracted record of the source prints the lower limit of the second series as \(n = 2\); with that limit the sum would be \(45/8 - 124/25 = 133/200\).

public theorem_wanted tsum_fib_cube_odd_index :
    ∑' n : ℕ, (4 * (Nat.fib (6 * (n + 1) + 3) : ℝ) - 3 * (Nat.fib (2 * (n + 1) + 1) : ℝ)) /
        ((Nat.fib (2 * (n + 1) + 1) : ℝ) ^ 2 - 1) ^ 3 = 5 ∧
      ∑' n : ℕ, (8 * (lucasNumber (6 * (n + 1) + 3) : ℝ) +
          3 * (lucasNumber (2 * (n + 1) + 1) : ℝ)) /
          ((Nat.fib (2 * (n + 1) + 1) : ℝ) ^ 2 + 1) ^ 3 = 45 / 8
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Corollary 4.8.
Uses 1
Statement usesLucas numbers

TheoremCubic series over odd-indexed Lucas numbers#●ready to prove

Let \(F_n\) and \(L_n\) denote the Fibonacci and Lucas numbers, given by \(F_0 = 0\), \(F_1 = 1\), \(L_0 = 2\), \(L_1 = 1\) and the recurrence \(z_{n+2} = z_{n+1} + z_n\) for both. Then

\[\sum_{n=1}^{\infty} \frac{4L_{6n+3} + 3L_{2n+1}}{(L_{2n+1}^2 + 5)^3} = \frac{1}{27}\]

and

\[\sum_{n=1}^{\infty} \frac{8F_{6n+3} - 3F_{2n+1}}{(L_{2n+1}^2 - 5)^3} = \frac{13}{64}.\]
public theorem_wanted tsum_lucas_cube_odd_index :
    ∑' n : ℕ, (4 * (lucasNumber (6 * (n + 1) + 3) : ℝ) + 3 * (lucasNumber (2 * (n + 1) + 1) : ℝ)) /
        ((lucasNumber (2 * (n + 1) + 1) : ℝ) ^ 2 + 5) ^ 3 = 1 / 27 ∧
      ∑' n : ℕ, (8 * (Nat.fib (6 * (n + 1) + 3) : ℝ) - 3 * (Nat.fib (2 * (n + 1) + 1) : ℝ)) /
          ((lucasNumber (2 * (n + 1) + 1) : ℝ) ^ 2 - 5) ^ 3 = 13 / 64
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Corollary 4.10.
Uses 1
Statement usesLucas numbers

TheoremSeries of even powers of Fibonacci polynomials at even indices#●ready to prove

Let \(f_i\) be the Fibonacci polynomials, defined by \(f_0 = 0\), \(f_1 = 1\) and \(f_{i+2} = x f_{i+1} + f_i\). Let \(x > 0\) be real and let \(k\) and \(m\) be positive integers. If \(k\) is odd, put \(L = (k + 1)/2\) and \(s_r = 2r - 1\); if \(k\) is even, put \(L = k/2 + 1\) and \(s_r = 2r\). Then

\[ \sum_{n \ge L} \frac{\sum_{j=0}^{m-1} \binom{2m}{j} (-1)^{(k+1)j} f_{2k(m-j)}(x) f_{4n(m-j)}(x)}{\bigl(f_{2n}(x)^2 - (-1)^k f_k(x)^2\bigr)^{2m}} = (x^2 + 4)^{m-1} \sum_{r=1}^{k} \frac{1}{f_{s_r}(x)^{2m}}. \]
public theorem_wanted tsum_fibPoly_even_pow_even_index {x : ℝ} (hx : 0 < x) {k m : ℕ}
    (hk : 0 < k) (hm : 0 < m) :
    ∑' n : ℕ, (∑ j ∈ Finset.range m, ((2 * m).choose j : ℝ) * (-1) ^ ((k + 1) * j) *
          aeval x (𝔣 (2 * k * (m - j))) * aeval x (𝔣 (4 * (n + 𝔏[k]) * (m - j)))) /
        (aeval x (𝔣 (2 * (n + 𝔏[k]))) ^ 2 - (-1) ^ k * aeval x (𝔣 k) ^ 2) ^ (2 * m) =
      (x ^ 2 + 4) ^ (m - 1) * ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (𝔣 𝔰[k, r]) ^ (2 * m)
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Theorem 1.1.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremEven-power sums with even-index Lucas polynomial denominators#●ready to prove

Let \(f_n\) and \(\ell_n\) denote the Fibonacci and Lucas polynomials, given by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and \(g_{n+2} = x g_{n+1} + g_n\) for \(g \in \{f, \ell\}\), evaluated at a real number \(x > 0\), and let \(k\) and \(m\) be positive integers. Put \(L = (k + 1)/2\) and \(s_r = 2r - 1\) if \(k\) is odd, and \(L = k/2 + 1\) and \(s_r = 2r\) if \(k\) is even. Then

\[\sum_{n \ge L} \frac{\sum_{j=0}^{m-1} \binom{2m}{j} (-1)^{kj} f_{2k(m-j)} f_{4n(m-j)}} {\left(\ell_{2n}^2 + (-1)^k (x^2 + 4) f_k^2\right)^{2m}} = \frac{1}{x^2 + 4} \sum_{r=1}^{k} \frac{1}{\ell_{s_r}^{2m}}.\]
public theorem_wanted tsum_lucasPoly_even_pow_even_index {x : ℝ} (hx : 0 < x) {k m : ℕ}
    (hk : 0 < k) (hm : 0 < m) :
    ∑' n : ℕ, (∑ j ∈ Finset.range m, ((2 * m).choose j : ℝ) * (-1) ^ (k * j) *
          aeval x (𝔣 (2 * k * (m - j))) * aeval x (𝔣 (4 * (n + 𝔏[k]) * (m - j)))) /
        (aeval x (𝔩 (2 * (n + 𝔏[k]))) ^ 2 + (-1) ^ k * (x ^ 2 + 4) * aeval x (𝔣 k) ^ 2) ^ (2 * m) =
      1 / (x ^ 2 + 4) * ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (𝔩 𝔰[k, r]) ^ (2 * m)
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Theorem 1.2.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremEven-power series over odd-indexed Fibonacci polynomials#●ready to prove

Let \(x > 0\) be real, let \(f_n\) denote the Fibonacci polynomials evaluated at \(x\), given by \(f_0 = 0\), \(f_1 = 1\) and \(f_{n+2} = x f_{n+1} + f_n\), and let \(k\) and \(m\) be positive integers. Put \(M = (k + 1)/2\) and \(t_r = 2r\) if \(k\) is odd, and \(M = k/2\) and \(t_r = 2r - 1\) if \(k\) is even. Then

\[\sum_{n=0}^{\infty} \frac{\sum_{j=0}^{m-1} \binom{2m}{j} (-1)^{kj} f_{2k(m-j)} f_{(4(n+M)+2)(m-j)}}{\left(f_{2(n+M)+1}^2 + (-1)^k f_k^2\right)^{2m}} = (x^2 + 4)^{m-1} \sum_{r=1}^{k} \frac{1}{f_{t_r}^{2m}}.\]

This is the source's sum over \(n \ge M\) with the summation index shifted to start at \(0\).

public theorem_wanted tsum_fibPoly_even_pow_odd_index {x : ℝ} (hx : 0 < x) {k m : ℕ}
    (hk : 0 < k) (hm : 0 < m) :
    ∑' n : ℕ, (∑ j ∈ Finset.range m, ((2 * m).choose j : ℝ) * (-1) ^ (k * j) *
          aeval x (𝔣 (2 * k * (m - j))) * aeval x (𝔣 ((4 * (n + 𝔐[k]) + 2) * (m - j)))) /
        (aeval x (𝔣 (2 * (n + 𝔐[k]) + 1)) ^ 2 + (-1) ^ k * aeval x (𝔣 k) ^ 2) ^ (2 * m) =
      (x ^ 2 + 4) ^ (m - 1) * ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (𝔣 𝔱[k, r]) ^ (2 * m)
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Theorem 1.3.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremEven-power sums with odd-index Lucas polynomial denominators#●ready to prove

Let \(f_n\) and \(\ell_n\) denote the Fibonacci and Lucas polynomials, given by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and \(g_{n+2} = x g_{n+1} + g_n\) for \(g \in \{f, \ell\}\), evaluated at a real number \(x > 0\), and let \(k\) and \(m\) be positive integers. Put \(M = (k + 1)/2\) and \(t_r = 2r\) if \(k\) is odd, and \(M = k/2\) and \(t_r = 2r - 1\) if \(k\) is even. Then

\[\sum_{n \ge M} \frac{\sum_{j=0}^{m-1} \binom{2m}{j} (-1)^{(k+1)j} f_{2k(m-j)} f_{(4n+2)(m-j)}} {\left(\ell_{2n+1}^2 - (-1)^k (x^2 + 4) f_k^2\right)^{2m}} = \frac{1}{x^2 + 4} \sum_{r=1}^{k} \frac{1}{\ell_{t_r}^{2m}}.\]
public theorem_wanted tsum_lucasPoly_even_pow_odd_index {x : ℝ} (hx : 0 < x) {k m : ℕ}
    (hk : 0 < k) (hm : 0 < m) :
    ∑' n : ℕ, (∑ j ∈ Finset.range m, ((2 * m).choose j : ℝ) * (-1) ^ ((k + 1) * j) *
          aeval x (𝔣 (2 * k * (m - j))) * aeval x (𝔣 ((4 * (n + 𝔐[k]) + 2) * (m - j)))) /
        (aeval x (𝔩 (2 * (n + 𝔐[k]) + 1)) ^ 2 - (-1) ^ k * (x ^ 2 + 4) * aeval x (𝔣 k) ^ 2) ^
          (2 * m) =
      1 / (x ^ 2 + 4) * ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (𝔩 𝔱[k, r]) ^ (2 * m)
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Theorem 1.4.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremOdd-power series over even-indexed Fibonacci polynomials#●ready to prove

Let \(x > 0\) be real, let \(f_n\) and \(\ell_n\) denote the Fibonacci and Lucas polynomials evaluated at \(x\), given by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and the recurrence \(z_{n+2} = x z_{n+1} + z_n\) for both, and let \(k\) be a positive integer and \(m\) a natural number. Put \(L = (k + 1)/2\) if \(k\) is odd and \(L = k/2 + 1\) if \(k\) is even. If \(k\) is odd, then

\[\sum_{n=0}^{\infty} \frac{\sum_{j=0}^{m} \binom{2m+1}{j} f_{2(n+L)(2m+1-2j)} \ell_{k(2m+1-2j)}}{\left(f_{2(n+L)}^2 + f_k^2\right)^{2m+1}} = (x^2 + 4)^m \sum_{r=1}^{k} \frac{1}{f_{2r-1}^{2m+1}},\]

and if \(k\) is even, then

\[\sum_{n=0}^{\infty} \frac{\sum_{j=0}^{m} \binom{2m+1}{j} (-1)^j \ell_{2(n+L)(2m+1-2j)} f_{k(2m+1-2j)}}{\left(f_{2(n+L)}^2 - f_k^2\right)^{2m+1}} = (x^2 + 4)^m \sum_{r=1}^{k} \frac{1}{f_{2r}^{2m+1}}.\]

These are the source's sums over \(n \ge L\) with the summation index shifted to start at \(0\).

public theorem_wanted tsum_fibPoly_odd_pow_even_index {x : ℝ} (hx : 0 < x) {k : ℕ}
    (hk : 0 < k) (m : ℕ) :
    (Odd k → ∑' n : ℕ, (∑ j ∈ Finset.range (m + 1), ((2 * m + 1).choose j : ℝ) *
          aeval x (𝔣 (2 * (n + 𝔏[k]) * (2 * m + 1 - 2 * j))) *
            aeval x (𝔩 (k * (2 * m + 1 - 2 * j)))) /
        (aeval x (𝔣 (2 * (n + 𝔏[k]))) ^ 2 + aeval x (𝔣 k) ^ 2) ^ (2 * m + 1) =
      (x ^ 2 + 4) ^ m * ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (𝔣 (2 * r - 1)) ^ (2 * m + 1)) ∧
    (Even k → ∑' n : ℕ, (∑ j ∈ Finset.range (m + 1), ((2 * m + 1).choose j : ℝ) * (-1) ^ j *
          aeval x (𝔩 (2 * (n + 𝔏[k]) * (2 * m + 1 - 2 * j))) *
            aeval x (𝔣 (k * (2 * m + 1 - 2 * j)))) /
        (aeval x (𝔣 (2 * (n + 𝔏[k]))) ^ 2 - aeval x (𝔣 k) ^ 2) ^ (2 * m + 1) =
      (x ^ 2 + 4) ^ m * ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (𝔣 (2 * r)) ^ (2 * m + 1))
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Theorem 1.5.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremOdd-power sums with even-index Lucas polynomial denominators#●ready to prove

Let \(f_n\) and \(\ell_n\) denote the Fibonacci and Lucas polynomials, given by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and \(g_{n+2} = x g_{n+1} + g_n\) for \(g \in \{f, \ell\}\), evaluated at a real number \(x > 0\), let \(k\) be a positive integer and \(m\) a natural number, and put \(L = (k + 1)/2\) if \(k\) is odd and \(L = k/2 + 1\) if \(k\) is even. If \(k\) is odd, then

\[\sum_{n \ge L} \frac{\sum_{j=0}^{m} (-1)^j \binom{2m+1}{j} \ell_{2n(2m+1-2j)} \ell_{k(2m+1-2j)}} {\left(\ell_{2n}^2 - (x^2 + 4) f_k^2\right)^{2m+1}} = \sum_{r=1}^{k} \frac{1}{\ell_{2r-1}^{2m+1}},\]

and if \(k\) is even, then

\[\sum_{n \ge L} \frac{\sum_{j=0}^{m} \binom{2m+1}{j} f_{2n(2m+1-2j)} f_{k(2m+1-2j)}} {\left(\ell_{2n}^2 + (x^2 + 4) f_k^2\right)^{2m+1}} = \frac{1}{x^2 + 4} \sum_{r=1}^{k} \frac{1}{\ell_{2r}^{2m+1}}.\]
public theorem_wanted tsum_lucasPoly_odd_pow_even_index {x : ℝ} (hx : 0 < x) {k : ℕ}
    (hk : 0 < k) (m : ℕ) :
    (Odd k → ∑' n : ℕ, (∑ j ∈ Finset.range (m + 1), ((2 * m + 1).choose j : ℝ) * (-1) ^ j *
          aeval x (𝔩 (2 * (n + 𝔏[k]) * (2 * m + 1 - 2 * j))) *
            aeval x (𝔩 (k * (2 * m + 1 - 2 * j)))) /
        (aeval x (𝔩 (2 * (n + 𝔏[k]))) ^ 2 - (x ^ 2 + 4) * aeval x (𝔣 k) ^ 2) ^ (2 * m + 1) =
      ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (𝔩 (2 * r - 1)) ^ (2 * m + 1)) ∧
    (Even k → ∑' n : ℕ, (∑ j ∈ Finset.range (m + 1), ((2 * m + 1).choose j : ℝ) *
          aeval x (𝔣 (2 * (n + 𝔏[k]) * (2 * m + 1 - 2 * j))) *
            aeval x (𝔣 (k * (2 * m + 1 - 2 * j)))) /
        (aeval x (𝔩 (2 * (n + 𝔏[k]))) ^ 2 + (x ^ 2 + 4) * aeval x (𝔣 k) ^ 2) ^ (2 * m + 1) =
      1 / (x ^ 2 + 4) * ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (𝔩 (2 * r)) ^ (2 * m + 1))
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Theorem 1.6.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremOdd-power series over odd-indexed Fibonacci polynomials#●ready to prove

Let \(x > 0\) be real, let \(f_n\) and \(\ell_n\) denote the Fibonacci and Lucas polynomials evaluated at \(x\), given by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and the recurrence \(z_{n+2} = x z_{n+1} + z_n\) for both, and let \(k\) be a positive integer and \(m\) a natural number. Put \(M = (k + 1)/2\) if \(k\) is odd and \(M = k/2\) if \(k\) is even. If \(k\) is odd, then

\[\sum_{n=0}^{\infty} \frac{\sum_{j=0}^{m} \binom{2m+1}{j} (-1)^j f_{(2(n+M)+1)(2m+1-2j)} \ell_{k(2m+1-2j)}}{\left(f_{2(n+M)+1}^2 - f_k^2\right)^{2m+1}} = (x^2 + 4)^m \sum_{r=1}^{k} \frac{1}{f_{2r}^{2m+1}},\]

and if \(k\) is even, then

\[\sum_{n=0}^{\infty} \frac{\sum_{j=0}^{m} \binom{2m+1}{j} \ell_{(2(n+M)+1)(2m+1-2j)} f_{k(2m+1-2j)}}{\left(f_{2(n+M)+1}^2 + f_k^2\right)^{2m+1}} = (x^2 + 4)^m \sum_{r=1}^{k} \frac{1}{f_{2r-1}^{2m+1}}.\]

These are the source's sums over \(n \ge M\) with the summation index shifted to start at \(0\).

public theorem_wanted tsum_fibPoly_odd_pow_odd_index {x : ℝ} (hx : 0 < x) {k : ℕ}
    (hk : 0 < k) (m : ℕ) :
    (Odd k → ∑' n : ℕ, (∑ j ∈ Finset.range (m + 1), ((2 * m + 1).choose j : ℝ) * (-1) ^ j *
          aeval x (𝔣 ((2 * (n + 𝔐[k]) + 1) * (2 * m + 1 - 2 * j))) *
            aeval x (𝔩 (k * (2 * m + 1 - 2 * j)))) /
        (aeval x (𝔣 (2 * (n + 𝔐[k]) + 1)) ^ 2 - aeval x (𝔣 k) ^ 2) ^ (2 * m + 1) =
      (x ^ 2 + 4) ^ m * ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (𝔣 (2 * r)) ^ (2 * m + 1)) ∧
    (Even k → ∑' n : ℕ, (∑ j ∈ Finset.range (m + 1), ((2 * m + 1).choose j : ℝ) *
          aeval x (𝔩 ((2 * (n + 𝔐[k]) + 1) * (2 * m + 1 - 2 * j))) *
            aeval x (𝔣 (k * (2 * m + 1 - 2 * j)))) /
        (aeval x (𝔣 (2 * (n + 𝔐[k]) + 1)) ^ 2 + aeval x (𝔣 k) ^ 2) ^ (2 * m + 1) =
      (x ^ 2 + 4) ^ m * ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (𝔣 (2 * r - 1)) ^ (2 * m + 1))
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Theorem 1.7.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremOdd-power sums with odd-index Lucas polynomial denominators#●ready to prove

Let \(f_n\) and \(\ell_n\) denote the Fibonacci and Lucas polynomials, given by \(f_0 = 0\), \(f_1 = 1\), \(\ell_0 = 2\), \(\ell_1 = x\) and \(g_{n+2} = x g_{n+1} + g_n\) for \(g \in \{f, \ell\}\), evaluated at a real number \(x > 0\), let \(k\) be a positive integer and \(m\) a natural number, and put \(M = (k + 1)/2\) if \(k\) is odd and \(M = k/2\) if \(k\) is even. If \(k\) is odd, then

\[\sum_{n \ge M} \frac{\sum_{j=0}^{m} \binom{2m+1}{j} \ell_{(2n+1)(2m+1-2j)} \ell_{k(2m+1-2j)}} {\left(\ell_{2n+1}^2 + (x^2 + 4) f_k^2\right)^{2m+1}} = \sum_{r=1}^{k} \frac{1}{\ell_{2r}^{2m+1}},\]

and if \(k\) is even, then

\[\sum_{n \ge M} \frac{\sum_{j=0}^{m} (-1)^j \binom{2m+1}{j} f_{(2n+1)(2m+1-2j)} f_{k(2m+1-2j)}} {\left(\ell_{2n+1}^2 - (x^2 + 4) f_k^2\right)^{2m+1}} = \frac{1}{x^2 + 4} \sum_{r=1}^{k} \frac{1}{\ell_{2r-1}^{2m+1}}.\]
public theorem_wanted tsum_lucasPoly_odd_pow_odd_index {x : ℝ} (hx : 0 < x) {k : ℕ}
    (hk : 0 < k) (m : ℕ) :
    (Odd k → ∑' n : ℕ, (∑ j ∈ Finset.range (m + 1), ((2 * m + 1).choose j : ℝ) *
          aeval x (𝔩 ((2 * (n + 𝔐[k]) + 1) * (2 * m + 1 - 2 * j))) *
            aeval x (𝔩 (k * (2 * m + 1 - 2 * j)))) /
        (aeval x (𝔩 (2 * (n + 𝔐[k]) + 1)) ^ 2 + (x ^ 2 + 4) * aeval x (𝔣 k) ^ 2) ^
          (2 * m + 1) =
      ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (𝔩 (2 * r)) ^ (2 * m + 1)) ∧
    (Even k → ∑' n : ℕ, (∑ j ∈ Finset.range (m + 1), ((2 * m + 1).choose j : ℝ) * (-1) ^ j *
          aeval x (𝔣 ((2 * (n + 𝔐[k]) + 1) * (2 * m + 1 - 2 * j))) *
            aeval x (𝔣 (k * (2 * m + 1 - 2 * j)))) /
        (aeval x (𝔩 (2 * (n + 𝔐[k]) + 1)) ^ 2 - (x ^ 2 + 4) * aeval x (𝔣 k) ^ 2) ^ (2 * m + 1) =
      1 / (x ^ 2 + 4) * ∑ r ∈ Finset.Icc 1 k, 1 / aeval x (𝔩 (2 * r - 1)) ^ (2 * m + 1))
Sources
  • Yinqi Lin and Bo Zhou, Infinite Sums Involving Powers of Gibonacci Polynomials, The Fibonacci Quarterly 62 (2024), Article linzhou02172024, Theorem 1.8.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremTelescoping sum of powers of gibonacci polynomial ratios#●ready to prove

Let \(f_n\) and \(l_n\) denote the Fibonacci and Lucas polynomials, given by \(f_0 = 0\), \(f_1 = 1\), \(l_0 = 2\), \(l_1 = x\) and \(g_{n+2} = x g_{n+1} + g_n\) for \(g \in \{f, l\}\), evaluated at a real number \(x > 0\), and let \(\alpha = (x + \sqrt{x^2 + 4})/2\). Then for \(g \in \{f, l\}\), every positive integer \(k\) and all natural numbers \(r\) and \(\lambda\),

\[\sum_{n \ge 0} \left(\frac{g_{(2n+1)k+r}^\lambda}{g_{(2n+1)k}^\lambda} - \frac{g_{(2n+3)k+r}^\lambda}{g_{(2n+3)k}^\lambda}\right) = \frac{g_{k+r}^\lambda}{g_k^\lambda} - \alpha^{r\lambda}.\]
public theorem_wanted tsum_gibonacciPoly_pow_ratio_telescope {x : ℝ} (hx : 0 < x)
    {g : ℕ → ℤ[X]} (hg : g = 𝔣 ∨ g = 𝔩) {k : ℕ} (hk : 0 < k) (r lam : ℕ) :
    ∑' n : ℕ, (aeval x (g ((2 * n + 1) * k + r)) ^ lam / aeval x (g ((2 * n + 1) * k)) ^ lam -
        aeval x (g ((2 * n + 3) * k + r)) ^ lam / aeval x (g ((2 * n + 3) * k)) ^ lam) =
      aeval x (g (k + r)) ^ lam / aeval x (g k) ^ lam - ((x + √(x ^ 2 + 4)) / 2) ^ (r * lam)
Sources
  • Thomas Koshy, More Sums Involving Gibonacci Polynomial Squares Revisited, The Fibonacci Quarterly 62 (2024), Article koshy07202023, Lemma 2.1.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremTelescoping sum of powers of inverse gibonacci polynomial ratios#●ready to prove

Let \(f_n\) and \(l_n\) denote the Fibonacci and Lucas polynomials, given by \(f_0 = 0\), \(f_1 = 1\), \(l_0 = 2\), \(l_1 = x\) and \(g_{n+2} = x g_{n+1} + g_n\) for \(g \in \{f, l\}\), evaluated at a real number \(x > 0\), and let \(\beta = (x - \sqrt{x^2 + 4})/2\). Then for \(g \in \{f, l\}\), every positive integer \(k\) and all natural numbers \(r\) and \(\lambda\),

\[\sum_{n \ge 0} \left(\frac{g_{(2n+1)k}^\lambda}{g_{(2n+1)k+r}^\lambda} - \frac{g_{(2n+3)k}^\lambda}{g_{(2n+3)k+r}^\lambda}\right) = \frac{g_k^\lambda}{g_{k+r}^\lambda} - (-\beta)^{r\lambda}.\]
public theorem_wanted tsum_gibonacciPoly_pow_inv_ratio_telescope {x : ℝ} (hx : 0 < x)
    {g : ℕ → ℤ[X]} (hg : g = 𝔣 ∨ g = 𝔩) {k : ℕ} (hk : 0 < k) (r lam : ℕ) :
    ∑' n : ℕ, (aeval x (g ((2 * n + 1) * k)) ^ lam / aeval x (g ((2 * n + 1) * k + r)) ^ lam -
        aeval x (g ((2 * n + 3) * k)) ^ lam / aeval x (g ((2 * n + 3) * k + r)) ^ lam) =
      aeval x (g k) ^ lam / aeval x (g (k + r)) ^ lam - (-((x - √(x ^ 2 + 4)) / 2)) ^ (r * lam)
Sources
  • Thomas Koshy, More Sums Involving Gibonacci Polynomial Squares Revisited, The Fibonacci Quarterly 62 (2024), Article koshy07202023, Lemma 2.2.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremGibonacci polynomial square sums at even multiples of the index#●ready to prove

Let \(f_n\) and \(l_n\) denote the Fibonacci and Lucas polynomials, given by \(f_0 = 0\), \(f_1 = 1\), \(l_0 = 2\), \(l_1 = x\) and \(g_{n+2} = x g_{n+1} + g_n\) for \(g \in \{f, l\}\), evaluated at a real number \(x > 0\), and let \(\alpha = (x + \sqrt{x^2 + 4})/2\). Let \(g\) be \(f\) with \((\mu, \nu) = (1, -1)\), or \(l\) with \((\mu, \nu) = (x^2 + 4, 1)\). Then for every positive integer \(k\) and every natural number \(r\),

\[\sum_{n \ge 1} \frac{(-1)^{k+1} \mu \nu f_r f_{2k}}{g_{2nk}^2 + (-1)^k \mu \nu f_k^2} = \frac{g_{k+r}}{g_k} - \alpha^r.\]

The extracted statement of this theorem prints the numerator with \((-1)^k\) in place of \((-1)^{k+1}\), which negates the left side and makes the identity false (for \(x = 1\), \(g = f\) and \(k = r = 1\) that left side is \((\sqrt{5} - 1)/2\) while the right side is \((1 - \sqrt{5})/2\)); the paper's proof and its corollaries use the sign stated here.

public theorem_wanted tsum_fib_mul_div_gibonacciPoly_sq_add {x : ℝ} (hx : 0 < x)
    {g : ℕ → ℤ[X]} {μ ν : ℝ}
    (hg : (g = 𝔣 ∧ μ = 1 ∧ ν = -1) ∨ (g = 𝔩 ∧ μ = x ^ 2 + 4 ∧ ν = 1)) {k : ℕ} (hk : 0 < k)
    (r : ℕ) :
    ∑' n : ℕ, (-1) ^ (k + 1) * μ * ν * aeval x (𝔣 r) * aeval x (𝔣 (2 * k)) /
        (aeval x (g (2 * (n + 1) * k)) ^ 2 + (-1) ^ k * μ * ν * aeval x (𝔣 k) ^ 2) =
      aeval x (g (k + r)) / aeval x (g k) - ((x + √(x ^ 2 + 4)) / 2) ^ r
Sources
  • Thomas Koshy, More Sums Involving Gibonacci Polynomial Squares Revisited, The Fibonacci Quarterly 62 (2024), Article koshy07202023, Theorem 3.1.
Uses 1
Statement usesGeneralized Fibonacci polynomials

TheoremGibonacci polynomial square sums at shifted even multiples of the index#●ready to prove

Let \(f_n\) and \(l_n\) denote the Fibonacci and Lucas polynomials, given by \(f_0 = 0\), \(f_1 = 1\), \(l_0 = 2\), \(l_1 = x\) and \(g_{n+2} = x g_{n+1} + g_n\) for \(g \in \{f, l\}\), evaluated at a real number \(x > 0\), and let \(\beta = (x - \sqrt{x^2 + 4})/2\). Let \(g\) be \(f\) with \((\mu, \nu) = (1, -1)\), or \(l\) with \((\mu, \nu) = (x^2 + 4, 1)\). Then for every positive integer \(k\) and every natural number \(r\),

\[\sum_{n \ge 1} \frac{(-1)^k \mu \nu f_r f_{2k}}{g_{2nk+r}^2 + (-1)^{r+k} \mu \nu f_k^2} = \frac{g_k}{g_{k+r}} - (-\beta)^r.\]
public theorem_wanted tsum_fib_mul_div_gibonacciPoly_shift_sq_add {x : ℝ} (hx : 0 < x)
    {g : ℕ → ℤ[X]} {μ ν : ℝ}
    (hg : (g = 𝔣 ∧ μ = 1 ∧ ν = -1) ∨ (g = 𝔩 ∧ μ = x ^ 2 + 4 ∧ ν = 1)) {k : ℕ} (hk : 0 < k)
    (r : ℕ) :
    ∑' n : ℕ, (-1) ^ k * μ * ν * aeval x (𝔣 r) * aeval x (𝔣 (2 * k)) /
        (aeval x (g (2 * (n + 1) * k + r)) ^ 2 + (-1) ^ (r + k) * μ * ν * aeval x (𝔣 k) ^ 2) =
      aeval x (g k) / aeval x (g (k + r)) - (-((x - √(x ^ 2 + 4)) / 2)) ^ r
Sources
  • Thomas Koshy, More Sums Involving Gibonacci Polynomial Squares Revisited, The Fibonacci Quarterly 62 (2024), Article koshy07202023, Theorem 3.2.
Uses 1
Statement usesGeneralized Fibonacci polynomials
29 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.