Zulip Chat Archive

Stream: maths

Topic: Density of orbits of an irrational rotation


view this post on Zulip Yury G. Kudryashov (Mar 28 2020 at 01:37):

I have an impression that I saw a lemma like this one formalized somewhere:

example {x : } (hx : irrational x) {ε : } (ε0 : 0 < ε) :  n : , fract (n * x) < ε :=

Do we have it somewhere in mathlib or this is a false memory / something I saw in Coq / ...?

view this post on Zulip Mario Carneiro (Mar 28 2020 at 01:37):

fract?

view this post on Zulip Yury G. Kudryashov (Mar 28 2020 at 01:38):

fract x = x - floor x

view this post on Zulip Mario Carneiro (Mar 28 2020 at 01:38):

I don't think that function exists, so probably the theorem doesn't either

view this post on Zulip Mario Carneiro (Mar 28 2020 at 01:39):

Stupid question: why not take n = 0?

view this post on Zulip Mario Carneiro (Mar 28 2020 at 01:39):

or n = -1 for that matter

view this post on Zulip Yury G. Kudryashov (Mar 28 2020 at 01:39):

https://github.com/leanprover-community/mathlib/blob/master/src/algebra/floor.lean#L116

view this post on Zulip Mario Carneiro (Mar 28 2020 at 01:40):

actually -1 would not work, but 0 would

view this post on Zulip Yury G. Kudryashov (Mar 28 2020 at 01:40):

Shame on me, it should be ∃ n ≠ 0.

view this post on Zulip Mario Carneiro (Mar 28 2020 at 01:41):

I suspect there is some easy proof using that the rationals are dense

view this post on Zulip Mario Carneiro (Mar 28 2020 at 01:42):

I guess this is usually proven using the pigeonhole principle

view this post on Zulip Yury G. Kudryashov (Mar 28 2020 at 01:42):

Yes.

view this post on Zulip Reid Barton (Mar 28 2020 at 01:42):

I was about to say exactly the same thing

view this post on Zulip Yury G. Kudryashov (Mar 28 2020 at 01:42):

I know how to prove it. Just didn't want to redo something that is already in the library.

view this post on Zulip Mario Carneiro (Mar 28 2020 at 01:42):

I don't know of any proof in mathlib for this, but my info might be out of date

view this post on Zulip Mario Carneiro (Mar 28 2020 at 01:43):

actually, if you look at all the uses of irrational, it's not a long list and this theorem isn't in it

view this post on Zulip Mario Carneiro (Mar 28 2020 at 01:44):

we don't have much of this kind of number theory

view this post on Zulip Yury G. Kudryashov (Mar 28 2020 at 01:45):

Then I'll add it.


Last updated: May 09 2021 at 10:11 UTC