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  :

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 : } :
0 < n0 < nat.fib n

theorem nat.fib_le_fib_succ {n : } :

theorem nat.fib_mono {n m : } :
n mnat.fib n nat.fib m

theorem nat.le_fib_self {n : } :
5 nn nat.fib n