Zulip Chat Archive

Stream: maths

Topic: complementary sequences


view this post on Zulip Johan Commelin (Sep 03 2019 at 20:16):

Suppose I have a strictly monotonous f : nat → nat. How hard is it to define g : nat → nat that is the strictly monotonous sequence of numbers that don't occur in the sequence f...

view this post on Zulip Johan Commelin (Sep 03 2019 at 20:19):

Can we define the Figure Figure sequences? https://en.wikipedia.org/wiki/Hofstadter_sequence#Hofstadter_Figure-Figure_sequences

view this post on Zulip Floris van Doorn (Sep 03 2019 at 20:20):

You need additional assumptions on f, right? You cannot define g when f = id.

view this post on Zulip Chris Hughes (Sep 03 2019 at 20:27):

I constructively proved at some point that every infinite subset of nat was denumerable.

view this post on Zulip Chris Hughes (Sep 03 2019 at 20:28):

It's in mathlib. It was part of the denumerability of Q proof.

view this post on Zulip Floris van Doorn (Sep 03 2019 at 20:29):

The Figure Figure sequences is a bit tricky since it is a mutual definition. I would probably define them mutually, together with R_list which is equal to (list.range n).map R

view this post on Zulip Patrick Massot (Sep 03 2019 at 20:30):

What's the point of this sequence? I skimmed through the wikipedia page without understand why it could be interesting

view this post on Zulip Kevin Buzzard (Sep 03 2019 at 22:40):

Just because it's in the OEIS doesn't mean it's interesting to someone who doesn't care about sequences. The OEIS contains huge collections of uninteresting sequences now, which to be honest is really really good, because whenever someone like me runs into a sequence it's now very likely it will be there. Someone like you is I guess far less likely to be running into sequences of positive integers in your day job.

view this post on Zulip Kevin Buzzard (Sep 03 2019 at 22:43):

"This is the lexicographically earliest sequence that together with its first differences contains every positive integer exactly once". If that floats your boat, then that's the point of the sequence.


Last updated: May 06 2021 at 18:20 UTC