Horadam and generalized Fibonacci sequences

TheoremGeneralized Catalan identity for Horadam sequences#✓fully proved

Let \(R\) be a commutative ring, let \(c_1, c_2 \in R\), and let \(W, Y, U : \mathbb{N} \to R\) be sequences that each satisfy \(x_{n+2} = c_1 x_{n+1} + c_2 x_n\) for every \(n \in \mathbb{N}\), with \(U_0 = 0\) and \(U_1 = 1\). Then for all \(s, i, j \in \mathbb{N}\),

\[W_{s+i}\,Y_{s+j} - W_s\,Y_{s+i+j} = (-c_2)^s\,(W_1 Y_j - W_0 Y_{j+1})\,U_i.\]

The source states the identity over the integers, with integer coefficients, all integer indices and \(c_2 \ne 0\). This version restricts the indices to natural numbers and allows coefficients in any commutative ring, so no invertibility of \(c_2\) is needed; the bi-infinite version is not claimed.

theorem horadam_generalized_catalan_identity
    {R : Type*} [CommRing R] (c₁ c₂ : R) (W Y U : ℕ → R)
    (hW : ∀ n, W (n + 2) = c₁ * W (n + 1) + c₂ * W n)
    (hY : ∀ n, Y (n + 2) = c₁ * Y (n + 1) + c₂ * Y n)
    (hU : ∀ n, U (n + 2) = c₁ * U (n + 1) + c₂ * U n)
    (hU0 : U 0 = 0) (hU1 : U 1 = 1) (s i j : ℕ) :
    W (s + i) * Y (s + j) - W s * Y (s + i + j) =
      (-c₂) ^ s * (W 1 * Y j - W 0 * Y (j + 1)) * U i
Sources
Used by 1
Used byCassini identity for generalized Fibonacci sequences

TheoremBinet formula for generalized Fibonacci sequences#✓fully proved

Let \(p\) be a real number and let \((W_k)_{k \ge 0}\) be a real sequence with \(W_{k+2} = p W_{k+1} + W_k\) for all \(k \ge 0\). Put \(s = \sqrt{p^2 + 4}\), and let \(\alpha = (p + s)/2\) and \(\beta = (p - s)/2\), the roots of \(z^2 - pz - 1\). Then for every \(n \ge 0\), \(W_n = \frac{W_1 - W_0 \beta}{s} \alpha^n + \frac{W_0 \alpha - W_1}{s} \beta^n\).

theorem generalizedFibonacci_binet (p : ℝ) (W : ℕ → ℝ)
    (hW : ∀ k, W (k + 2) = p * W (k + 1) + W k) (n : ℕ) :
    W n = (W 1 - W 0 * ((p - Real.sqrt (p ^ 2 + 4)) / 2)) / Real.sqrt (p ^ 2 + 4) *
        ((p + Real.sqrt (p ^ 2 + 4)) / 2) ^ n +
      (W 0 * ((p + Real.sqrt (p ^ 2 + 4)) / 2) - W 1) / Real.sqrt (p ^ 2 + 4) *
        ((p - Real.sqrt (p ^ 2 + 4)) / 2) ^ n
Uses 1 · Used by 2
Proof usesBinet formula for second-order linear recurrences
Used byBinet, Cassini, mixed identity and ratio limit for generalized Fibonacci sequences · Ratio limit for generalized Fibonacci sequences

TheoremMixed identity for generalized Fibonacci sequences#✓fully proved

Let \(p\) be a real number and let \(W, F : \mathbb{Z} \to \mathbb{R}\) satisfy \(W_{k+2} = p W_{k+1} + W_k\) and \(F_{k+2} = p F_{k+1} + F_k\) for every integer \(k\), with \(F_0 = 0\) and \(F_1 = 1\). Then for all integers \(m\) and \(n\), \(F_{m-2} W_{n-2} - F_{m-3} W_{n-1} = (-1)^{m-1} W_{n-m+1}\).

theorem generalizedFibonacci_mixed_identity (p : ℝ) (W F : ℤ → ℝ)
    (hWrec : ∀ k : ℤ, W (k + 2) = p * W (k + 1) + W k) (hF0 : F 0 = 0) (hF1 : F 1 = 1)
    (hFrec : ∀ k : ℤ, F (k + 2) = p * F (k + 1) + F k) (m n : ℤ) :
    F (m - 2) * W (n - 2) - F (m - 3) * W (n - 1) = (-1 : ℝ) ^ (m - 1) * W (n - m + 1)
Used by 1
Used byBinet, Cassini, mixed identity and ratio limit for generalized Fibonacci sequences

TheoremCassini identity for generalized Fibonacci sequences#✓fully proved

Let \(R\) be a commutative ring, let \(p \in R\), and let \((W_k)_{k \ge 0}\) be a sequence in \(R\) with \(W_{k+2} = p W_{k+1} + W_k\) for all \(k \ge 0\). Then for every \(n \ge 0\), \(W_n W_{n+2} - W_{n+1}^2 = (-1)^n (W_0^2 + p W_0 W_1 - W_1^2)\).

theorem generalizedFibonacci_cassini {R : Type*} [CommRing R] (p : R) (W : ℕ → R)
    (hW : ∀ k, W (k + 2) = p * W (k + 1) + W k) (n : ℕ) :
    W n * W (n + 2) - W (n + 1) ^ 2 = (-1) ^ n * (W 0 ^ 2 + p * W 0 * W 1 - W 1 ^ 2)
