k-generalized Fibonacci numbers

DefinitionOctanacci window#✓fully proved

The octanacci window is the sequence \((w_n)_{n \ge 0}\) of \(8\)-tuples of natural numbers with \(w_0 = (1, 1, 2, 4, 8, 16, 32, 64)\) and, if \(w_n = (a_1, \dots, a_8)\), then \(w_{n+1} = (a_2, \dots, a_8, a_1 + a_2 + \dots + a_8)\). The octanacci numbers \(f_n\) are the first entries of these tuples, so \(w_n = (f_n, f_{n+1}, \dots, f_{n+7})\).

def octanacciWindow : Nat → Nat × Nat × Nat × Nat × Nat × Nat × Nat × Nat
  | 0 => (1, 1, 2, 4, 8, 16, 32, 64)
  | n + 1 =>
    match octanacciWindow n with
    | (a, b, c, d, e, f, g, h) =>
      (b, c, d, e, f, g, h, a + b + c + d + e + f + g + h)
Used by 1
Used byOctanacci numbers

DefinitionOctanacci numbers#✓fully proved

The octanacci sequence \((f_n)_{n \ge 0}\) of natural numbers is defined by \(f_0 = f_1 = 1\), \(f_n = 2^{n-1}\) for \(2 \le n \le 7\), and \(f_n = f_{n-1} + f_{n-2} + \dots + f_{n-8}\) for \(n \ge 8\). It begins \(1, 1, 2, 4, 8, 16, 32, 64, 128, 255, \dots\), and its generating function is \(1/(1 - t - t^2 - \dots - t^8)\).

def octanacciNumber (n : Nat) : Nat :=
  (octanacciWindow n).1
Uses 1
Statement usesOctanacci window

DefinitionN-step Fibonacci numbers#✓fully proved

For a natural number \(N\), the \(N\)-step Fibonacci numbers \(F^{(N)}_n\) (\(n \ge 0\)), in the convention of Noe and Post, are defined by \(F^{(N)}_0 = 0\), \(F^{(N)}_1 = 1\) and, for \(n \ge 2\), \(F^{(N)}_n = \sum_{i=1}^{N} F^{(N)}_{n-i}\), where a term whose index \(n - i\) is negative counts as \(0\). In particular \(F^{(0)}_n = 0\) for \(n \ge 2\).

def nStepFibonacci (N : ℕ) : ℕ → ℕ
  | 0 => 0
  | 1 => 1
  | n + 2 => ∑ i : Fin N, nStepFibonacci N (n + 1 - i)
decreasing_by omega
Sources
  • Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Section 4.4.
Used by 4
Used byRecurrence for the N-step Fibonacci numbers · First N-step Fibonacci number · The tribonacci number with index 5 · Zeroth N-step Fibonacci number

TheoremRecurrence for the N-step Fibonacci numbers#✓fully proved

For all natural numbers \(N\) and \(n\), the \(N\)-step Fibonacci numbers \(F^{(N)}\) satisfy \(F^{(N)}_{n+2} = \sum_{i=0}^{N-1} F^{(N)}_{\max(n+1-i,\,0)}\).

theorem nStepFibonacci_add_two (N n : ℕ) :
    nStepFibonacci N (n + 2) = ∑ i : Fin N, nStepFibonacci N (n + 1 - i)
Sources
  • Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Section 4.4.
Uses 1
Statement usesN-step Fibonacci numbers

TheoremZeroth N-step Fibonacci number#✓fully proved

For every natural number \(N\), the \(N\)-step Fibonacci number \(F^{(N)}_0\) equals \(0\).

@[simp] theorem nStepFibonacci_zero (N : ℕ) : nStepFibonacci N 0 = 0
Sources
  • Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Section 4.4.
Uses 1 · Used by 1
Statement usesN-step Fibonacci numbers
Used byThe tribonacci number with index 5

TheoremFirst N-step Fibonacci number#✓fully proved

For every natural number \(N\), the \(N\)-step Fibonacci number \(F^{(N)}_1\) equals \(1\).

@[simp] theorem nStepFibonacci_one (N : ℕ) : nStepFibonacci N 1 = 1
Sources
  • Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Section 4.4.
Uses 1 · Used by 1
Statement usesN-step Fibonacci numbers
Used byThe tribonacci number with index 5

TheoremThe tribonacci number with index 5#✓fully proved

The \(3\)-step Fibonacci number \(F^{(3)}_5\) equals \(7\).

The tribonacci numbers \(F^{(3)}_0, \dots, F^{(3)}_5\) are \(0, 1, 1, 2, 4, 7\).

theorem nStepFibonacci_three_five : nStepFibonacci 3 5 = 7
Sources
  • Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Section 4.4.
Uses 3
Statement usesN-step Fibonacci numbers
Proof usesFirst N-step Fibonacci number · Zeroth N-step Fibonacci number

TheoremBounds on the dominant root of the k-generalized Fibonacci polynomial#✓fully proved

Let \(k\) be a natural number and let \(\alpha > 1\) be a real number with \(\alpha^k = \sum_{i=0}^{k-1} \alpha^i\). Then \(2 - 1/k < \alpha < 2\), and if \(k \ge 4\), moreover \(2 - 1/(3k) < \alpha < 2\).

theorem dominant_root_bounds_k_generalized_fibonacci
    (k : ℕ)
    (α : ℝ)
    (hα : 1 < α)
    (hroot : α ^ k = ∑ i ∈ Finset.range k, α ^ i) :
    (2 - 1 / (k : ℝ) < α ∧ α < 2) ∧
      (4 ≤ k → 2 - 1 / (3 * (k : ℝ)) < α ∧ α < 2)
Sources

TheoremSimplified Binet formula for k-generalized Fibonacci numbers from an initial window#✓fully proved

Let \(k \ge 2\) and let \(F : \mathbb{Z} \to \mathbb{Z}\) satisfy \(F(n) = 0\) for all integers \(n\) with \(2 - k \le n < 1\), \(F(1) = 1\), and \(F(n) = \sum_{i=0}^{k-1} F(n - 1 - i)\) for all integers \(n > 1\). Let \(\alpha\) be a positive real number with \(\alpha^k = \sum_{i=0}^{k-1} \alpha^i\), and put \(c = (\alpha - 1)/(2 + (k + 1)(\alpha - 2))\). Then for every integer \(n \ge 2 - k\), \(F(n) = \lfloor c\,\alpha^{n-1} + 1/2 \rfloor\).

Proof: We follow Dresden–Du's recurrence and first-crossing route, replacing their appeal to the non-dominant-root results of Miles (1960) and Miller (1971) with an exact positive weighted invariant.

public theorem dresden_du_simplified_binet_of_initial_window :
    ∀ (k : ℕ) (_hk : 2 ≤ k) (F : ℤ → ℤ)
      (_hFzero : ∀ n : ℤ, 2 - (k : ℤ) ≤ n → n < 1 → F n = 0)
      (_hFone : F 1 = 1)
      (_hFrec : ∀ n : ℤ, 1 < n → F n = ∑ i ∈ Finset.range k, F (n - 1 - (i : ℤ))) (α : ℝ)
      (_hαpos : 0 < α) (_hαroot : α ^ k = ∑ i ∈ Finset.range k, α ^ i),
      ∀ n : ℤ, 2 - (k : ℤ) ≤ n →
        F n = ⌊((α - 1) / (2 + ((k : ℝ) + 1) * (α - 2))) * α ^ (n - 1) + 1 / 2⌋
Sources
Used by 1
Used byDresden–Du simplified Binet formula

TheoremDresden–Du simplified Binet formula#✓fully proved

Let \(k \ge 2\) and let \(F : \mathbb{Z} \to \mathbb{Z}\) satisfy \(F(n) = 0\) for all integers \(n < 1\), \(F(1) = 1\), and \(F(n) = \sum_{i=0}^{k-1} F(n - 1 - i)\) for all integers \(n > 1\). Let \(\alpha\) be a positive real number with \(\alpha^k = \sum_{i=0}^{k-1} \alpha^i\), and suppose that every positive real \(\beta\) with \(\beta^k = \sum_{i=0}^{k-1} \beta^i\) equals \(\alpha\). Put \(c = (\alpha - 1)/(2 + (k + 1)(\alpha - 2))\). Then for every integer \(n \ge 2 - k\), \(F(n) = \lfloor c\,\alpha^{n-1} + 1/2 \rfloor\).

public theorem dresden_du_simplified_binet :
    ∀ (k : ℕ) (_hk : 2 ≤ k) (F : ℤ → ℤ) (_hFneg : ∀ n : ℤ, n < 1 → F n = 0)
      (_hFone : F 1 = 1)
      (_hFrec : ∀ n : ℤ, 1 < n → F n = ∑ i ∈ Finset.range k, F (n - 1 - (i : ℤ))) (α : ℝ)
      (_hαpos : 0 < α) (_hαroot : α ^ k = ∑ i ∈ Finset.range k, α ^ i)
      (_hαuniq : ∀ β : ℝ, 0 < β → β ^ k = ∑ i ∈ Finset.range k, β ^ i → β = α),
      ∀ n : ℤ, 2 - (k : ℤ) ≤ n →
        F n = ⌊((α - 1) / (2 + ((k : ℝ) + 1) * (α - 2))) * α ^ (n - 1) + 1 / 2⌋
Sources
Uses 1
Proof usesSimplified Binet formula for k-generalized Fibonacci numbers from an initial window

TheoremPower-weighted convolution of Fibonacci \(m\)-step numbers#✓fully proved

Let \(m \ge 1\) and let \(F \colon \mathbb{N} \to \mathbb{N}\) satisfy \(F(0) = 0\), \(F(1) = 1\) and \(F(k) = \sum_{j=1}^{m} F(k - j)\) for every \(k \ge 2\), where a term \(F(k - j)\) with \(j > k\) is read as \(F(0) = 0\). Then for every natural number \(n\),

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

where the subtraction on the right is taken in \(\mathbb{N}\) (truncated at \(0\)).

The initial conditions are those of the paper's definition of Fibonacci \(m\)-step numbers (lines 126–133), whose values at negative indices are \(0\). The paper states the theorem for \(m \ge 3\); the cases \(m = 1\) and \(m = 2\) also hold, so the hypothesis here is \(m \ge 1\).

theorem two_pow_convolution_mstep_fibonacci (F : ℕ → ℕ) (m n : ℕ)
    (hm : 1 ≤ m) (h0 : F 0 = 0) (h1 : F 1 = 1)
    (hrec : ∀ k : ℕ, 2 ≤ k → F k = ∑ j ∈ Finset.range m, F (k - (j + 1))) :
    (∑ j ∈ Finset.range (n + 1), 2 ^ j * F (n - j)) =
      2 ^ (n + m - 1) - F (n + 1 + m)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers," Journal of Integer Sequences 27 (2024), Article 24.8.8, Theorem, lines 453–459, https://cs.uwaterloo.ca/journals/JIS/VOL27/Gryszka/gryszka12.tex

TheoremBinet asymptotics for weighted generalized Fibonacci sequences, positive-root form#✓fully proved

Let \(r \ge 2\), let \(A_1, \dots, A_r\) and \(c_1, \dots, c_r\) be nonnegative real numbers with \(A_r > 0\) and \(c_j > 0\) for some \(j\), and suppose that the indices \(j\) with \(A_j > 0\) have greatest common divisor \(1\). Let \(a_0, a_1, a_2, \dots\) be the real sequence with \(a_n = c_{n+1}\) for \(0 \le n < r\) and \(a_n = \sum_{j=1}^{r} A_j a_{n-j}\) for \(n \ge r\), and let \(p(x) = x^r - \sum_{j=1}^{r} A_j x^{r-j}\) be its characteristic polynomial. Let \(\lambda > 0\) be a root of \(p\). Then there is a constant \(C > 0\) such that \(a_n = C \lambda^n + o(\lambda^n)\) as \(n \to \infty\), and \(a_{n+1} / a_n \to \lambda\).

