Documentation

Mathlib.Data.Nat.Fib.Zeckendorf

Zeckendorf's Theorem #

This file proves Zeckendorf's theorem: Every natural number can be written uniquely as a sum of distinct non-consecutive Fibonacci numbers.

Main declarations #

TODO #

We could prove that the order induced by zeckendorfEquiv on Zeckendorf representations is exactly the lexicographic order.

Tags #

fibonacci, zeckendorf, digit

source
theorem instIsTransNatLeHAddOfNat :
IsTrans ℕ fun (a b : ℕ) => b + 2 ≤ a
source
def List.IsZeckendorfRep (l : List ℕ) :
Prop

A list of natural numbers is a Zeckendorf representation (of a natural number) if it is an increasing sequence of non-consecutive numbers greater than or equal to 2.

This is relevant for Zeckendorf's theorem, since if we write a natural n as a sum of Fibonacci numbers (l.map fib).sum, IsZeckendorfRep l exactly means that we can't simplify any expression of the form fib n + fib (n + 1) = fib (n + 2), fib 1 = fib 2 or fib 0 = 0 in the sum.

Equations
Instances For
    source
    @[simp]
    theorem List.IsZeckendorfRep_nil :
    [].IsZeckendorfRep
    source
    theorem List.IsZeckendorfRep.sum_fib_lt {n : ℕ} {l : List ℕ} :
    l.IsZeckendorfRep → (∀ a ∈ (l ++ [0]).head?, a < n) → (map Nat.fib l).sum < Nat.fib n
    source
    def Nat.greatestFib (n : ℕ) :
    ℕ

    The greatest index of a Fibonacci number less than or equal to n.

    Equations
    Instances For
      source
      theorem Nat.fib_greatestFib_le (n : ℕ) :
      fib n.greatestFib ≤ n
      source
      theorem Nat.greatestFib_mono :
      Monotone greatestFib
      source
      @[simp]
      theorem Nat.le_greatestFib {m n : ℕ} :
      m ≤ n.greatestFib ↔ fib m ≤ n
      source
      @[simp]
      theorem Nat.greatestFib_lt {m n : ℕ} :
      m.greatestFib < n ↔ m < fib n
      source
      theorem Nat.lt_fib_greatestFib_add_one (n : ℕ) :
      n < fib (n.greatestFib + 1)
      source
      @[simp]
      theorem Nat.greatestFib_fib {n : ℕ} :
      n ≠ 1 → (fib n).greatestFib = n
      source
      @[simp]
      theorem Nat.greatestFib_eq_zero {n : ℕ} :
      n.greatestFib = 0 ↔ n = 0
      source
      theorem Nat.greatestFib_ne_zero {n : ℕ} :
      n.greatestFib ≠ 0 ↔ n ≠ 0
      source
      @[simp]
      theorem Nat.greatestFib_pos {n : ℕ} :
      0 < n.greatestFib ↔ 0 < n
      source
      theorem Nat.greatestFib_sub_fib_greatestFib_le_greatestFib {n : ℕ} (hn : n ≠ 0) :
      (n - fib n.greatestFib).greatestFib ≤ n.greatestFib - 2
      source
      @[irreducible]
      def Nat.zeckendorf :
      ℕ → List ℕ

      The Zeckendorf representation of a natural number.

      Note: For unfolding, you should use the equational lemmas Nat.zeckendorf_zero and Nat.zeckendorf_of_pos instead of the autogenerated one.

      Equations
      Instances For
        source
        @[simp]
        theorem Nat.zeckendorf_zero :
        zeckendorf 0 = []
        source
        @[simp]
        theorem Nat.zeckendorf_succ (n : ℕ) :
        (n + 1).zeckendorf = (n + 1).greatestFib :: (n + 1 - fib (n + 1).greatestFib).zeckendorf
        source
        @[simp]
        theorem Nat.zeckendorf_of_pos {n : ℕ} :
        0 < n → n.zeckendorf = n.greatestFib :: (n - fib n.greatestFib).zeckendorf
        source
        @[irreducible]
        theorem Nat.isZeckendorfRep_zeckendorf (n : ℕ) :
        n.zeckendorf.IsZeckendorfRep
        source
        theorem Nat.zeckendorf_sum_fib {l : List ℕ} :
        l.IsZeckendorfRep → (List.map fib l).sum.zeckendorf = l
        source
        @[simp]
        theorem Nat.sum_zeckendorf_fib (n : ℕ) :
        (List.map fib n.zeckendorf).sum = n
        source
        def Nat.zeckendorfEquiv :
        ℕ ≃ { l : List ℕ // l.IsZeckendorfRep }

        Zeckendorf's Theorem as an equivalence between natural numbers and Zeckendorf representations. Every natural number can be written uniquely as a sum of non-consecutive Fibonacci numbers (if we forget about the first two terms F₀ = 0, F₁ = 1).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For