# Zulip Chat Archive

## Stream: general

### Topic: Sharkovsky's Theorem

#### Kenny Lau (Mar 28 2019 at 15:03):

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 (Mar 28 2019 at 15:04):

Isn't that just the best theorem?

#### Kevin Buzzard (Mar 28 2019 at 15:04):

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 (Mar 28 2019 at 15:25):

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

#### Agnishom Chattopadhyay (Oct 21 2022 at 17:11):

Is there a lean proof of this yet?

#### Bolton Bailey (Oct 22 2022 at 05:27):

@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 (Oct 22 2022 at 09:31):

@Bhavik Mehta has one somewhere

#### Eric Rodriguez (Oct 22 2022 at 15:14):

(for all cases, btw, not just `n=3`

; he built the proper ordering)

#### Eric Rodriguez (Oct 22 2022 at 15:14):

it seems to be branch#bm-sharkovsky

#### Bhavik Mehta (Oct 22 2022 at 15:33):

Yup, I also did the converse of the theorem

#### Kevin Buzzard (Oct 22 2022 at 16:47):

Did you PR?

#### Bhavik Mehta (Oct 22 2022 at 17:26):

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

#### Yaël Dillies (Oct 22 2022 at 18:21):

Kevin Buzzard said:

Did you PR?

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

#### Agnishom Chattopadhyay (Oct 22 2022 at 23:01):

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 (Oct 22 2022 at 23:03):

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

#### Agnishom Chattopadhyay (Oct 22 2022 at 23:08):

Do we have Desargues Theorem?

#### Eric Rodriguez (Oct 23 2022 at 00:05):

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

#### Junyan Xu (Oct 23 2022 at 02:58):

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

Last updated: Aug 03 2023 at 10:10 UTC