MetaMathlibExt.binet_general · 22 lines 
theorem binet_general
    (r : ℕ) (hr : 2 ≤ r)
    (A c : Fin r → ℝ)
    (hA : ∀ k, 0 ≤ A k)
    (hc : ∀ k, 0 ≤ c k)
    (hAr : ∃ i : Fin r, i.val + 1 = r ∧ 0 < A i)
    (hcpos : ∃ k₀, 0 < c k₀)
    (hgcd : ∀ d : ℕ, (∀ k : Fin r, 0 < A k → d ∣ k.val + 1) → d = 1)
    (a : ℕ → ℝ)
    (ha_init : ∀ n (h : n < r), a n = c ⟨n, h⟩)
    (ha_rec : ∀ n, r ≤ n → a n = Finset.sum Finset.univ (fun k : Fin r => A k * a (n - 1 - k.val)))
    (p : Polynomial ℝ)
    (hp : p = Polynomial.X ^ r -
      Finset.sum Finset.univ (fun k : Fin r =>
        Polynomial.C (A k) * Polynomial.X ^ (r - 1 - k.val)))
    (lam : ℝ)
    (hlam_pos : 0 < lam)
    (hlam_root : p.IsRoot lam) :
    ∃ C : ℝ, 0 < C ∧
      Asymptotics.IsLittleO Filter.atTop (fun n => a n - C * lam ^ n)
        (fun n => lam ^ n) ∧
      Filter.Tendsto (fun n => a (n + 1) / a n) Filter.atTop (nhds lam)
Used by 1
Used byBinet asymptotics for weighted generalized Fibonacci sequences

TheoremBinet asymptotics for weighted generalized Fibonacci sequences#✓fully proved

