Documentation

Mathlib.Data.Nat.Fib.Basic

Fibonacci Numbers #

This file defines the fibonacci series, proves results about it and introduces methods to compute it quickly.

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
Instances For
    @[simp]
    theorem Nat.fib_zero :
    @[simp]
    theorem Nat.fib_one :
    @[simp]
    theorem Nat.fib_two :
    theorem Nat.fib_add_two {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_add_one {n : } :
    n 0Nat.fib (n + 1) = Nat.fib (n - 1) + Nat.fib n
    @[simp]
    theorem Nat.fib_eq_zero {n : } :
    Nat.fib n = 0 n = 0
    @[simp]
    theorem Nat.fib_pos {n : } :
    0 < Nat.fib n 0 < n
    theorem Nat.fib_lt_fib_succ {n : } (hn : 2 n) :
    Nat.fib n < Nat.fib (n + 1)
    theorem Nat.fib_add_two_strictMono :
    StrictMono fun (n : ) => Nat.fib (n + 2)

    fib (n + 2) is strictly monotone.

    theorem Nat.fib_lt_fib {m : } (hm : 2 m) {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_two_mul (n : ) :
    Nat.fib (2 * n) = Nat.fib n * (2 * Nat.fib (n + 1) - Nat.fib n)
    theorem Nat.fib_two_mul_add_one (n : ) :
    Nat.fib (2 * n + 1) = Nat.fib (n + 1) ^ 2 + Nat.fib n ^ 2
    theorem Nat.fib_two_mul_add_two (n : ) :
    Nat.fib (2 * n + 2) = Nat.fib (n + 1) * (2 * Nat.fib n + Nat.fib (n + 1))

    Computes (Nat.fib n, Nat.fib (n + 1)) using the binary representation of n. Supports Nat.fastFib.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Nat.fastFib (n : ) :

      Computes Nat.fib n using the binary representation of n. Proved to be equal to Nat.fib in Nat.fast_fib_eq.

      Equations
      • n.fastFib = n.fastFibAux.1
      Instances For
        theorem Nat.fast_fib_aux_bit_ff (n : ) :
        (Nat.bit false n).fastFibAux = let p := n.fastFibAux; (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)
        theorem Nat.fast_fib_aux_bit_tt (n : ) :
        (Nat.bit true n).fastFibAux = let p := n.fastFibAux; (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
        theorem Nat.fast_fib_aux_eq (n : ) :
        n.fastFibAux = (Nat.fib n, Nat.fib (n + 1))
        theorem Nat.fast_fib_eq (n : ) :
        n.fastFib = Nat.fib n
        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) :
        theorem Nat.fib_succ_eq_sum_choose (n : ) :
        Nat.fib (n + 1) = pFinset.antidiagonal n, p.1.choose p.2
        theorem Nat.fib_succ_eq_succ_sum (n : ) :
        Nat.fib (n + 1) = kFinset.range n, Nat.fib k + 1