Sharkovsky's Theorem

Stream: general

[Kenny Lau]

http://mathworld.wolfram.com/SharkovskysTheorem.html

Order the natural numbers as such: 3<5<7<9<11<13<....<6<10<14<18<22<26<....<12<20<28<36<44<52<...<8<4<2<1
Now let p<q. If f:R->R is continuous and there is a point of least period p then there is a point of least period q.

(period here referring to f(f(f(...f(x)...))))

[Kevin Buzzard]

Isn't that just the best theorem?

[Kevin Buzzard]

For me what is most remarkable about it is that any result of that nature should even be true. If there is a point of period 3 then there is a point of period n for all n?? Really? Yes!

[Sebastien Gouezel]

The proof is not even hard. Just needs the intermediate value theorem, and a careful study of overlaps of intervals.

[Agnishom Chattopadhyay]

Is there a lean proof of this yet?

[Bolton Bailey]

@Agnishom Chattopadhyay I don't think so. The case for n=3 isn't that hard and would make for a nice short project for someone.

[Eric Rodriguez]

@Bhavik Mehta has one somewhere

[Eric Rodriguez]

(for all cases, btw, not just n=3; he built the proper ordering)

[Eric Rodriguez]

it seems to be branch#bm-sharkovsky

[Bhavik Mehta]

Yup, I also did the converse of the theorem

[Kevin Buzzard]

Did you PR?

[Bhavik Mehta]

Not yet, but as usual I've been slowly making prerequisite PRs

[Yaël Dillies]

Kevin Buzzard said:

Did you PR?

The correct question is "Did Yaël PR it?" :rofl:

[Agnishom Chattopadhyay]

That's pretty cool. I learnt about this yesterday from https://kpknudson.com/my-favorite-theorem/2022/10/20/episode-80-kimberley-ayers

[Julian Berman]

Great podcast :) (I wondered awhile ago how many of the favorite theorems from it we have, probably a decent number)

[Agnishom Chattopadhyay]

Do we have Desargues Theorem?

[Eric Rodriguez]

no, but a couple of theorem provers do: https://www.cs.ru.nl/~freek/100/#87

[Junyan Xu]

People over at this thread are interested in axiomatic projective geometry.