Decomposition of terms in Lucas sequences

ABDELMADJID BOUDAOUD

We define the Lucas sequences from the paper and verify that the Fibonacci sequence appears.

def U (P Q : ℤ) : ℕ → ℤ

Equations

• U P Q 0 = 0
• U P Q 1 = 1
• U P Q n_2.succ.succ = P * U P Q n_2.succ - Q * U P Q n_2

def V (P Q : ℤ) : ℕ → ℤ

Equations

• V P Q 0 = 2
• V P Q 1 = P
• V P Q n_2.succ.succ = P * V P Q n_2.succ - Q * V P Q n_2

theorem fibonacciLucas : (fun (i : Fin 15) => U 1 (-1) ↑i) = ![0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377]

Fibonacci sequence appearing in Lucas sequence.

def D {P Q : ℤ} : ℤ

Equations

• D = P ^ 2 - 4 * Q