Let \(r \ge 2\), let \(A_1, \dots, A_r\) and \(c_1, \dots, c_r\) be nonnegative real numbers with \(A_r > 0\) and \(c_j > 0\) for some \(j\), and suppose that the indices \(j\) with \(A_j > 0\) have greatest common divisor \(1\). Let \(a_0, a_1, a_2, \dots\) be the real sequence with \(a_n = c_{n+1}\) for \(0 \le n < r\) and \(a_n = \sum_{j=1}^{r} A_j a_{n-j}\) for \(n \ge r\), and let \(p(x) = x^r - \sum_{j=1}^{r} A_j x^{r-j}\) be its characteristic polynomial. Let \(\lambda > 0\) be a root of \(p\) that is not a root of the derivative \(p'\), and such that every complex root \(z\) of \(p\) satisfies \(|z| \le \lambda\), with \(|z| = \lambda\) only for \(z = \lambda\). Then there is a constant \(C > 0\) such that \(a_n = C \lambda^n + o(\lambda^n)\) as \(n \to \infty\), and \(a_{n+1} / a_n \to \lambda\).

The source indexes the sequence from \(1\); the \(a_n\) here is the source's \(a_{n+1}\), and \(A_j\), \(c_j\) are the source's weights and initial values.

MetaMathlibExt.binet · 24 lines 
theorem binet
    (r : ℕ) (hr : 2 ≤ r)
    (A c : Fin r → ℝ)
    (hA : ∀ k, 0 ≤ A k)
    (hc : ∀ k, 0 ≤ c k)
    (hAr : ∃ i : Fin r, i.val + 1 = r ∧ 0 < A i)
    (hcpos : ∃ k₀, 0 < c k₀)
    (hgcd : ∀ d : ℕ, (∀ k : Fin r, 0 < A k → d ∣ k.val + 1) → d = 1)
    (a : ℕ → ℝ)
    (ha_init : ∀ n (h : n < r), a n = c ⟨n, h⟩)
    (ha_rec : ∀ n, r ≤ n → a n = Finset.sum Finset.univ (fun k : Fin r => A k * a (n - 1 - k.val)))
    (p : Polynomial ℝ)
    (hp : p = Polynomial.X ^ r -
      Finset.sum Finset.univ (fun k : Fin r =>
        Polynomial.C (A k) * Polynomial.X ^ (r - 1 - k.val)))
    (lam : ℝ)
    (hlam_pos : 0 < lam)
    (hlam_root : p.IsRoot lam)
    (hlam_simple : ¬ p.derivative.IsRoot lam)
    (hlam_dom : ∀ z : ℂ, (p.map Complex.ofRealHom).IsRoot z → ‖z‖ ≤ lam ∧ (‖z‖ = lam → z = ↑lam)) :
    ∃ C : ℝ, 0 < C ∧
      Asymptotics.IsLittleO Filter.atTop (fun n => a n - C * lam ^ n)
        (fun n => lam ^ n) ∧
      Filter.Tendsto (fun n => a (n + 1) / a n) Filter.atTop (nhds lam)
Sources
  • Passawan Noppakaew and Thanakorn Prinyasart, "Complete Sequences of Weighted r-Generalized Fibonacci Powers," Journal of Integer Sequences 24 (2021), Article 21.5.4, Proposition, lines 119–126, https://cs.uwaterloo.ca/journals/JIS/VOL24/Prinyasart/prin3.tex. It follows from binet_general; the hypotheses hlam_simple and hlam_dom are unused and keep the source's shape.
Uses 1
Proof usesBinet asymptotics for weighted generalized Fibonacci sequences, positive-root form

DefinitionInitial segments of the Fibonacci \(m\)-step sequence#✓fully proved

For natural numbers \(m\) and \(n\), this is the list of integers \([F_0, F_1, \dots, F_n]\), built recursively: the list for \(n = 0\) is \([0]\), the list for \(n = 1\) is \([0, 1]\), and for \(n \ge 2\) the list for \(n\) is the list for \(n - 1\) followed by \(F_n = \sum_{j=1}^{m} F_{n-j}\), where \(F_i = 0\) for \(i < 0\).

def fibStepSeq (m : ℕ) : ℕ → List ℤ
  | 0 => [0]
  | 1 => [0, 1]
  | n + 2 =>
      let prev := fibStepSeq m (n + 1)
      prev ++ [∑ j ∈ Finset.Icc 1 m, prev.getD (n + 2 - j) 0]
Used by 1
Used byFibonacci \(m\)-step numbers

DefinitionFibonacci \(m\)-step numbers#✓fully proved

For natural numbers \(m\) and \(n\), the integer \(F^{(m)}_n\) is defined by \(F^{(m)}_0 = 0\), \(F^{(m)}_1 = 1\) and \(F^{(m)}_n = \sum_{j=1}^{m} F^{(m)}_{n-j}\) for \(n \ge 2\), where \(F^{(m)}_i = 0\) for \(i < 0\).

def fibStep (m n : ℕ) : ℤ := (fibStepSeq m n).getD n 0
Uses 1 · Used by 40
Statement usesInitial segments of the Fibonacci \(m\)-step sequence
Used byConvolution of an even number of consecutive Fibonacci step sequences · Triple convolution of two consecutive Fibonacci step sequences with a third · Closed form of the Fibonacci–tribonacci–tetranacci triple sum · Two convolution forms of the Fibonacci–tribonacci–tetranacci triple sum · Convolution of four consecutive Fibonacci step sequences · Convolution of an odd number of consecutive Fibonacci step sequences · Triple convolution of Pell numbers with two consecutive Fibonacci step sequences · Pell–Fibonacci–tribonacci triple sum via a Pell–tribonacci convolution · Generating function of the Fibonacci \(m\)-step numbers · Double partial sums of Fibonacci step numbers · Convolution of the Fibonacci \(6\)-step numbers with the Fibonacci numbers · Partial sums of the Fibonacci \(m\)-step numbers · Convolution of the Fibonacci numbers with tribonacci minus tetranacci · Convolution of the Fibonacci and tetranacci numbers · Convolution of the Fibonacci and tribonacci numbers · Convolution of the \(m\)-step Fibonacci numbers with consecutive sums of the \((m+2)\)-step ones · Convolution of the \(m\)-step and \((m-2)\)-step Fibonacci numbers via Jacobsthal numbers · Truncated convolution of the \(m\)-step and \((m+1)\)-step Fibonacci numbers · Convolution of the \((m-1)\)-step and \(m\)-step Fibonacci numbers against powers of two · Exchange identity for convolutions of \((m-2)\)-, \((m-1)\)- and \(m\)-step Fibonacci numbers · Sum of \(2m + 2\) consecutive Fibonacci \(m\)-step numbers · Alternating sum of differences of \(2m\)-step and \((2m-2)\)-step Fibonacci numbers · Alternating sums of differences of odd-order Fibonacci step numbers · Convolution of the Pell numbers with the Fibonacci numbers · Iterated convolution of Fibonacci \(m\)-step and \((m+p)\)-step numbers · Convolution of the Fibonacci 4-step and 5-step numbers · Convolution of the Fibonacci 3-step numbers with differences of 4- and 5-step numbers · Convolution of the Fibonacci 3-step and 4-step numbers · Convolution of the Fibonacci 3-step and 4-step numbers as a sum weighted by powers of 2 · Difference of the Fibonacci 3-step and 2-step numbers as a convolution · Triple convolution of the Fibonacci 2-, 4- and 5-step numbers · Triple convolution of the Fibonacci 2-, 3- and 5-step numbers · Four-fold convolution of the Fibonacci, tribonacci, tetranacci and pentanacci numbers · Closed form for the Pell–Fibonacci–tribonacci triple convolution · Triple convolution of the tribonacci, tetranacci and pentanacci numbers · Convolution of the Fibonacci and pentanacci numbers · Convolution of the Jacobsthal and tribonacci numbers · Alternating sum of the tribonacci numbers · Convolution of the pentanacci and tribonacci numbers · Convolution of the pentanacci and tribonacci numbers, second closed form

DefinitionJacobsthal numbers#✓fully proved

The Jacobsthal numbers are the integers \(J_n\) defined by \(J_0 = 0\), \(J_1 = 1\) and \(J_{n+2} = J_{n+1} + 2 J_n\) for all \(n \ge 0\).

def jacobsthalSeq : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => jacobsthalSeq (n + 1) + 2 * jacobsthalSeq n
Used by 2
Used byConvolution of the \(m\)-step and \((m-2)\)-step Fibonacci numbers via Jacobsthal numbers · Convolution of the Jacobsthal and tribonacci numbers

DefinitionGenerating function of the Fibonacci \(m\)-step numbers#✓fully proved

For a natural number \(m\), \(F^{(m)}(X)\) is the formal power series \(\sum_{n \ge 0} F^{(m)}_n X^n\) with rational coefficients, where \(F^{(m)}_n\) is the \(n\)-th Fibonacci \(m\)-step number.

noncomputable def fibStepGF (m : ℕ) : PowerSeries ℚ :=
  PowerSeries.mk fun n => (fibStep m n : ℚ)
Uses 1 · Used by 4
Statement usesFibonacci \(m\)-step numbers
Used byGenerating-function form of the triple convolution with two consecutive step sequences · A product identity for four consecutive Fibonacci step generating functions · A product identity for three consecutive Fibonacci step generating functions · A product identity for Fibonacci step generating functions of orders \(m\), \(m+p\), \(m+p+q\)

DefinitionSums over compositions#✓fully proved

Given integer sequences \(a_0, \dots, a_{r-1}\) and a natural number \(n\), the sum over the compositions \(K(r, n)\) of \(n\) into \(r\) nonnegative parts is the sum, over all \((k_0, \dots, k_{r-1}) \in \mathbb{N}^r\) with \(k_0 + \dots + k_{r-1} = n\), of \(\prod_{i=0}^{r-1} a_i(k_i)\).

def compProdSum {r : ℕ} (seqs : Fin r → ℕ → ℤ) (n : ℕ) : ℤ :=
  ∑ k ∈ (Finset.univ : Finset (Fin r → Fin (n + 1))).filter
      (fun k => ∑ i, (k i).val = n), ∏ i, seqs i (k i).val
Used by 13
Used byConvolution of an even number of consecutive Fibonacci step sequences · Triple convolution of two consecutive Fibonacci step sequences with a third · Closed form of the Fibonacci–tribonacci–tetranacci triple sum · Two convolution forms of the Fibonacci–tribonacci–tetranacci triple sum · Convolution of four consecutive Fibonacci step sequences · Convolution of an odd number of consecutive Fibonacci step sequences · Triple convolution of Pell numbers with two consecutive Fibonacci step sequences · Pell–Fibonacci–tribonacci triple sum via a Pell–tribonacci convolution · Triple convolution of the Fibonacci 2-, 4- and 5-step numbers · Triple convolution of the Fibonacci 2-, 3- and 5-step numbers · Four-fold convolution of the Fibonacci, tribonacci, tetranacci and pentanacci numbers · Closed form for the Pell–Fibonacci–tribonacci triple convolution · Triple convolution of the tribonacci, tetranacci and pentanacci numbers

TheoremTruncated convolution of the \(m\)-step and \((m+1)\)-step Fibonacci numbers#●ready to prove

Write \(F^{(m)}_n\) for the Fibonacci \(m\)-step numbers (\(F^{(m)}_0 = 0\), \(F^{(m)}_1 = 1\), and each later term is the sum of the \(m\) terms before it, terms at negative indices being \(0\)). For all natural numbers \(m \ge 1\) and \(n \ge m\),

\[\sum_{j=0}^{n-m} F^{(m)}_j F^{(m+1)}_{n-m-j} = F^{(m+1)}_n - F^{(m)}_n.\]
theorem_wanted sum_fibStep_mul_succ (m n : ℕ) (hm : 1 ≤ m)
    (hn : m ≤ n) :
    ∑ j ∈ Finset.range (n - m + 1),
        fibStep m j * fibStep (m + 1) (n - m - j) =
      fibStep (m + 1) n - fibStep m n
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 1.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the Fibonacci and tribonacci numbers#●ready to prove

Write \(F_n\) and \(T_n\) for the Fibonacci and tribonacci numbers, that is, the Fibonacci \(m\)-step numbers \(F^{(m)}_n\) for \(m = 2, 3\) (\(F^{(m)}_0 = 0\), \(F^{(m)}_1 = 1\), and each later term is the sum of the \(m\) terms before it, terms at negative indices being \(0\)). For every natural number \(n\),

\[\sum_{j=0}^{n} F_j T_{n-j} = T_{n+2} - F_{n+2}.\]
theorem_wanted sum_fib_mul_trib (n : ℕ) :
    ∑ j ∈ Finset.range (n + 1), fibStep 2 j * fibStep 3 (n - j) =
      fibStep 3 (n + 2) - fibStep 2 (n + 2)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 2.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the Fibonacci 3-step and 4-step numbers#●ready to prove

Let \(T_j\) and \(Q_j\) be the Fibonacci \(3\)-step and \(4\)-step numbers, where the Fibonacci \(k\)-step numbers start \(0, 1\) and each later term is the sum of the \(k\) terms before it (terms of negative index being \(0\)). For every natural number \(n\),

\[\sum_{j=0}^{n} T_j \, Q_{n-j} = Q_{n+3} - T_{n+3}.\]
theorem_wanted sum_trib_mul_tetra (n : ℕ) :
    ∑ j ∈ Finset.range (n + 1), fibStep 3 j * fibStep 4 (n - j) =
      fibStep 4 (n + 3) - fibStep 3 (n + 3)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 2.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the Fibonacci 4-step and 5-step numbers#●ready to prove

Let \(Q_j\) and \(P_j\) be the Fibonacci \(4\)-step and \(5\)-step numbers, where the Fibonacci \(k\)-step numbers start \(0, 1\) and each later term is the sum of the \(k\) terms before it (terms of negative index being \(0\)). For every natural number \(n\),

\[\sum_{j=0}^{n} Q_j \, P_{n-j} = P_{n+4} - Q_{n+4}.\]
theorem_wanted sum_tetra_mul_penta (n : ℕ) :
    ∑ j ∈ Finset.range (n + 1), fibStep 4 j * fibStep 5 (n - j) =
      fibStep 5 (n + 4) - fibStep 4 (n + 4)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 2.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremIterated convolution of Fibonacci \(m\)-step and \((m+p)\)-step numbers#●ready to prove

Let \(F^{(k)}_j\) be the \(j\)-th Fibonacci \(k\)-step number: the sequence starts \(F^{(k)}_0 = 0\), \(F^{(k)}_1 = 1\), and each later term is the sum of the \(k\) terms before it (terms of negative index being \(0\)). For all natural numbers \(m\), \(p\) and \(n\) with \(m \ge 1\) and \(n \ge m\),

\[\sum_{k=0}^{p-1} \sum_{j=0}^{n-m-k} F^{(m)}_j \, F^{(m+p)}_{n-m-k-j} = F^{(m+p)}_n - F^{(m)}_n,\]

where an inner sum whose upper limit \(n - m - k\) is negative counts as \(0\).

theorem_wanted sum_sum_fibStep_mul (m p n : ℕ) (hm : 1 ≤ m)
    (hn : m ≤ n) :
    ∑ k ∈ Finset.range p, ∑ j ∈ Finset.range (n - m - k + 1),
        fibStep m j * fibStep (m + p) (n - m - k - j) =
      fibStep (m + p) n - fibStep m n
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 3.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the \(m\)-step Fibonacci numbers with consecutive sums of the \((m+2)\)-step ones#●ready to prove

Convolution of the \(m\)-step Fibonacci numbers with consecutive sums of the \((m+2)\)-step ones. Write \(F^{(m)}_n\) for the Fibonacci \(m\)-step numbers (\(F^{(m)}_0 = 0\), \(F^{(m)}_1 = 1\), and each later term is the sum of the \(m\) terms before it, terms at negative indices being \(0\)). For all natural numbers \(m \ge 1\) and \(n \ge m\),

\[\sum_{j=0}^{n-m-1} F^{(m)}_j \bigl(F^{(m+2)}_{n-m-j} + F^{(m+2)}_{n-m-j-1}\bigr) = F^{(m+2)}_n - F^{(m)}_n.\]
theorem_wanted sum_fibStep_mul_add (m n : ℕ) (hm : 1 ≤ m)
    (hn : m ≤ n) :
    ∑ j ∈ Finset.range (n - m), fibStep m j *
        (fibStep (m + 2) (n - m - j) +
          fibStep (m + 2) (n - m - j - 1)) =
      fibStep (m + 2) n - fibStep m n
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 4.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremDouble partial sums of Fibonacci step numbers#●ready to prove

For natural numbers \(p\) and \(n\) with \(1 \le p \le n\), the Fibonacci \((p+1)\)-step numbers \(F^{(p+1)}_j\) satisfy

\[F^{(p+1)}_n - 1 = \sum_{k=0}^{p-1} \sum_{j=0}^{n-2-k} F^{(p+1)}_j,\]

where an inner sum whose upper limit is \(-1\) is empty.

theorem_wanted fibStep_sub_one_eq_sum_sum (p n : ℕ)
    (hp : 1 ≤ p) (hn : p ≤ n) :
    fibStep (p + 1) n - 1 =
      ∑ k ∈ Finset.range p, ∑ j ∈ Finset.range (n - 1 - k),
        fibStep (p + 1) j
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 7.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremPartial sums of the Fibonacci \(m\)-step numbers#●ready to prove

For natural numbers \(m \ge 2\) and \(n\), the Fibonacci \(m\)-step numbers \(F^{(m)}_k\) satisfy

\[(m-1) \sum_{k=0}^{n} F^{(m)}_k = F^{(m)}_{n+m} - \sum_{k=1}^{m-2} (m-1-k) F^{(m)}_{n+k} - 1.\]

The source prints this identity divided by \(m - 1\) and with coefficients \(k\) in place of \(m-1-k\); its proof gives \(m-1-k\), and the printed form already fails at \(m = 4\), \(n = 1\), where it gives \(2/3\) instead of \(1\).

theorem_wanted mul_sum_fibStep (m n : ℕ) (hm : 2 ≤ m) :
    ((m : ℤ) - 1) * ∑ k ∈ Finset.range (n + 1), fibStep m k =
      fibStep m (n + m) -
        ∑ k ∈ Finset.Icc 1 (m - 2),
          ((m - 1 - k : ℕ) : ℤ) * fibStep m (n + k) - 1
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 8.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the Fibonacci and tetranacci numbers#●ready to prove

Write \(F_n\) and \(Q_n\) for the Fibonacci and tetranacci numbers, that is, the Fibonacci \(m\)-step numbers \(F^{(m)}_n\) for \(m = 2, 4\) (\(F^{(m)}_0 = 0\), \(F^{(m)}_1 = 1\), and each later term is the sum of the \(m\) terms before it, terms at negative indices being \(0\)). For every natural number \(n\),

\[\sum_{j=0}^{n} F_j Q_{n-j} = Q_{n+1} + Q_{n-1} - F_{n+1},\]

where for \(n = 0\) the term \(Q_{n-1}\) is \(Q_0 = 0\).

theorem_wanted sum_fib_mul_tetra (n : ℕ) :
    ∑ j ∈ Finset.range (n + 1), fibStep 2 j * fibStep 4 (n - j) =
      fibStep 4 (n + 1) + fibStep 4 (n - 1) - fibStep 2 (n + 1)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollaries 9 and 16.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the Fibonacci and pentanacci numbers#●ready to prove

Write \(F_n\) for the Fibonacci numbers and \(P_n\) for the pentanacci numbers (the Fibonacci \(m\)-step numbers \(F^{(m)}_n\) with \(m = 2\) and \(m = 5\)). For every integer \(n \ge 0\), \(2 \sum_{j=0}^{n} F_j P_{n-j} = P_{n+2} + P_{n-1} - F_{n+2}\), where \(P_{n-1}\) is read as \(P_0 = 0\) when \(n = 0\).

The source prints this identity with a factor \(1/2\); it is stated here multiplied by \(2\).

theorem_wanted two_mul_sum_fib_mul_penta (n : ℕ) :
    2 * ∑ j ∈ Finset.range (n + 1),
        fibStep 2 j * fibStep 5 (n - j) =
      fibStep 5 (n + 2) + fibStep 5 (n - 1) - fibStep 2 (n + 2)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 9.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the pentanacci and tribonacci numbers#●ready to prove

Write \(P_n\) for the pentanacci numbers and \(T_n\) for the tribonacci numbers (the Fibonacci \(m\)-step numbers \(F^{(m)}_n\) with \(m = 5\) and \(m = 3\)). For every integer \(n \ge 0\), \(2 \sum_{j=0}^{n} P_j T_{n-j} = P_{n+3} + P_{n+1} + P_{n-1} - T_{n+3} - T_{n+1}\), where \(P_{n-1}\) is read as \(P_0 = 0\) when \(n = 0\).

The source prints this identity with a factor \(1/2\); it is stated here multiplied by \(2\).

theorem_wanted two_mul_sum_penta_mul_trib (n : ℕ) :
    2 * ∑ j ∈ Finset.range (n + 1),
        fibStep 5 j * fibStep 3 (n - j) =
      fibStep 5 (n + 3) + fibStep 5 (n + 1) + fibStep 5 (n - 1) -
        fibStep 3 (n + 3) - fibStep 3 (n + 1)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 9.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremExchange identity for convolutions of \((m-2)\)-, \((m-1)\)- and \(m\)-step Fibonacci numbers#●ready to prove

Write \(F^{(m)}_n\) for the Fibonacci \(m\)-step numbers (\(F^{(m)}_0 = 0\), \(F^{(m)}_1 = 1\), and each later term is the sum of the \(m\) terms before it, terms at negative indices being \(0\)). For all natural numbers \(m \ge 3\) and \(n \ge 1\),

\[\sum_{j=0}^{n} F^{(m-2)}_j \bigl(F^{(m)}_{n-j} - F^{(m-1)}_{n-j}\bigr) = \sum_{j=0}^{n-1} F^{(m)}_j \bigl(F^{(m-1)}_{n-1-j} - F^{(m-2)}_{n-1-j}\bigr).\]
theorem_wanted sum_fibStep_sub_eq (m n : ℕ) (hm : 3 ≤ m)
    (hn : 1 ≤ n) :
    ∑ j ∈ Finset.range (n + 1), fibStep (m - 2) j *
        (fibStep m (n - j) - fibStep (m - 1) (n - j)) =
      ∑ j ∈ Finset.range n, fibStep m j *
        (fibStep (m - 1) (n - 1 - j) - fibStep (m - 2) (n - 1 - j))
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 10.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremDifference of the Fibonacci 3-step and 2-step numbers as a convolution#●ready to prove

Let \(F_j\) and \(T_j\) be the Fibonacci \(2\)-step and \(3\)-step numbers, where the Fibonacci \(k\)-step numbers start \(0, 1\) and each later term is the sum of the \(k\) terms before it (terms of negative index being \(0\)). For every natural number \(n \ge 1\),

\[T_{n+1} - F_{n+1} = \sum_{j=0}^{n-1} T_j \, F_{n-1-j}.\]
theorem_wanted trib_sub_fib_eq_sum (n : ℕ) (hn : 1 ≤ n) :
    fibStep 3 (n + 1) - fibStep 2 (n + 1) =
      ∑ j ∈ Finset.range n, fibStep 3 j * fibStep 2 (n - 1 - j)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 11.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the Fibonacci numbers with tribonacci minus tetranacci#●ready to prove

Write \(F_n\), \(T_n\) and \(Q_n\) for the Fibonacci, tribonacci and tetranacci numbers, that is, the Fibonacci \(m\)-step numbers \(F^{(m)}_n\) for \(m = 2, 3, 4\) (\(F^{(m)}_0 = 0\), \(F^{(m)}_1 = 1\), and each later term is the sum of the \(m\) terms before it, terms at negative indices being \(0\)). For every natural number \(n \ge 1\),

\[\sum_{j=0}^{n} F_j (T_{n-j} - Q_{n-j}) = \sum_{j=0}^{n-1} (F_j - T_j) Q_{n-1-j}.\]
theorem_wanted sum_fib_mul_sub_eq (n : ℕ) (hn : 1 ≤ n) :
    ∑ j ∈ Finset.range (n + 1), fibStep 2 j *
        (fibStep 3 (n - j) - fibStep 4 (n - j)) =
      ∑ j ∈ Finset.range n,
        (fibStep 2 j - fibStep 3 j) * fibStep 4 (n - 1 - j)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 11.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the Fibonacci 3-step numbers with differences of 4- and 5-step numbers#●ready to prove

Let \(T_j\), \(Q_j\) and \(P_j\) be the Fibonacci \(3\)-, \(4\)- and \(5\)-step numbers, where the Fibonacci \(k\)-step numbers start \(0, 1\) and each later term is the sum of the \(k\) terms before it (terms of negative index being \(0\)). For every natural number \(n \ge 1\),

\[\sum_{j=0}^{n} T_j \bigl(Q_{n-j} - P_{n-j}\bigr) = \sum_{j=0}^{n-1} \bigl(T_j - Q_j\bigr) P_{n-1-j}.\]
theorem_wanted sum_trib_mul_sub_eq (n : ℕ) (hn : 1 ≤ n) :
    ∑ j ∈ Finset.range (n + 1), fibStep 3 j *
        (fibStep 4 (n - j) - fibStep 5 (n - j)) =
      ∑ j ∈ Finset.range n,
        (fibStep 3 j - fibStep 4 j) * fibStep 5 (n - 1 - j)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 11.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the \((m-1)\)-step and \(m\)-step Fibonacci numbers against powers of two#●ready to prove

Write \(F^{(m)}_n\) for the Fibonacci \(m\)-step numbers (\(F^{(m)}_0 = 0\), \(F^{(m)}_1 = 1\), and each later term is the sum of the \(m\) terms before it, terms at negative indices being \(0\)). For all natural numbers \(m \ge 2\) and \(n \ge 2\),

\[\sum_{j=0}^{n} F^{(m-1)}_j F^{(m)}_{n-j} = \sum_{j=0}^{n-2} 2^j \bigl(F^{(m-1)}_{n-1-j} - F^{(m)}_{n-2-j}\bigr).\]
theorem_wanted sum_fibStep_pred_mul (m n : ℕ) (hm : 2 ≤ m)
    (hn : 2 ≤ n) :
    ∑ j ∈ Finset.range (n + 1),
        fibStep (m - 1) j * fibStep m (n - j) =
      ∑ j ∈ Finset.range (n - 1), 2 ^ j *
        (fibStep (m - 1) (n - 1 - j) - fibStep m (n - 2 - j))
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 12.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the Fibonacci 3-step and 4-step numbers as a sum weighted by powers of 2#●ready to prove

Let \(T_j\) and \(Q_j\) be the Fibonacci \(3\)-step and \(4\)-step numbers, where the Fibonacci \(k\)-step numbers start \(0, 1\) and each later term is the sum of the \(k\) terms before it (terms of negative index being \(0\)). For every natural number \(n\),

\[\sum_{j=0}^{n+2} T_j \, Q_{n+2-j} = \sum_{j=0}^{n} 2^j \bigl(T_{n+1-j} - Q_{n-j}\bigr).\]

This is the case \(m = 4\) of the paper's Theorem 12 with \(n\) replaced by \(n + 2\). The paper prints \(Q_{n-j}\) in place of \(Q_{n+2-j}\) on the left; as printed, the identity fails at \(n = 0\), where the left side is \(0\) and the right side is \(1\).

theorem_wanted sum_trib_mul_tetra_eq (n : ℕ) :
    ∑ j ∈ Finset.range (n + 3), fibStep 3 j * fibStep 4 (n + 2 - j) =
      ∑ j ∈ Finset.range (n + 1), 2 ^ j *
        (fibStep 3 (n + 1 - j) - fibStep 4 (n - j))
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 13.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremAlternating sum of differences of \(2m\)-step and \((2m-2)\)-step Fibonacci numbers#●ready to prove

Write \(F^{(m)}_n\) for the Fibonacci \(m\)-step numbers (\(F^{(m)}_0 = 0\), \(F^{(m)}_1 = 1\), and each later term is the sum of the \(m\) terms before it, terms at negative indices being \(0\)). For all natural numbers \(m \ge 2\) and \(n \ge 2m - 1\),

\[\sum_{j=0}^{n-1} (-1)^j \bigl(F^{(2m)}_j - F^{(2m-2)}_j\bigr) = (-1)^{n+1} \sum_{j=0}^{n-2m+1} F^{(2m)}_j F^{(2m-2)}_{n-2m+1-j}.\]
theorem_wanted sum_neg_one_pow_sub_even (m n : ℕ)
    (hm : 2 ≤ m) (hn : 2 * m - 1 ≤ n) :
    ∑ j ∈ Finset.range n, (-1 : ℤ) ^ j *
        (fibStep (2 * m) j - fibStep (2 * m - 2) j) =
      (-1 : ℤ) ^ (n + 1) *
        ∑ j ∈ Finset.range (n - 2 * m + 2),
          fibStep (2 * m) j * fibStep (2 * m - 2) (n - 2 * m + 1 - j)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 15.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremAlternating sums of differences of odd-order Fibonacci step numbers#●ready to prove

Let \(F^{(k)}_j\) be the \(j\)-th Fibonacci \(k\)-step number: the sequence starts \(F^{(k)}_0 = 0\), \(F^{(k)}_1 = 1\), and each later term is the sum of the \(k\) terms before it (terms of negative index being \(0\)). For all natural numbers \(m\) and \(n\) with \(m \ge 1\) and \(n \ge 2m\),

\[\sum_{j=0}^{n-1} (-1)^{j+1} \bigl(F^{(2m+1)}_j - F^{(2m-1)}_j\bigr) = (-1)^n \sum_{j=0}^{n-2m} F^{(2m+1)}_j \, F^{(2m-1)}_{n-2m-j}.\]
theorem_wanted sum_neg_one_pow_sub_odd (m n : ℕ)
    (hm : 1 ≤ m) (hn : 2 * m ≤ n) :
    ∑ j ∈ Finset.range n, (-1 : ℤ) ^ (j + 1) *
        (fibStep (2 * m + 1) j - fibStep (2 * m - 1) j) =
      (-1 : ℤ) ^ n *
        ∑ j ∈ Finset.range (n - 2 * m + 1),
          fibStep (2 * m + 1) j * fibStep (2 * m - 1) (n - 2 * m - j)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 17.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremAlternating sum of the tribonacci numbers#●ready to prove

Write \(T_n\) for the tribonacci numbers (the Fibonacci \(3\)-step numbers \(F^{(3)}_n\)). For every integer \(n \ge 0\), \(2 \sum_{j=0}^{n} (-1)^j T_j = (-1)^n (T_{n+1} - T_{n-1}) - 1\), where \(T_{n-1}\) is read as \(T_0 = 0\) when \(n = 0\).

The source prints this identity with a factor \(1/2\); it is stated here multiplied by \(2\).

theorem_wanted two_mul_sum_neg_one_pow_trib (n : ℕ) :
    2 * ∑ j ∈ Finset.range (n + 1),
        (-1 : ℤ) ^ j * fibStep 3 j =
      (-1 : ℤ) ^ n * (fibStep 3 (n + 1) - fibStep 3 (n - 1)) - 1
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 18.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the pentanacci and tribonacci numbers, second closed form#●ready to prove

Write \(P_n\) for the pentanacci numbers and \(T_n\) for the tribonacci numbers (the Fibonacci \(m\)-step numbers \(F^{(m)}_n\) with \(m = 5\) and \(m = 3\)). For every integer \(n \ge 0\), \(2 \sum_{j=0}^{n} P_j T_{n-j} = -P_{n+7} + 2P_{n+6} - P_{n+5} + 2P_{n+4} + P_{n+3} - T_{n+4} + T_{n+2}\).

The source prints this identity with a factor \(1/2\); it is stated here multiplied by \(2\).

theorem_wanted two_mul_sum_penta_mul_trib' (n : ℕ) :
    2 * ∑ j ∈ Finset.range (n + 1),
        fibStep 5 j * fibStep 3 (n - j) =
      -fibStep 5 (n + 7) + 2 * fibStep 5 (n + 6) -
        fibStep 5 (n + 5) + 2 * fibStep 5 (n + 4) +
        fibStep 5 (n + 3) - fibStep 3 (n + 4) + fibStep 3 (n + 2)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 18.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the \(m\)-step and \((m-2)\)-step Fibonacci numbers via Jacobsthal numbers#●ready to prove

Write \(F^{(m)}_n\) for the Fibonacci \(m\)-step numbers (\(F^{(m)}_0 = 0\), \(F^{(m)}_1 = 1\), and each later term is the sum of the \(m\) terms before it, terms at negative indices being \(0\)), and \(J_n\) for the Jacobsthal numbers (\(J_0 = 0\), \(J_1 = 1\), \(J_{n+2} = J_{n+1} + 2 J_n\)). For all natural numbers \(m \ge 3\) and \(n \ge 2\),

\[\sum_{j=0}^{n} F^{(m)}_j F^{(m-2)}_{n-j} = J_{n-1} + \sum_{j=0}^{n-2} J_j \bigl(F^{(m-2)}_{n-j} - F^{(m)}_{n-2-j}\bigr).\]
theorem_wanted sum_fibStep_mul_sub_two (m n : ℕ) (hm : 3 ≤ m)
    (hn : 2 ≤ n) :
    ∑ j ∈ Finset.range (n + 1),
        fibStep m j * fibStep (m - 2) (n - j) =
      jacobsthalSeq (n - 1) +
        ∑ j ∈ Finset.range (n - 1), jacobsthalSeq j *
          (fibStep (m - 2) (n - j) - fibStep m (n - 2 - j))
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 19.
Uses 2
Statement usesFibonacci \(m\)-step numbers · Jacobsthal numbers

TheoremConvolution of the Jacobsthal and tribonacci numbers#●ready to prove

Write \(J_n\) for the Jacobsthal numbers (\(J_0 = 0\), \(J_1 = 1\), \(J_{n+2} = J_{n+1} + 2J_n\)) and \(T_n\) for the tribonacci numbers (the Fibonacci \(3\)-step numbers \(F^{(3)}_n\)). For every integer \(n \ge 0\), \(2 \sum_{j=0}^{n} J_j T_{n-j} = 2J_{n+1} + J_{n+2} - T_{n+3} - T_{n+1}\).

The source prints this identity with a factor \(1/2\) on part of the right-hand side; it is stated here multiplied by \(2\).

theorem_wanted two_mul_sum_jacobsthal_mul_trib (n : ℕ) :
    2 * ∑ j ∈ Finset.range (n + 1),
        jacobsthalSeq j * fibStep 3 (n - j) =
      2 * jacobsthalSeq (n + 1) + jacobsthalSeq (n + 2) -
        fibStep 3 (n + 3) - fibStep 3 (n + 1)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 20.
Uses 2
Statement usesFibonacci \(m\)-step numbers · Jacobsthal numbers

TheoremTriple convolution of Pell numbers with two consecutive Fibonacci step sequences#●ready to prove

Write \(P_k\) for the Pell numbers (\(P_0 = 0\), \(P_1 = 1\), \(P_{k+2} = 2P_{k+1} + P_k\)), \(F^{(s)}_k\) for the Fibonacci \(s\)-step numbers, and \(\sum_{K(3,N)}\) for a sum over all \((k_1, k_2, k_3) \in \mathbb{N}^3\) with \(k_1 + k_2 + k_3 = N\). For all natural numbers \(m \ge 2\) and \(n \ge 1\),

\[ \sum_{K(3, n - 1)} P_{k_1} F^{(m-1)}_{k_2} F^{(m)}_{k_3} = \sum_{j=0}^{n} F^{(m-1)}_j \left(P_{n-j} - F^{(m)}_{n-j}\right) - \sum_{j=0}^{n-1} P_j F^{(m)}_{n-1-j}. \]
theorem_wanted compProdSum_pell_fibStep (m n : ℕ)
    (hm : 2 ≤ m) (hn : 1 ≤ n) :
    compProdSum
        (fun i k => ![fun t => (MetaMathlibExt.pellNumber t : ℤ),
          fibStep (m - 1), fibStep m] i k) (n - 1) =
      ∑ j ∈ Finset.range (n + 1), fibStep (m - 1) j *
          ((MetaMathlibExt.pellNumber (n - j) : ℤ) -
            fibStep m (n - j)) -
        ∑ j ∈ Finset.range n,
          (MetaMathlibExt.pellNumber j : ℤ) * fibStep m (n - 1 - j)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 21.
Uses 3
Statement usesSums over compositions · Fibonacci \(m\)-step numbers · Pell numbers

TheoremConvolution of the Pell numbers with the Fibonacci numbers#●ready to prove

Let \(\mathcal{P}_j\) be the Pell numbers (\(\mathcal{P}_0 = 0\), \(\mathcal{P}_1 = 1\), \(\mathcal{P}_{j+2} = 2\mathcal{P}_{j+1} + \mathcal{P}_j\)) and \(F_j\) the Fibonacci numbers (\(F_0 = 0\), \(F_1 = 1\), \(F_{j+2} = F_{j+1} + F_j\)), that is, the Fibonacci \(2\)-step numbers. For every natural number \(n\),

\[\sum_{j=0}^{n} \mathcal{P}_j \, F_{n-j} = \mathcal{P}_n - F_n.\]
theorem_wanted sum_pell_mul_fib (n : ℕ) :
    ∑ j ∈ Finset.range (n + 1),
        (MetaMathlibExt.pellNumber j : ℤ) * fibStep 2 (n - j) =
      (MetaMathlibExt.pellNumber n : ℤ) - fibStep 2 n
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 22.
Uses 2
Statement usesFibonacci \(m\)-step numbers · Pell numbers

TheoremPell–Fibonacci–tribonacci triple sum via a Pell–tribonacci convolution#●ready to prove

Write \(P_k\) for the Pell numbers (\(P_0 = 0\), \(P_1 = 1\), \(P_{k+2} = 2P_{k+1} + P_k\)), \(F_k\) and \(T_k\) for the Fibonacci \(2\)- and \(3\)-step numbers, and \(\sum_{K(3,n)}\) for a sum over all \((k_1, k_2, k_3) \in \mathbb{N}^3\) with \(k_1 + k_2 + k_3 = n\). For every natural number \(n\),

\[ \sum_{K(3,n)} P_{k_1} F_{k_2} T_{k_3} = P_{n+1} + F_{n+2} - T_{n+3} - \sum_{j=0}^{n} P_j T_{n-j}. \]
theorem_wanted compProdSum_pell_fib_trib (n : ℕ) :
    compProdSum
        (fun i k => ![fun t => (MetaMathlibExt.pellNumber t : ℤ),
          fibStep 2, fibStep 3] i k) n =
      (MetaMathlibExt.pellNumber (n + 1) : ℤ) + fibStep 2 (n + 2) -
        fibStep 3 (n + 3) -
        ∑ j ∈ Finset.range (n + 1),
          (MetaMathlibExt.pellNumber j : ℤ) * fibStep 3 (n - j)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 23.
Uses 3
Statement usesSums over compositions · Fibonacci \(m\)-step numbers · Pell numbers

TheoremClosed form for the Pell–Fibonacci–tribonacci triple convolution#●ready to prove

Write \(\mathcal{P}_n\) for the Pell numbers, \(F_n\) for the Fibonacci numbers and \(T_n\) for the tribonacci numbers (the Fibonacci \(m\)-step numbers \(F^{(m)}_n\) with \(m = 2\) and \(m = 3\)). For every integer \(n \ge 0\), \(2 \sum \mathcal{P}_{k_1} F_{k_2} T_{k_3} = \mathcal{P}_{n+1} - T_{n+3} - T_{n+2} + 2F_{n+2}\), where the sum runs over all triples \((k_1, k_2, k_3)\) of nonnegative integers with \(k_1 + k_2 + k_3 = n\).

The source prints this identity with a factor \(1/2\); it is stated here multiplied by \(2\).

theorem_wanted two_mul_compProdSum_pell_fib_trib (n : ℕ) :
    2 * compProdSum
        (fun i k => ![fun t => (MetaMathlibExt.pellNumber t : ℤ),
          fibStep 2, fibStep 3] i k) n =
      (MetaMathlibExt.pellNumber (n + 1) : ℤ) - fibStep 3 (n + 3) -
        fibStep 3 (n + 2) + 2 * fibStep 2 (n + 2)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 23.
Uses 3
Statement usesSums over compositions · Fibonacci \(m\)-step numbers · Pell numbers

TheoremA product identity for Fibonacci step generating functions of orders \(m\), \(m+p\), \(m+p+q\)#●ready to prove

A product identity for Fibonacci step generating functions of orders \(m\), \(m+p\), \(m+p+q\). Let \(m, p, q \ge 1\) be natural numbers. For each \(k\), let \(F^{(k)} = \sum_{n \ge 0} F^{(k)}_n X^n\) in \(\mathbb{Q}[[X]]\) be the ordinary generating function of the Fibonacci \(k\)-step numbers \(F^{(k)}_n\). Then

\[X^{2m+p} (1-X^p)(1-X^q) F^{(m)} F^{(m+p)} F^{(m+p+q)} = X^m (1-X)(1-X^p) F^{(m)} F^{(m+p+q)} - (1-X)^2 \left(F^{(m+p)} - F^{(m)}\right).\]
theorem_wanted fibStepGF_triple_identity (m p q : ℕ)
    (hm : 1 ≤ m) (hp : 1 ≤ p) (hq : 1 ≤ q) :
    PowerSeries.X ^ (2 * m + p) *
        (1 - PowerSeries.X ^ p) * (1 - PowerSeries.X ^ q) *
        fibStepGF m * fibStepGF (m + p) * fibStepGF (m + p + q) =
      PowerSeries.X ^ m * (1 - PowerSeries.X) *
          (1 - PowerSeries.X ^ p) * fibStepGF m *
          fibStepGF (m + p + q) -
        (1 - PowerSeries.X) ^ 2 *
          (fibStepGF (m + p) - fibStepGF m)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 24.
Uses 1
Statement usesGenerating function of the Fibonacci \(m\)-step numbers

TheoremA product identity for three consecutive Fibonacci step generating functions#●ready to prove

Let \(m \ge 1\) be a natural number. For each \(k\), let \(F^{(k)} = \sum_{n \ge 0} F^{(k)}_n X^n\) in \(\mathbb{Q}[[X]]\) be the ordinary generating function of the Fibonacci \(k\)-step numbers \(F^{(k)}_n\). Then

\[X^{2m+1} F^{(m)} F^{(m+1)} F^{(m+2)} = X^m F^{(m)} F^{(m+2)} - F^{(m+1)} + F^{(m)}.\]
theorem_wanted fibStepGF_triple_consecutive (m : ℕ)
    (hm : 1 ≤ m) :
    PowerSeries.X ^ (2 * m + 1) * fibStepGF m * fibStepGF (m + 1) *
        fibStepGF (m + 2) =
      PowerSeries.X ^ m * fibStepGF m * fibStepGF (m + 2) -
        fibStepGF (m + 1) + fibStepGF m
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 24.
Uses 1
Statement usesGenerating function of the Fibonacci \(m\)-step numbers

TheoremGenerating-function form of the triple convolution with two consecutive step sequences#●ready to prove

For a natural number \(s\) let \(F^{(s)}(X) = \sum_{n \ge 0} F^{(s)}_n X^n\) be the ordinary generating function, with rational coefficients, of the Fibonacci \(s\)-step numbers \(F^{(s)}_n\). For all natural numbers \(m \ge 1\) and \(p \ge 1\), the formal power series over \(\mathbb{Q}\) satisfy

\[ X^m F^{(m)}(X) F^{(m+1)}(X) F^{(p)}(X) = F^{(p)}(X) F^{(m+1)}(X) - F^{(p)}(X) F^{(m)}(X). \]
theorem_wanted fibStepGF_mixed_triple (m p : ℕ) (hm : 1 ≤ m)
    (hp : 1 ≤ p) :
    PowerSeries.X ^ m * fibStepGF m * fibStepGF (m + 1) *
        fibStepGF p =
      fibStepGF p * fibStepGF (m + 1) - fibStepGF p * fibStepGF m
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 25.
Uses 1
Statement usesGenerating function of the Fibonacci \(m\)-step numbers

TheoremTriple convolution of two consecutive Fibonacci step sequences with a third#●ready to prove

Write \(F^{(s)}_k\) for the Fibonacci \(s\)-step numbers, and write \(\sum_{K(3,N)}\) for a sum over all \((k_1, k_2, k_3) \in \mathbb{N}^3\) with \(k_1 + k_2 + k_3 = N\). For all natural numbers \(m \ge 1\), \(p \ge 1\) and \(n \ge m\),

\[ \sum_{K(3, n - m)} F^{(m)}_{k_1} F^{(m+1)}_{k_2} F^{(p)}_{k_3} = \sum_{j=0}^{n} F^{(p)}_j F^{(m+1)}_{n-j} - \sum_{j=0}^{n} F^{(p)}_j F^{(m)}_{n-j}. \]
theorem_wanted compProdSum_fibStep_triple (m p n : ℕ)
    (hm : 1 ≤ m) (hp : 1 ≤ p) (hn : m ≤ n) :
    compProdSum (fun i k => ![fibStep m, fibStep (m + 1),
        fibStep p] i k) (n - m) =
      ∑ j ∈ Finset.range (n + 1),
          fibStep p j * fibStep (m + 1) (n - j) -
        ∑ j ∈ Finset.range (n + 1),
          fibStep p j * fibStep m (n - j)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 25.
Uses 2
Statement usesSums over compositions · Fibonacci \(m\)-step numbers

TheoremClosed form of the Fibonacci–tribonacci–tetranacci triple sum#●ready to prove

Write \(F_k\), \(T_k\) and \(Q_k\) for the Fibonacci \(2\)-, \(3\)- and \(4\)-step numbers, and write \(\sum_{K(3,n)}\) for a sum over all \((k_1, k_2, k_3) \in \mathbb{N}^3\) with \(k_1 + k_2 + k_3 = n\). For every natural number \(n\),

\[ \sum_{K(3,n)} F_{k_1} T_{k_2} Q_{k_3} = Q_{n+4} + Q_{n+2} - T_{n+5} + F_{n+3}. \]
theorem_wanted compProdSum_fib_trib_tetra (n : ℕ) :
    compProdSum (fun i k => ![fibStep 2, fibStep 3, fibStep 4] i k) n =
      fibStep 4 (n + 4) + fibStep 4 (n + 2) - fibStep 3 (n + 5) +
        fibStep 2 (n + 3)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 26.
Uses 2
Statement usesSums over compositions · Fibonacci \(m\)-step numbers

TheoremTriple convolution of the tribonacci, tetranacci and pentanacci numbers#●ready to prove

Write \(T_n\), \(Q_n\) and \(P_n\) for the Fibonacci \(m\)-step numbers \(F^{(m)}_n\) with \(m = 3, 4, 5\) respectively. For every integer \(n \ge 7\), \(2 \sum T_{k_1} Q_{k_2} P_{k_3} = P_n + P_{n-2} + P_{n-4} + T_n - T_{n-2} - 2Q_n\), where the sum runs over all triples \((k_1, k_2, k_3)\) of nonnegative integers with \(k_1 + k_2 + k_3 = n - 7\).

The source prints this identity with a factor \(1/2\); it is stated here multiplied by \(2\).

theorem_wanted two_mul_compProdSum_trib_tetra_penta (n : ℕ)
    (hn : 7 ≤ n) :
    2 * compProdSum
        (fun i k => ![fibStep 3, fibStep 4, fibStep 5] i k) (n - 7) =
      fibStep 5 n + fibStep 5 (n - 2) + fibStep 5 (n - 4) +
        fibStep 3 n - fibStep 3 (n - 2) - 2 * fibStep 4 n
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 27.
Uses 2
Statement usesSums over compositions · Fibonacci \(m\)-step numbers

TheoremTriple convolution of the Fibonacci 2-, 4- and 5-step numbers#●ready to prove

Let \(F_j\), \(Q_j\) and \(P_j\) be the Fibonacci \(2\)-, \(4\)- and \(5\)-step numbers, where the Fibonacci \(k\)-step numbers start \(0, 1\) and each later term is the sum of the \(k\) terms before it (terms of negative index being \(0\)). For every natural number \(n \ge 5\),

\[2 \sum_{k_1 + k_2 + k_3 = n - 5} F_{k_1} Q_{k_2} P_{k_3} = -2Q_n - 2Q_{n-2} + P_{n+1} + P_{n-2} - F_{n+1} + 2F_n,\]

where the sum runs over all triples \((k_1, k_2, k_3)\) of natural numbers with \(k_1 + k_2 + k_3 = n - 5\).

The paper prints this identity with a factor \(\tfrac{1}{2}\) on part of the right side.

theorem_wanted two_mul_compProdSum_fib_tetra_penta (n : ℕ)
    (hn : 5 ≤ n) :
    2 * compProdSum
        (fun i k => ![fibStep 2, fibStep 4, fibStep 5] i k) (n - 5) =
      -2 * fibStep 4 n - 2 * fibStep 4 (n - 2) +
        fibStep 5 (n + 1) + fibStep 5 (n - 2) - fibStep 2 (n + 1) +
        2 * fibStep 2 n
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 28.
Uses 2
Statement usesSums over compositions · Fibonacci \(m\)-step numbers

TheoremTriple convolution of the Fibonacci 2-, 3- and 5-step numbers#●ready to prove

Let \(F_j\), \(T_j\) and \(P_j\) be the Fibonacci \(2\)-, \(3\)- and \(5\)-step numbers, where the Fibonacci \(k\)-step numbers start \(0, 1\) and each later term is the sum of the \(k\) terms before it (terms of negative index being \(0\)). For every natural number \(n \ge 5\),

\[2 \sum_{k_1 + k_2 + k_3 = n - 5} F_{k_1} T_{k_2} P_{k_3} = P_n - P_{n-1} + P_{n-2} - T_n - T_{n-2} + F_{n-1},\]

where the sum runs over all triples \((k_1, k_2, k_3)\) of natural numbers with \(k_1 + k_2 + k_3 = n - 5\).

The paper prints this identity with a factor \(\tfrac{1}{2}\).

theorem_wanted two_mul_compProdSum_fib_trib_penta (n : ℕ)
    (hn : 5 ≤ n) :
    2 * compProdSum
        (fun i k => ![fibStep 2, fibStep 3, fibStep 5] i k) (n - 5) =
      fibStep 5 n - fibStep 5 (n - 1) + fibStep 5 (n - 2) -
        fibStep 3 n - fibStep 3 (n - 2) + fibStep 2 (n - 1)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 29.
Uses 2
Statement usesSums over compositions · Fibonacci \(m\)-step numbers

TheoremA product identity for four consecutive Fibonacci step generating functions#●ready to prove

Let \(m \ge 1\) be a natural number. For each \(k\), let \(F^{(k)} = \sum_{n \ge 0} F^{(k)}_n X^n\) in \(\mathbb{Q}[[X]]\) be the ordinary generating function of the Fibonacci \(k\)-step numbers \(F^{(k)}_n\). Then

\[X^{2m+1} F^{(m)} F^{(m+1)} F^{(m+2)} F^{(m+3)} = X^m F^{(m)} F^{(m+2)} F^{(m+3)} - F^{(m+1)} F^{(m+3)} + F^{(m)} F^{(m+3)}.\]
theorem_wanted fibStepGF_quadruple_consecutive (m : ℕ)
    (hm : 1 ≤ m) :
    PowerSeries.X ^ (2 * m + 1) * fibStepGF m * fibStepGF (m + 1) *
        fibStepGF (m + 2) * fibStepGF (m + 3) =
      PowerSeries.X ^ m * fibStepGF m * fibStepGF (m + 2) *
          fibStepGF (m + 3) -
        fibStepGF (m + 1) * fibStepGF (m + 3) +
        fibStepGF m * fibStepGF (m + 3)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 31.
Uses 1
Statement usesGenerating function of the Fibonacci \(m\)-step numbers

TheoremFour-fold convolution of the Fibonacci, tribonacci, tetranacci and pentanacci numbers#●ready to prove

Write \(F_n\), \(T_n\), \(Q_n\) and \(P_n\) for the Fibonacci \(m\)-step numbers \(F^{(m)}_n\) with \(m = 2, 3, 4, 5\) respectively. For every integer \(n \ge 5\), \(2 \sum F_{k_1} T_{k_2} Q_{k_3} P_{k_4} = P_{n+4} - P_{n+3} + P_{n+2} + T_{n+3} + T_{n+1} - F_n - 2Q_{n+3} - 2Q_{n+1}\), where the sum runs over all \(4\)-tuples \((k_1, k_2, k_3, k_4)\) of nonnegative integers with \(k_1 + k_2 + k_3 + k_4 = n - 5\).

The source prints this identity with a factor \(1/2\); it is stated here multiplied by \(2\).

theorem_wanted two_mul_compProdSum_four (n : ℕ) (hn : 5 ≤ n) :
    2 * compProdSum (fun i k => ![fibStep 2, fibStep 3,
        fibStep 4, fibStep 5] i k) (n - 5) =
      fibStep 5 (n + 4) - fibStep 5 (n + 3) + fibStep 5 (n + 2) +
        fibStep 3 (n + 3) + fibStep 3 (n + 1) - fibStep 2 n -
        2 * fibStep 4 (n + 3) - 2 * fibStep 4 (n + 1)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 32.
Uses 2
Statement usesSums over compositions · Fibonacci \(m\)-step numbers

TheoremConvolution of four consecutive Fibonacci step sequences#●ready to prove

Write \(F^{(s)}_k\) for the Fibonacci \(s\)-step numbers, and write \(\sum_{K(4,N)}\) for a sum over all \((k_1, k_2, k_3, k_4) \in \mathbb{N}^4\) with \(k_1 + k_2 + k_3 + k_4 = N\). For all natural numbers \(m \ge 1\) and \(n \ge 2m + 2\),

\[ \sum_{K(4, n - 2m - 2)} F^{(m)}_{k_1} F^{(m+1)}_{k_2} F^{(m+2)}_{k_3} F^{(m+3)}_{k_4} = \sum_{j=0}^{n} \left(F^{(m+3)}_j - F^{(m+2)}_j\right) \left(F^{(m+1)}_{n-j} - F^{(m)}_{n-j}\right). \]

The paper prints the index of the last factor on the left as \(k_3\); it is corrected to \(k_4\) here.

theorem_wanted compProdSum_four_consecutive (m n : ℕ)
    (hm : 1 ≤ m) (hn : 2 * m + 2 ≤ n) :
    compProdSum (fun i k => ![fibStep m, fibStep (m + 1),
        fibStep (m + 2), fibStep (m + 3)] i k) (n - 2 * m - 2) =
      ∑ j ∈ Finset.range (n + 1),
        (fibStep (m + 3) j - fibStep (m + 2) j) *
          (fibStep (m + 1) (n - j) - fibStep m (n - j))
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 34.
Uses 2
Statement usesSums over compositions · Fibonacci \(m\)-step numbers

TheoremConvolution of an even number of consecutive Fibonacci step sequences#●ready to prove

Write \(F^{(s)}_k\) for the Fibonacci \(s\)-step numbers, and write \(\sum_{K(r,N)}\) for a sum over all \((k_1, \dots, k_r) \in \mathbb{N}^r\) with \(k_1 + \dots + k_r = N\). For all natural numbers \(\ell \ge 1\), \(m \ge 1\) and \(n \ge \ell(m + \ell - 1)\),

\[ \sum_{K(2\ell, n - \ell(m + \ell - 1))} \prod_{j=0}^{2\ell-1} F^{(m+j)}_{k_{j+1}} = \sum_{K(\ell, n)} \prod_{j=0}^{\ell-1} \left(F^{(m+2j+1)}_{k_{j+1}} - F^{(m+2j)}_{k_{j+1}}\right). \]
theorem_wanted compProdSum_even (l m n : ℕ) (hl : 1 ≤ l)
    (hm : 1 ≤ m) (hn : l * (m + l - 1) ≤ n) :
    @compProdSum (2 * l) (fun (j : Fin (2 * l)) k =>
        fibStep (m + j.val) k) (n - l * (m + l - 1)) =
      @compProdSum l (fun (j : Fin l) k =>
        fibStep (m + 2 * j.val + 1) k - fibStep (m + 2 * j.val) k) n
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 35.
Uses 2
Statement usesSums over compositions · Fibonacci \(m\)-step numbers

TheoremConvolution of an odd number of consecutive Fibonacci step sequences#●ready to prove

Write \(F^{(s)}_k\) for the Fibonacci \(s\)-step numbers, and write \(\sum_{K(r,N)}\) for a sum over all \((k_1, \dots, k_r) \in \mathbb{N}^r\) with \(k_1 + \dots + k_r = N\). For all natural numbers \(\ell \ge 1\), \(m \ge 1\) and \(n \ge \ell(m + \ell - 1)\),

\[ \sum_{K(2\ell+1, n - \ell(m + \ell - 1))} \prod_{j=0}^{2\ell} F^{(m+j)}_{k_{j+1}} = \sum_{K(\ell+1, n)} F^{(m+2\ell)}_{k_{\ell+1}} \prod_{j=0}^{\ell-1} \left(F^{(m+2j+1)}_{k_{j+1}} - F^{(m+2j)}_{k_{j+1}}\right). \]
theorem_wanted compProdSum_odd (l m n : ℕ) (hl : 1 ≤ l)
    (hm : 1 ≤ m) (hn : l * (m + l - 1) ≤ n) :
    @compProdSum (2 * l + 1) (fun (j : Fin (2 * l + 1)) k =>
        fibStep (m + j.val) k) (n - l * (m + l - 1)) =
      @compProdSum (l + 1) (fun (j : Fin (l + 1)) k =>
        if (j.val : ℕ) = l then fibStep (m + 2 * l) k
        else fibStep (m + 2 * j.val + 1) k -
          fibStep (m + 2 * j.val) k) n
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 35.
Uses 2
Statement usesSums over compositions · Fibonacci \(m\)-step numbers

TheoremTwo convolution forms of the Fibonacci–tribonacci–tetranacci triple sum#●ready to prove

Write \(F_k\), \(T_k\) and \(Q_k\) for the Fibonacci \(2\)-, \(3\)- and \(4\)-step numbers, and write \(\sum_{K(3,N)}\) for a sum over all \((k_1, k_2, k_3) \in \mathbb{N}^3\) with \(k_1 + k_2 + k_3 = N\). For every natural number \(n \ge 2\),

\[ \sum_{K(3, n - 2)} F_{k_1} T_{k_2} Q_{k_3} = \sum_{j=0}^{n} (T_j - F_j) Q_{n-j} = \sum_{j=0}^{n+1} F_{n+1-j} (Q_j - T_j). \]
theorem_wanted compProdSum_fib_trib_tetra_eq (n : ℕ)
    (hn : 2 ≤ n) :
    compProdSum (fun i k => ![fibStep 2, fibStep 3, fibStep 4] i k)
          (n - 2) =
        ∑ j ∈ Finset.range (n + 1),
          (fibStep 3 j - fibStep 2 j) * fibStep 4 (n - j) ∧
      compProdSum (fun i k => ![fibStep 2, fibStep 3, fibStep 4] i k)
          (n - 2) =
        ∑ j ∈ Finset.range (n + 2),
          fibStep 2 (n + 1 - j) * (fibStep 4 j - fibStep 3 j)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Corollary 36.
Uses 2
Statement usesSums over compositions · Fibonacci \(m\)-step numbers

TheoremSum of \(2m + 2\) consecutive Fibonacci \(m\)-step numbers#●ready to prove

Write \(F^{(m)}_n\) for the Fibonacci \(m\)-step numbers (\(F^{(m)}_0 = 0\), \(F^{(m)}_1 = 1\), and each later term is the sum of the \(m\) terms before it, terms at negative indices being \(0\)). For every natural number \(m \ge 2\) and every natural number \(n\),

\[\sum_{k=0}^{2m+1} F^{(m)}_{n+k} = 4 F^{(m)}_{n+2m}.\]
theorem_wanted sum_fibStep_window (m n : ℕ) (hm : 2 ≤ m) :
    ∑ k ∈ Finset.range (2 * m + 2), fibStep m (n + k) =
      4 * fibStep m (n + 2 * m)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Lemma 39.
Uses 1
Statement usesFibonacci \(m\)-step numbers

TheoremConvolution of the Fibonacci \(6\)-step numbers with the Fibonacci numbers#●ready to prove

Write \(s_n = F^{(6)}_n\) for the Fibonacci \(6\)-step numbers and \(F_n = F^{(2)}_n\) for the Fibonacci numbers. For every natural number \(n \ge 3\),

\[5 \sum_{j=0}^{n} s_j F_{n-j} = s_{n+3} + s_{n+1} - s_n + 3 s_{n-1} + s_{n-3} - F_{n+3} - F_{n+1}.\]

The source prints this identity divided by \(5\).

theorem_wanted five_mul_sum_fibStep6_mul_fib (n : ℕ)
    (hn : 3 ≤ n) :
    5 * ∑ j ∈ Finset.range (n + 1),
        fibStep 6 j * fibStep 2 (n - j) =
      fibStep 6 (n + 3) + fibStep 6 (n + 1) - fibStep 6 n +
        3 * fibStep 6 (n - 1) + fibStep 6 (n - 3) -
        fibStep 2 (n + 3) - fibStep 2 (n + 1)
Sources
  • Robert Frontczak and Karol Gryszka, "General Convolution Sums Involving Fibonacci m-Step Numbers", Theorem 41.
Uses 1
Statement usesFibonacci \(m\)-step numbers

DefinitionTruncated binomial sum \(G_n^{(k)}\)#✓fully proved

For an integer \(x\) and a natural number \(j\) let \(\binom{x}{j} = x(x-1)\cdots(x-j+1)/j!\). For natural numbers \(k\) and \(n\), the rational number \(G_n^{(k)}\) is

\[ G_n^{(k)} = 2^{n-2} \sum_{\ell=0}^{m} \left(\binom{(k+1)\ell - n}{\ell} - \binom{(k+1)\ell - n}{\ell - 1}\right) 2^{-(k+1)\ell}, \]

where \(m = \lfloor (n-1)/(k+1) \rfloor\) for \(n \ge 1\) and \(m = 0\) for \(n = 0\), and the term \(\binom{(k+1)\ell - n}{\ell - 1}\) is taken to be \(0\) for \(\ell = 0\).

The paper defines \(G_n^{(k)}\) only for \(n, k \ge 2\).

public def kFibonacciBinomialTruncation (k n : ℕ) : ℚ :=
  2 ^ ((n : ℤ) - 2) * ∑ ℓ ∈ Finset.range ((n - 1) / (k + 1) + 1),
    ((Ring.choose (((k + 1) * ℓ : ℕ) - (n : ℤ)) ℓ -
      (if ℓ = 0 then 0 else Ring.choose (((k + 1) * ℓ : ℕ) - (n : ℤ)) (ℓ - 1)) : ℤ) : ℚ) /
      2 ^ ((k + 1) * ℓ)
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, definition before Proposition 10.
Used by 5
Used byInitial values of the truncated binomial sums · Recurrence for the truncated binomial sums · Value \(G_4^{(2)} = 3\) · Value \(G_2^{(2)} = 1\) · \(k\)-Fibonacci numbers as truncated binomial sums

TheoremValue \(G_2^{(2)} = 1\)#✓fully proved

The truncated binomial sum satisfies \(G_2^{(2)} = 1\).

This is the Fibonacci number \(F_2\).

public theorem kFibonacciBinomialTruncation_two_two : kFibonacciBinomialTruncation 2 2 = 1
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, definition before Proposition 10.
Uses 1
Statement usesTruncated binomial sum \(G_n^{(k)}\)

TheoremValue \(G_4^{(2)} = 3\)#✓fully proved

The truncated binomial sum satisfies \(G_4^{(2)} = 3\).

This is the Fibonacci number \(F_4\), and \(n = 4\) is the first index for which the sum defining \(G_n^{(2)}\) has two terms.

public theorem kFibonacciBinomialTruncation_two_four : kFibonacciBinomialTruncation 2 4 = 3
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, definition before Proposition 10.
Uses 1
Statement usesTruncated binomial sum \(G_n^{(k)}\)

TheoremLagrange inversion formula#●ready to prove

Let \(f, g : \mathbb{C} \to \mathbb{C}\) be analytic at \(z_0\). There are \(\varepsilon > 0\) and \(\delta > 0\) such that for every \(\alpha \in \mathbb{C}\) with \(|\alpha| < \delta\) the equation \(w = z_0 + \alpha f(w)\) has exactly one solution \(w\) with \(|w - z_0| < \varepsilon\), and for this solution the series \(\sum_{n \ge 1} \frac{\alpha^n}{n!} \frac{d^{n-1}}{dz^{n-1}} \bigl(f(z)^n g'(z)\bigr)\big|_{z=z_0}\) converges absolutely to \(g(w) - g(z_0)\).

public theorem_wanted lagrange_inversion_formula_analytic (z₀ : ℂ) (f g : ℂ → ℂ)
    (hf : AnalyticAt ℂ f z₀) (hg : AnalyticAt ℂ g z₀) :
    ∃ ε > 0, ∃ δ > 0, ∀ α : ℂ, ‖α‖ < δ →
      (∃! w, w ∈ Metric.ball z₀ ε ∧ w = z₀ + α * f w) ∧
      ∀ w ∈ Metric.ball z₀ ε, w = z₀ + α * f w →
        HasSum (fun m : ℕ => α ^ (m + 1) / ((m + 1).factorial : ℂ) *
            iteratedDeriv m (fun z => f z ^ (m + 1) * deriv g z) z₀)
          (g w - g z₀)
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, Theorem 1 (jis-2024-24.1.1-thm-1).

TheoremBinomial series for the powers of the dominant \(k\)-Fibonacci root#●ready to prove

Let \(k \ge 2\) and let \(\rho_k > 0\) be a real number with \(\rho_k^k = 1 + \rho_k + \dots + \rho_k^{k-1}\). For integers \(a\) and \(j \ge 0\) write \(\binom{a}{j} = a(a-1)\cdots(a-j+1)/j!\). Then for every \(n \ge 1\) the series \(S = \sum_{\ell \ge 0} \frac{1}{\ell+1} \binom{k(\ell+1)+\ell-n}{\ell} 2^{-(k+1)\ell}\) converges absolutely and \(\rho_k^n = 2^n - n\, 2^{n-k-1} S\).

For \(n = 1\) this is the paper's series for \(\rho_k\) itself.

public theorem_wanted kFibonacci_root_pow_eq_binomial_series (k n : ℕ) (hk : 2 ≤ k)
    (hn : 1 ≤ n) (α : ℝ) (hα : 0 < α) (hroot : α ^ k = ∑ i ∈ Finset.range k, α ^ i) :
    ∃ S : ℝ, HasSum (fun ℓ : ℕ => 1 / ((ℓ : ℝ) + 1) *
        ((Ring.choose ((k * (ℓ + 1) + ℓ : ℕ) - (n : ℤ)) ℓ : ℤ) : ℝ) / 2 ^ ((k + 1) * ℓ)) S ∧
      α ^ n = 2 ^ n - n * (2 : ℝ) ^ ((n : ℤ) - k - 1) * S
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, Theorem 3 (jis-2024-24.1.1-thm-3).

TheoremBinomial series for the powers of the golden ratio#●ready to prove

Let \(\varphi = (1 + \sqrt{5})/2\) be the golden ratio, and for an integer \(x\) and a natural number \(j\) let \(\binom{x}{j} = x(x-1)\cdots(x-j+1)/j!\). For every natural number \(n \ge 1\) the series \(S_n = \sum_{\ell \ge 0} \frac{1}{\ell + 1} \binom{3\ell + 2 - n}{\ell} 2^{-3\ell}\) converges absolutely and \(\varphi^n = 2^n - n \, 2^{n-3} S_n\). Moreover, the series \(\sum_{\ell \ge 0} \frac{1}{\ell + 1} \binom{3\ell + 1}{\ell} 2^{-(3\ell + 2)}\) converges absolutely to \(2 - \varphi\).

public theorem_wanted goldenRatio_pow_eq_binomial_series :
    (∀ n : ℕ, 1 ≤ n → ∃ S : ℝ, HasSum (fun ℓ : ℕ => 1 / ((ℓ : ℝ) + 1) *
        ((Ring.choose ((3 * ℓ + 2 : ℕ) - (n : ℤ)) ℓ : ℤ) : ℝ) / 2 ^ (3 * ℓ)) S ∧
      Real.goldenRatio ^ n = 2 ^ n - n * (2 : ℝ) ^ ((n : ℤ) - 3) * S) ∧
    HasSum (fun ℓ : ℕ => 1 / ((ℓ : ℝ) + 1) * ((3 * ℓ + 1).choose ℓ : ℝ) / 2 ^ (3 * ℓ + 2))
      (2 - Real.goldenRatio)
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, Corollary 5 (jis-2024-24.1.1-cor-5).

TheoremBinomial series summed at the \(k\)-Fibonacci root#●ready to prove

Let \(k \ge 2\) be a natural number and \(\rho > 0\) a real number with \(\rho^k = 1 + \rho + \cdots + \rho^{k-1}\), and for an integer \(x\) and a natural number \(j\) let \(\binom{x}{j} = x(x-1)\cdots(x-j+1)/j!\). Then for every integer \(a\) the series below converges absolutely and

\[ \sum_{\ell \ge 0} \binom{(k+1)\ell + a}{\ell} 2^{-(k+1)\ell} = \frac{2^{a+1} \rho^{-a}}{(k+1)\rho - 2k}. \]
public theorem_wanted hasSum_choose_div_two_pow_kFibonacci_root (k : ℕ) (hk : 2 ≤ k) (a : ℤ)
    (α : ℝ) (hα : 0 < α) (hroot : α ^ k = ∑ i ∈ Finset.range k, α ^ i) :
    HasSum (fun ℓ : ℕ => ((Ring.choose (((k + 1) * ℓ : ℕ) + a) ℓ : ℤ) : ℝ) /
        2 ^ ((k + 1) * ℓ))
      ((2 : ℝ) ^ (a + 1) * α ^ (-a) / ((k + 1) * α - 2 * k))
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, Theorem 6 (jis-2024-24.1.1-thm-6).

TheoremDifference binomial series at the \(k\)-Fibonacci root#●ready to prove

Let \(k \ge 2\) be a natural number and \(\rho > 0\) a real number with \(\rho^k = 1 + \rho + \cdots + \rho^{k-1}\), and for an integer \(x\) and a natural number \(j\) let \(\binom{x}{j} = x(x-1)\cdots(x-j+1)/j!\). For every natural number \(n \ne 1\) the series below converges absolutely and

\[ 2^{n-2} \sum_{\ell \ge 0} \left(\binom{(k+1)\ell - n}{\ell} - \binom{(k+1)\ell - n}{\ell - 1}\right) 2^{-(k+1)\ell} = \frac{\rho - 1}{(k+1)\rho - 2k} \rho^{n-1}, \]

where the term \(\binom{(k+1)\ell - n}{\ell - 1}\) is taken to be \(0\) for \(\ell = 0\).

public theorem_wanted hasSum_binomial_series_kFibonacci_asymptotic (k n : ℕ) (hk : 2 ≤ k)
    (hn : n ≠ 1) (α : ℝ) (hα : 0 < α) (hroot : α ^ k = ∑ i ∈ Finset.range k, α ^ i) :
    HasSum (fun ℓ : ℕ => (2 : ℝ) ^ ((n : ℤ) - 2) *
        ((Ring.choose (((k + 1) * ℓ : ℕ) - (n : ℤ)) ℓ -
          (if ℓ = 0 then 0 else Ring.choose (((k + 1) * ℓ : ℕ) - (n : ℤ)) (ℓ - 1)) : ℤ) : ℝ) /
        2 ^ ((k + 1) * ℓ))
      ((α - 1) / ((k + 1) * α - 2 * k) * α ^ ((n : ℤ) - 1))
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, Theorem 8 (jis-2024-24.1.1-thm-8), with As_n^{(k)} from equation (8).

Theorem\(k\)-Fibonacci numbers as truncated binomial sums#●ready to prove

Let \(k \ge 2\) and let \((F_n)_{n \ge 0}\) be the \(k\)-Fibonacci sequence, given by \(F_0 = \dots = F_{k-2} = 0\), \(F_{k-1} = 1\) and \(F_{m+k} = F_m + F_{m+1} + \dots + F_{m+k-1}\) for all \(m \ge 0\). For integers \(a\) and \(j \ge 0\) write \(\binom{a}{j} = a(a-1)\cdots(a-j+1)/j!\), and put \(\binom{a}{-1} = 0\). For \(n \ge 2\) let \(G_n^{(k)}\) be the truncated binomial sum \(G_n^{(k)} = 2^{n-2} \sum_{\ell=0}^{\lfloor (n-1)/(k+1) \rfloor} \left(\binom{(k+1)\ell-n}{\ell} - \binom{(k+1)\ell-n}{\ell-1}\right) 2^{-(k+1)\ell}\). Then \(F_{n+k-2} = G_n^{(k)}\) for every \(n \ge 2\).

public theorem_wanted kFibonacci_eq_kFibonacciBinomialTruncation (k n : ℕ) (hk : 2 ≤ k)
    (hn : 2 ≤ n) (F : ℕ → ℤ) (hF0 : ∀ i < k - 1, F i = 0) (hF1 : F (k - 1) = 1)
    (hrec : ∀ m, F (m + k) = ∑ i ∈ Finset.range k, F (m + i)) :
    (F (n + k - 2) : ℚ) = kFibonacciBinomialTruncation k n
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, Theorem 9 (jis-2024-24.1.1-thm-9).
Uses 1
Statement usesTruncated binomial sum \(G_n^{(k)}\)

TheoremInitial values of the truncated binomial sums#●ready to prove

Let \(k \ge 2\) be a natural number and let \(G_n^{(k)}\) be the truncated binomial sum. Then \(G_n^{(k)} = 2^{n-2}\) for every natural number \(n\) with \(2 \le n \le k + 1\), and \(G_{k+2}^{(k)} = 2^k - 1\).

public theorem_wanted kFibonacciBinomialTruncation_initial_values (k : ℕ) (hk : 2 ≤ k) :
    (∀ n, 2 ≤ n → n ≤ k + 1 → kFibonacciBinomialTruncation k n = 2 ^ (n - 2)) ∧
      kFibonacciBinomialTruncation k (k + 2) = 2 ^ k - 1
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, Proposition 10 (jis-2024-24.1.1-prop-10).
Uses 1
Statement usesTruncated binomial sum \(G_n^{(k)}\)

TheoremRecurrence for the truncated binomial sums#●ready to prove

Let \(G_n^{(k)}\) be the truncated binomial sum. For all natural numbers \(k \ge 2\) and \(n \ge 2\), \(G_{n+k+1}^{(k)} = 2 G_{n+k}^{(k)} - G_n^{(k)}\).

public theorem_wanted kFibonacciBinomialTruncation_recurrence (k n : ℕ) (hk : 2 ≤ k)
    (hn : 2 ≤ n) :
    kFibonacciBinomialTruncation k (n + k + 1) =
      2 * kFibonacciBinomialTruncation k (n + k) - kFibonacciBinomialTruncation k n
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, Proposition 11 (jis-2024-24.1.1-prop-11).
Uses 1
Statement usesTruncated binomial sum \(G_n^{(k)}\)

TheoremBinomial-sum formula for the \(k\)-Fibonacci numbers#●ready to prove

Let \(k \ge 2\) and let \((F_n)_{n \ge 0}\) be the \(k\)-Fibonacci sequence, given by \(F_0 = \dots = F_{k-2} = 0\), \(F_{k-1} = 1\) and \(F_{m+k} = F_m + F_{m+1} + \dots + F_{m+k-1}\) for all \(m \ge 0\). For integers \(a\) and \(j \ge 0\) write \(\binom{a}{j} = a(a-1)\cdots(a-j+1)/j!\), and put \(\binom{a}{-1} = 0\). Then for every \(n \ge k\),

\[F_n = 2^{n-k} \sum_{\ell=0}^{\lfloor (n-k+1)/(k+1) \rfloor} \left(\binom{(k+1)\ell+k-n-2}{\ell} - \binom{(k+1)\ell+k-n-2}{\ell-1}\right) 2^{-(k+1)\ell}.\]
public theorem_wanted kFibonacci_eq_binomial_sum (k n : ℕ) (hk : 2 ≤ k) (hkn : k ≤ n)
    (F : ℕ → ℤ) (hF0 : ∀ i < k - 1, F i = 0) (hF1 : F (k - 1) = 1)
    (hrec : ∀ m, F (m + k) = ∑ i ∈ Finset.range k, F (m + i)) :
    (F n : ℚ) = 2 ^ (n - k) * ∑ ℓ ∈ Finset.range ((n - k + 1) / (k + 1) + 1),
      ((Ring.choose (((k + 1) * ℓ + k : ℕ) - (n : ℤ) - 2) ℓ -
        (if ℓ = 0 then 0 else Ring.choose (((k + 1) * ℓ + k : ℕ) - (n : ℤ) - 2) (ℓ - 1)) :
          ℤ) : ℚ) / 2 ^ ((k + 1) * ℓ)
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, Corollary 12 (jis-2024-24.1.1-cor-12).

TheoremFibonacci numbers as a truncated binomial sum#●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 for an integer \(x\) and a natural number \(j\) let \(\binom{x}{j} = x(x-1)\cdots(x-j+1)/j!\). For every natural number \(n \ge 2\),

\[ F_n = 2^{n-2} \sum_{\ell=0}^{\lfloor (n-1)/3 \rfloor} \left(\binom{3\ell - n}{\ell} - \binom{3\ell - n}{\ell - 1}\right) 2^{-3\ell}, \]

where the term \(\binom{3\ell - n}{\ell - 1}\) is taken to be \(0\) for \(\ell = 0\).

public theorem_wanted fib_eq_binomial_sum (n : ℕ) (hn : 2 ≤ n) :
    (Nat.fib n : ℚ) = 2 ^ (n - 2) * ∑ ℓ ∈ Finset.range ((n - 1) / 3 + 1),
      ((Ring.choose ((3 * ℓ : ℕ) - (n : ℤ)) ℓ -
        (if ℓ = 0 then 0 else Ring.choose ((3 * ℓ : ℕ) - (n : ℤ)) (ℓ - 1)) : ℤ) : ℚ) /
        2 ^ (3 * ℓ)
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, Corollary 13 (jis-2024-24.1.1-cor-13).

TheoremAlternating binomial formula for the \(k\)-Fibonacci numbers#●ready to prove

Let \(k \ge 2\) be a natural number and let \(F_n^{(k)}\) be the \(k\)-Fibonacci numbers: \(F_i^{(k)} = 0\) for \(i < k - 1\), \(F_{k-1}^{(k)} = 1\) and \(F_{m+k}^{(k)} = F_m^{(k)} + F_{m+1}^{(k)} + \cdots + F_{m+k-1}^{(k)}\) for every \(m \ge 0\). For an integer \(x\) and a natural number \(j\) let \(\binom{x}{j} = x(x-1)\cdots(x-j+1)/j!\). Then for every natural number \(n \ge k\),

\[ F_n^{(k)} = 2^{n-k} + \sum_{\ell=1}^{\lfloor (n-k+1)/(k+1) \rfloor} (-1)^\ell \left(\binom{n - (\ell+1)k + 2}{\ell} - \binom{n - (\ell+1)k}{\ell - 2}\right) 2^{n - (k+1)\ell - k}, \]

where the term \(\binom{n - (\ell+1)k}{\ell - 2}\) is taken to be \(0\) for \(\ell = 1\).

The paper assumes \(n \ne 2k - 1\); for \(n = 2k - 1\) the sum is empty and both sides equal \(2^{k-1}\).

public theorem_wanted kFibonacci_eq_alternating_binomial_sum (k n : ℕ) (hk : 2 ≤ k)
    (hkn : k ≤ n) (F : ℕ → ℤ) (hF0 : ∀ i < k - 1, F i = 0) (hF1 : F (k - 1) = 1)
    (hrec : ∀ m, F (m + k) = ∑ i ∈ Finset.range k, F (m + i)) :
    (F n : ℚ) = 2 ^ (n - k) + ∑ ℓ ∈ Finset.Icc 1 ((n - k + 1) / (k + 1)),
      (-1) ^ ℓ * ((Ring.choose ((n : ℤ) - (ℓ + 1) * k + 2) ℓ -
        (if ℓ = 1 then 0 else Ring.choose ((n : ℤ) - (ℓ + 1) * k) (ℓ - 2)) : ℤ) : ℚ) *
        (2 : ℚ) ^ ((n : ℤ) - (k + 1) * ℓ - k)
Sources
  • Bakir Farhi, Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers, Journal of Integer Sequences 27 (2024), Article 24.1.1, Corollary 14 (jis-2024-24.1.1-cor-14).
21 fully proved54 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.