Binomial sums of Fibonacci and Lucas numbers

TheoremPascal's rule for binomial coefficients#✓fully proved

For all natural numbers \(n\) and \(i\), \(\binom{n+1}{i+1} = \binom{n}{i} + \binom{n}{i+1}\), as an identity of integers.

theorem choose_succ_int (n i : ℕ) :
    (Nat.choose (n + 1) (i + 1) : ℤ) =
      (Nat.choose n i : ℤ) + (Nat.choose n (i + 1) : ℤ)

Used by 1

Used byAlternating binomial sum of Fibonacci numbers

TheoremFibonacci step in the alternating binomial sum#✓fully proved

Let \(F_m\) denote the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). For natural numbers \(n\), \(k\) and \(i\) with \(i \le n\), \(F_{2n+2-i+k} - F_{2n+1-i+k} = F_{2n-i+k}\), as an identity of integers.

theorem fib_conv_step (n k i : ℕ) (hi : i ≤ n) :
    (Nat.fib (2 * n + 2 - i + k) : ℤ) - (Nat.fib (2 * n + 1 - i + k) : ℤ) =
      (Nat.fib (2 * n - i + k) : ℤ)

Used by 1

Used byAlternating binomial sum of Fibonacci numbers

TheoremAlternating binomial sum of Fibonacci numbers#✓fully proved

Let \(F_m\) denote the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). For all natural numbers \(n\) and \(k\),

\[\sum_{i=0}^{n} (-1)^i \binom{n}{i} F_{2n-i+k} = F_k.\]

theorem binomial_fibonacci_convolution (n k : ℕ) :
    Finset.sum (Finset.range (n + 1)) (fun i =>
      (-1 : ℤ) ^ i * (Nat.fib (2 * n - i + k) : ℤ) * (Nat.choose n i : ℤ)) =
    (Nat.fib k : ℤ)

Sources

Brian Hopkins and Aram Tangboonduangjit, "Scaled Fibonacci- and Lucas-Producing Rational Polynomials," Journal of Integer Sequences 25 (2022), Article 22.3.5 (Corollary generalizing Corollary cor51(a), lines 989–1000), https://cs.uwaterloo.ca/journals/JIS/VOL25/Hopkins/tang25.tex. The sum is the n-th forward difference, which telescopes by Pascal's rule and fib (m + 2) = fib m + fib (m + 1).

Uses 2

Proof usesPascal's rule for binomial coefficients · Fibonacci step in the alternating binomial sum

TheoremThe square root of 5 is nonzero#✓fully proved

The real square root \(\sqrt{5}\) is not equal to \(0\).

This is used to clear the denominators in Binet's formula.

theorem sqrt5_ne : √5 ≠ (0 : ℝ)

Used by 1

Used byChurch–Bicknell convolution over the reals

TheoremBinet's formula for the Lucas numbers#✓fully proved

For every natural number \(n\), \(\varphi^n + \psi^n = L_n\) as real numbers, where \(\varphi = (1 + \sqrt{5})/2\) is the golden ratio, \(\psi = (1 - \sqrt{5})/2\) is its conjugate, and \(L_n\) is the \(n\)-th Lucas number.

theorem cb_lucas_binet (n : ℕ) : φ ^ n + ψ ^ n = (lucasNumber n : ℝ)

Uses 1 · Used by 1

Statement usesLucas numbers

Used byChurch–Bicknell convolution over the reals

TheoremChurch–Bicknell convolution over the reals#✓fully proved

For every natural number \(n\),

\[\sum_{k=0}^{n} \binom{n}{k} F_k F_{n-k} = \frac{2^n L_n - 2}{5}\]

holds as an identity of real numbers, where \(F_k\) is the \(k\)-th Fibonacci number and \(L_n\) is the \(n\)-th Lucas number.

theorem cb_keyR (n : ℕ) :
    (∑ k ∈ Finset.range (n + 1),
      (Nat.choose n k : ℝ) * (Nat.fib k : ℝ) * (Nat.fib (n - k) : ℝ)) =
      ((2 : ℝ) ^ n * (lucasNumber n : ℝ) - 2) / 5

Uses 3 · Used by 1

Statement usesLucas numbers

Proof usesBinet's formula for the Lucas numbers · The square root of 5 is nonzero

Used byChurch–Bicknell Fibonacci binomial convolution

TheoremChurch–Bicknell Fibonacci binomial convolution#✓fully proved

For every natural number \(n\),

\[\sum_{k=0}^{n} \binom{n}{k} F_k F_{n-k} = \frac{2^n L_n - 2}{5}\]

holds as an identity of rational numbers, where \(F_k\) is the \(k\)-th Fibonacci number and \(L_n\) is the \(n\)-th Lucas number.

theorem church_bicknell_fibonacci_convolution (n : ℕ) :
    (∑ k ∈ Finset.range (n + 1),
        (Nat.choose n k : ℚ) * Nat.fib k * Nat.fib (n - k)) =
      (((2 : ℚ) ^ n * lucasNumber n - 2) / 5)

Sources

Ira M. Gessel and Ishan Kar, "Binomial Convolutions for Rational Power Series," Journal of Integer Sequences 27 (2024), Article 24.1.3, equation e-cb1 (attributed there to C. A. Church and Marjorie Bicknell, "Exponential generating functions for Fibonacci identities," Fibonacci Quarterly 11 (1973), 275–281). The proof follows the Binet-form computation in the JIS article: with φ, ψ the golden ratio and its conjugate, expand (φ^k - ψ^k)(φ^(n-k) - ψ^(n-k)) and evaluate the four resulting binomial sums by the binomial theorem.

Uses 2

Statement usesLucas numbers

Proof usesChurch–Bicknell convolution over the reals

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.