Zeckendorf's theorem

Stream: maths

[Jakub Kądziołka]

Hi, I'm new to mathlib and I'm somewhat unclear on its scope. Would a proof of Zeckendorf's theorem be a welcome addition?

[Patrick Massot]

Do you have any hint for us about what this theorem is about?

[Yaël Dillies]

It's about writing natural numbers in Fibonacci numbers base.

[Yaël Dillies]

It would definitely be in scope.

[Mario Carneiro]

yeah, let's get phinary numbers

[Yaël Dillies]

Some people were working on it like three months ago. Don't know where they're at.

[Jakub Kądziołka]

Found a proof of the existence part pasted in a previous thread. I'm surprised how long-winded it is, I think I'll try to write a simpler proof myself.

[Adam Topaz]

Let me just casually drop in the following link
https://www.math.leidenuniv.nl/~hwl/papers/fibo.pdf
in case folks want some more ideas for fun formalization projects around Fibonacci numbers.

[Jakub Kądziołka]

So, at what point do I ask for side-branch GitHub access?

[Mario Carneiro]

@Jakub Kądziołka what's your github ID?

[Jakub Kądziołka]

NieDzejkob

[Johan Commelin]

@Jakub Kądziołka https://github.com/leanprover-community/mathlib/invitations

[Jakub Kądziołka]

thanks!

[Jakub Kądziołka]

BTW, is this something that should go in data/nat/fib.lean, or a separate file?

[Johan Commelin]

if you are adding > 200 lines, I would start a new file. If you need heavy imports, also start a new file please. Otherwise, appending it to the existing file is fine.

[Mario Carneiro]

also if the new material is costly in compile time start a new file

[Yaël Dillies]

I would rename data.nat.fib to data.nat.fib.basic and add your stuff to data.nat.fib.zeckendorf

[Jakub Kądziołka]

What would be the best way of defining something like this?

def fib_floor (n : ℕ): ℕ := {k : ℕ | fib k ≤ n}.max

[Yaël Dillies]

Induction probably!

[Jakub Kądziołka]

What would you induct on here? O_o

[Jakub Kądziołka]

I was thinking I could maybe make use of fib_add_two_strict_mono

[Jakub Kądziołka]

oh, perhaps induct on n, case splitting on whether n is in the image

[Jakub Kądziołka]

is there no lemma about a strictly monotone function splitting its codomain into intervals?

[Yaël Dillies]

Maybe you can use docs#nat.find?

[Jakub Kądziołka]

and I'm done. Interestingly I managed to replace a lot of the hairy details of the proof on Wikipedia with a straightforward induction. PR: https://github.com/leanprover-community/mathlib/pull/12443

[Yaël Dillies]

You can type #12443 rather than copying the link :wink:

[Kyle Miller]

Is there a lemma somewhere that a strict monotone function f : ℕ -> ℕ has the property that for all n greater than or equal to f 0 that n lies in a closed-open interval between consecutive images? That could be used to prove this lemma:

lemma fib_between (n : ℕ): ∃ k : ℕ, fib k ≤ n ∧ n < fib k.succ

[Yaël Dillies]

I'm pretty sure we don't have such a lemma, but I agree we should.

[David Wärn]

This is sort of a variant of the adjoint functor theorem. If f : nat -> nat is monotone, unbounded, andf 0 = 0, then f should be the lower adjoint in a Galois connection. I think this fib_between follows from this (use the upper adjoint to find k)

[Jakub Kądziołka]

sounds interesting, do you have any suggestions for a short-ish description of how this works, compatible with a first-year undergrad?

[Patrick Massot]

Jakub, David is using a fancy language but his claim is completely elementary. Do you know about Galois connections?

[Patrick Massot]

docs#galois_connection

[Jakub Kądziołka]

oh, so where's the theorem he's referencing?

[Patrick Massot]

I don't think this is in mathlib yet

[Jakub Kądziołka]

I think I'll prove it just about monotone functions, then. Where would I put it? data.nat.lattice?

[Patrick Massot]

Modulo easy stuff that may be already here, David means:

import data.nat.basic
import data.finset.lattice
import data.set.finite
import order.galois_connection
import order.monotone
import order.filter.at_top_bot
open set
variables {f : ℕ → ℕ} (fmono : strict_mono f) (f0 : f 0 = 0)

lemma nat.finite_of_bdd_above {s : set ℕ} (h : bdd_above s) : finite s :=
begin

  sorry
end

lemma yo (fmono : strict_mono f) (k : ℕ): finite {n | f n ≤ k} :=
begin
  apply nat.finite_of_bdd_above,
sorry,
end

noncomputable
def foo (fmono : strict_mono f)  (k : ℕ): finset ℕ := (yo fmono k).to_finset

@[simp]
lemma mem_foo (fmono : strict_mono f)  (k : ℕ) {n : ℕ} : n ∈ foo fmono k ↔ f n ≤ k :=
by simp [foo]


lemma strict_mono.bar (fmono : strict_mono f) (f0 : f 0 = 0) (k : ℕ) : (foo fmono k).nonempty :=
begin
  use 0,
  rw [mem_foo, f0],
  exact zero_le _
end

/-- Given a strict mono `f : ℕ → ℕ` with `f 0 = 0`, `g k = max {n | f n ≤ k}`.
This is the upper adjoint of a Galois connection having `f` as a lower adjoint, see
`gc` below. -/
noncomputable def g : ℕ → ℕ := λ k, finset.max' _ (fmono.bar f0 k)

lemma g_mem (k) : g fmono f0 k ∈ (foo fmono k) :=
finset.max'_mem (foo fmono k) (fmono.bar f0 k)

lemma gc : galois_connection f (g fmono f0)  :=
λ n k, ⟨λ h, finset.le_max' _ _ ((mem_foo fmono k).mpr h),
        λ h, (fmono.monotone h).trans $ (mem_foo fmono k).mp $ g_mem fmono f0 k⟩

[Patrick Massot]

Of course you would also need proper names. @Jakub Kądziołka