Fibonacci numbers extended onto the integers

This file defines the Fibonacci sequence on the integers.

Definition of the sequence: F₀ = 0, F₁ = 1, and Fₙ₊₂ = Fₙ₊₁ + Fₙ (same as the natural number version Nat.fib, but here n is an integer).

def Int.fib (n : ℤ) : ℤ

The Fibonacci sequence for integers. This satisfies fib 0 = 0, fib 1 = 1, fib (n + 2) = fib n + fib (n + 1).

This is an extension of Nat.fib.

Equations

• Int.fib n = if 0 ≤ n then ↑(Nat.fib n.toNat) else if Even n then -↑(Nat.fib (-n).toNat) else ↑(Nat.fib (-n).toNat)

@[simp]

theorem Int.fib_natCast (n : ℕ) : fib ↑n = ↑(Nat.fib n)

@[simp]

theorem Int.fib_zero : fib 0 = 0

@[simp]

theorem Int.fib_one : fib 1 = 1

@[simp]

theorem Int.fib_two : fib 2 = 1

@[simp]

theorem Int.fib_neg_one : fib (-1) = 1

@[simp]

theorem Int.fib_neg_two : fib (-2) = -1

theorem Int.fib_of_nonneg {n : ℤ} (hn : 0 ≤ n) : fib n = ↑(Nat.fib n.toNat)

theorem Int.fib_of_odd {n : ℤ} (hn : Odd n) : fib n = ↑(Nat.fib n.natAbs)

theorem Int.fib_two_mul_add_one_eq_natFib_natAbs {n : ℤ} : fib (2 * n + 1) = ↑(Nat.fib (2 * n + 1).natAbs)

theorem Int.fib_two_mul_add_one_pos {n : ℤ} : 0 < fib (2 * n + 1)

theorem Int.fib_neg_natCast (n : ℕ) : fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)

theorem Int.fib_neg (n : ℤ) : fib (-n) = if Even n then -fib n else fib n

theorem Int.coe_fib_neg (n : ℤ) : ↑(fib (-n)) = (-1) ^ (n + 1) * ↑(fib n)

theorem Int.fib_add_two (n : ℤ) : fib (n + 2) = fib n + fib (n + 1)

theorem Int.fib_eq_fib_add_two_sub_fib_add_one (n : ℤ) : fib n = fib (n + 2) - fib (n + 1)

theorem Int.fib_add_one (n : ℤ) : fib (n + 1) = fib (n + 2) - fib n

@[simp]

theorem Int.fib_eq_zero {n : ℤ} : fib n = 0 ↔ n = 0

theorem Int.fib_add (m n : ℤ) : fib (m + n) = fib (m - 1) * fib n + fib m * fib (n + 1)

theorem Int.fib_two_mul (n : ℤ) : fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)

theorem Int.fib_two_mul_add_one (n : ℤ) : fib (2 * n + 1) = fib (n + 1) ^ 2 + fib n ^ 2

theorem Int.fib_two_mul_add_two (n : ℤ) : fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

theorem Int.gcd_fib (m n : ℤ) : (fib m).gcd (fib n) = Nat.fib (m.gcd n)

theorem Int.fib_dvd (m n : ℤ) (h : m ∣ n) : fib m ∣ fib n