mathlib documentation

data.nat.fib

The Fibonacci Sequence

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

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

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

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 :

0.fib = 0

@[simp]

theorem nat.fib_one :

1.fib = 1

theorem nat.fib_succ_succ {n : ℕ} :

(n + 2).fib = n.fib + (n + 1).fib

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

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

0 < n.fib

theorem nat.fib_le_fib_succ {n : ℕ} :

n.fib ≤ (n + 1).fib

theorem nat.fib_mono {n m : ℕ} (n_le_m : n ≤ m) :

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