Fibonacci and Lucas numbers

Identities, sums, reciprocal series, determinants and generating functions specifically for Fibonacci and Lucas numbers.

• Bernoulli–Fibonacci and Euler–Lucas double sums
• Binomial sums of Fibonacci and Lucas numbers
• Fibonacci identities via Fibonacci functions
• Fibonacci representations with polynomial coefficients
• Fibonacci series for π²
• Sury's identity and its extensions

TheoremAlfred's determinant of consecutive Fibonacci powers#✓fully proved

Let \(F_n\) denote the Fibonacci numbers extended to all integers \(n\) by \(F_0 = 0\), \(F_1 = 1\) and \(F_{n+2} = F_{n+1} + F_n\), so that \(F_{-n} = (-1)^{n+1} F_n\). For every natural number \(r\) and all integers \(s\) and \(k\), the \((r+1) \times (r+1)\) integer matrix whose entry in row \(i\) and column \(j\), for \(0 \le i, j \le r\), is \(F_{s+ik}^{\,r-j} \, F_{s+(i+1)k}^{\,j}\) has determinant \((-1)^{|e|} \, F_k^{\binom{r+1}{2}} \prod_{\ell=1}^{r} F_{k\ell}^{\,r+1-\ell}\), where \(e = (s+1)\binom{r+1}{2} + k\binom{r+1}{3}\).

This is a slight variation of a result of Brother U. Alfred, "Some determinants involving powers of Fibonacci numbers," Fibonacci Quarterly 2 (1964), 81–92.

theorem alfred_consecutive_fibonacci_powers_determinant
    (r : ℕ) (s k : ℤ) :
    Matrix.det (fun (i j : Fin (r + 1)) =>
      Int.fib (s + (i.val : ℤ) * k) ^ (r - j.val) *
        Int.fib (s + ((i.val : ℤ) + 1) * k) ^ j.val) =
      (-1 : ℤ) ^ (((s + 1) * (Nat.choose (r + 1) 2 : ℤ) +
        k * (Nat.choose (r + 1) 3 : ℤ)).natAbs) *
        (Int.fib k ^ Nat.choose (r + 1) 2 *
          Finset.prod (Finset.Icc 1 r)
            (fun ℓ => Int.fib (k * (ℓ : ℤ)) ^ (r + 1 - ℓ)))

Sources

• Aram Tangboonduangjit and Thotsaporn Thanatipanonda, "Determinants Containing Powers of Generalized Fibonacci Numbers," Journal of Integer Sequences 19 (2016), Article 16.7.1, Corollary, lines 406–418, https://cs.uwaterloo.ca/journals/JIS/VOL19/Tangboonduangjit/aram5.tex

TheoremBrousseau's alternating series of reciprocal Fibonacci squares#✓fully proved

Let \(F_n\) denote the Fibonacci numbers, with \(F_0 = 0\), \(F_1 = 1\) and \(F_{n+2} = F_{n+1} + F_n\). For every positive integer \(q\), the real series \(\sum_{k \ge 1} (-1)^{k-1} \frac{F_{2k+q}}{F_k^2 \, F_{k+q}^2}\) is unconditionally summable, with sum \(\frac{1}{F_q} \sum_{k=1}^{q} \frac{(-1)^{k-1}}{F_k^2}\).

Adegoke's generalization has a further integer parameter \(n\) and assumes that \(q\) is even or \(nq\) is odd; this is its case \(n = 1\), in which that assumption holds for every positive \(q\).

theorem brousseau_fibonacci_reciprocal_sum (q : ℕ) (hq : 0 < q) :
    HasSum
      (fun k : ℕ =>
        ((-1 : ℝ) ^ k * Nat.fib (2 * (k + 1) + q)) /
          ((Nat.fib (k + 1) : ℝ) ^ 2 * (Nat.fib (k + 1 + q) : ℝ) ^ 2))
      ((Nat.fib q : ℝ)⁻¹ *
        ∑ k ∈ Finset.Icc 1 q, ((-1 : ℝ) ^ (k - 1)) / (Nat.fib k : ℝ) ^ 2)

Sources

• Kunle Adegoke, "Generalizations of the Reciprocal Fibonacci-Lucas Sums of Brousseau," Journal of Integer Sequences 21 (2018), https://cs.uwaterloo.ca/journals/JIS/VOL21/Adegoke/ade3.tex; controlling theorem, equation, and specialization at lines 1135–1148; original reference: Brother Alfred Brousseau, "Fibonacci-Lucas Infinite Series — Research Topic," Fibonacci Quarterly 7 (1969), 211–217, Formula (6), cited at source line 1414.

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.