Commit 2023-09-22 08:17 1d02ef70

View on Github →

feat: Zeckendorf's theorem (#6880) Prove Zeckendorf's theorem: Every natural number can be written uniquely as a sum of distinct non-consecutive Fibonacci numbers. Instead of proving an ExistsUnique statement, I define an equivalence between natural numbers and Zeckendorf representations.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

Modified Mathlib/Data/Nat/Fib.lean

added theorem Nat.fib_add_one

added theorem Nat.fib_eq_zero

added theorem Nat.fib_lt_fib

modified theorem Nat.fib_pos

added theorem Nat.fib_strictMonoOn

added theorem Nat.le_fib_add_one

Created Mathlib/Data/Nat/Fib/Zeckendorf.lean

added theorem List.IsZeckendorfRep.sum_fib_lt

added def List.IsZeckendorfRep

added theorem Nat.fib_greatestFib_le

added def Nat.greatestFib

added theorem Nat.greatestFib_eq_zero

added theorem Nat.greatestFib_fib

added theorem Nat.greatestFib_lt

added theorem Nat.greatestFib_mono

added theorem Nat.greatestFib_ne_zero

added theorem Nat.greatestFib_pos

added theorem Nat.greatestFib_sub_fib_greatestFib_le_greatestFib

added theorem Nat.isZeckendorfRep_zeckendorf

added theorem Nat.le_greatestFib

added theorem Nat.lt_fib_greatestFib_add_one

added theorem Nat.sum_zeckendorf_fib

added def Nat.zeckendorf

added def Nat.zeckendorfEquiv

added theorem Nat.zeckendorf_of_pos

added theorem Nat.zeckendorf_succ

added theorem Nat.zeckendorf_sum_fib

added theorem Nat.zeckendorf_zero

Modified Mathlib/Data/Nat/Order/Basic.lean

added theorem Nat.findGreatest_pos