Documentation

Marginis.Boudaoud2009

Decomposition of terms in Lucas sequences #

ABDELMADJID BOUDAOUD

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

source
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
Instances For
    source
    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
    Instances For
      source
      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.

      source
      def D {P : ℤ} {Q : ℤ} :
      ℤ
      Equations
      Instances For