Uses 1 · Used by 1
Proof usesGeneralized Catalan identity for Horadam sequences
Used byBinet, Cassini, mixed identity and ratio limit for generalized Fibonacci sequences

TheoremRatio limit for generalized Fibonacci sequences#✓fully proved

Let \(p > 0\) be a real number and let \((W_k)_{k \ge 0}\) be a real sequence with \(W_0 \ge 0\), \(W_1 > 0\) and \(W_{k+2} = p W_{k+1} + W_k\) for all \(k \ge 0\). Then \(W_{k+1}/W_k\) tends to \((p + \sqrt{p^2 + 4})/2\) as \(k \to \infty\).

theorem generalizedFibonacci_tendsto_ratio (p : ℝ) (hp : 0 < p) (W : ℕ → ℝ) (hW0 : 0 ≤ W 0)
    (hW1 : 0 < W 1) (hW : ∀ k, W (k + 2) = p * W (k + 1) + W k) :
    Filter.Tendsto (fun k => W (k + 1) / W k) Filter.atTop
      (nhds ((p + Real.sqrt (p ^ 2 + 4)) / 2))
Uses 1 · Used by 1
Proof usesBinet formula for generalized Fibonacci sequences
Used byBinet, Cassini, mixed identity and ratio limit for generalized Fibonacci sequences

TheoremBinet, Cassini, mixed identity and ratio limit for generalized Fibonacci sequences#✓fully proved

Let \(p \ge 1\), \(a \ge 0\) and \(b > 0\) be integers, and let \(m \ge 0\) and \(n \ge 0\) be integers. Let \(W, F : \mathbb{Z} \to \mathbb{R}\) satisfy \(W_0 = a\), \(W_1 = b\), \(F_0 = 0\), \(F_1 = 1\), \(W_{k+2} = p W_{k+1} + W_k\) and \(F_{k+2} = p F_{k+1} + F_k\) for every integer \(k\). Put \(s = \sqrt{p^2 + 4}\), \(\alpha = (p + s)/2\) and \(\beta = (p - s)/2\). Then \(W_n = \frac{b - a \beta}{s} \alpha^n + \frac{a \alpha - b}{s} \beta^n\), \(F_{m-2} W_{n-2} - F_{m-3} W_{n-1} = (-1)^{m-1} W_{n-m+1}\), \(W_n W_{n+2} - W_{n+1}^2 = (-1)^n (a^2 + p a b - b^2)\), and \(W_{k+1}/W_k\) tends to \(\alpha\) as \(k \to \infty\) through the natural numbers.

Here \(a^2 + pab - b^2\) is the source's \(\Delta\). The four parts also hold separately under weaker hypotheses; in particular the mixed identity holds for all integers \(m\) and \(n\).

theorem generalizedFibonacci_binet_cassini_and_ratio_limit (p a b : ℤ) (W F : ℤ → ℝ)
  (m n : ℤ) (hp : 1 ≤ p) (ha : 0 ≤ a) (hb : 0 < b) (hm : 0 ≤ m) (hn : 0 ≤ n) (hW0 : W 0 = (a : ℝ))
  (hW1 : W 1 = (b : ℝ)) (hWrec : ∀ k : ℤ, W (k + 2) = (p : ℝ) * W (k + 1) + W k) (hF0 : F 0 = 0)
  (hF1 : F 1 = 1) (hFrec : ∀ k : ℤ, F (k + 2) = (p : ℝ) * F (k + 1) + F k) :
  (W n =
  ((((b : ℝ) - (a : ℝ) * (((p : ℝ) - Real.sqrt ((p : ℝ) ^ 2 + 4)) / 2)) / Real.sqrt
  ((p : ℝ) ^ 2 + 4)) * ((((p : ℝ) + Real.sqrt ((p : ℝ) ^ 2 + 4)) / 2) ^ n) +
  (((a : ℝ) * (((p : ℝ) + Real.sqrt ((p : ℝ) ^ 2 + 4)) / 2) - (b : ℝ)) / Real.sqrt
  ((p : ℝ) ^ 2 + 4)) * ((((p : ℝ) - Real.sqrt ((p : ℝ) ^ 2 + 4)) / 2) ^ n)) ∧ F (m - 2) * W
  (n - 2) - F (m - 3) * W (n - 1) = (-1 : ℝ) ^ (m - 1) * W (n - m + 1) ∧ W n * W (n + 2) - W
  (n + 1) ^ 2 = (-1 : ℝ) ^ n * ((a : ℝ) ^ 2 + (p : ℝ) * (a : ℝ) * (b : ℝ) - (b : ℝ) ^ 2) ∧
  Filter.Tendsto (fun k : ℕ => W (↑k + 1) / W ↑k) Filter.atTop
  (nhds ((((p : ℝ) + Real.sqrt ((p : ℝ) ^ 2 + 4)) / 2))))
Sources
  • Abdelhak Taane, Ihab-Eddine Djellas, and Mohammed Mekkaoui, "Total Positivity of Toeplitz Matrices Involving Generalized Hyper-Fibonacci Numbers," Journal of Integer Sequences 29 (2026), Article 26.2.5, preliminary-results lemma, lines 192–200, https://cs.uwaterloo.ca/journals/JIS/VOL29/Djellas/djellas7.tex
Uses 4
Proof usesBinet formula for generalized Fibonacci sequences · Cassini identity for generalized Fibonacci sequences · Mixed identity for generalized Fibonacci sequences · Ratio limit for generalized Fibonacci sequences
6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.