Density of orbits of an irrational rotation

Stream: maths

[Yury G. Kudryashov]

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 / ...?

[Mario Carneiro]

fract?

[Yury G. Kudryashov]

fract x = x - floor x

[Mario Carneiro]

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

[Mario Carneiro]

Stupid question: why not take n = 0?

[Mario Carneiro]

or n = -1 for that matter

[Yury G. Kudryashov]

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

[Mario Carneiro]

actually -1 would not work, but 0 would

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Mario Carneiro]

I guess this is usually proven using the pigeonhole principle

[Yury G. Kudryashov]

Yes.

[Reid Barton]

I was about to say exactly the same thing

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

Then I'll add it.