mathlib documentation

data.nat.fib

The Fibonacci Sequence

Summary

Definition of the Fibonacci sequence F₀ = 0, F₁ = 1, Fₙ₊₂ = Fₙ + Fₙ₊₁.

Main Definitions

Main Statements

Implementation Notes

For efficiency purposes, the sequence is defined using stream.iterate.

Tags

fib, fibonacci

def nat.fib (n : ) :

Implementation of the fibonacci sequence satisfying fib 0 = 0, fib 1 = 1, fib (n + 2) = fib n + fib (n + 1).

Note: We use a stream iterator for better performance when compared to the naive recursive implementation.

Equations
@[simp]
theorem nat.fib_zero  :

@[simp]
theorem nat.fib_one  :

@[simp]
theorem nat.fib_two  :

theorem nat.fib_succ_succ {n : } :
nat.fib (n + 2) = nat.fib n + nat.fib (n + 1)

Shows that fib indeed satisfies the Fibonacci recurrence Fₙ₊₂ = Fₙ + Fₙ₊₁.

theorem nat.fib_pos {n : } (n_pos : 0 < n) :

theorem nat.fib_le_fib_succ {n : } :

theorem nat.le_fib_self {n : } (five_le_n : 5 n) :

theorem nat.fib_coprime_fib_succ (n : ) :
(nat.fib n).coprime (nat.fib (n + 1))

Subsequent Fibonacci numbers are coprime, see https://proofwiki.org/wiki/Consecutive_Fibonacci_Numbers_are_Coprime

theorem nat.fib_add (m n : ) :
(nat.fib m) * nat.fib n + (nat.fib (m + 1)) * nat.fib (n + 1) = nat.fib (m + n + 1)

See https://proofwiki.org/wiki/Fibonacci_Number_in_terms_of_Smaller_Fibonacci_Numbers

theorem nat.gcd_fib_add_self (m n : ) :
(nat.fib m).gcd (nat.fib (n + m)) = (nat.fib m).gcd (nat.fib n)

theorem nat.gcd_fib_add_mul_self (m n k : ) :
(nat.fib m).gcd (nat.fib (n + k * m)) = (nat.fib m).gcd (nat.fib n)

theorem nat.fib_gcd (m n : ) :
nat.fib (m.gcd n) = (nat.fib m).gcd (nat.fib n)

fib n is a strong divisibility sequence, see https://proofwiki.org/wiki/GCD_of_Fibonacci_Numbers

theorem nat.fib_dvd (m n : ) (h : m n) :