## Stream: maths

### Topic: Density of orbits of an irrational rotation

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

#### Mario Carneiro (Mar 28 2020 at 01:37):

fract?

#### Yury G. Kudryashov (Mar 28 2020 at 01:38):

fract x = x - floor x

#### Mario Carneiro (Mar 28 2020 at 01:38):

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

#### Mario Carneiro (Mar 28 2020 at 01:39):

Stupid question: why not take n = 0?

#### Mario Carneiro (Mar 28 2020 at 01:39):

or n = -1 for that matter

#### Yury G. Kudryashov (Mar 28 2020 at 01:39):

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

#### Mario Carneiro (Mar 28 2020 at 01:40):

actually -1 would not work, but 0 would

#### Yury G. Kudryashov (Mar 28 2020 at 01:40):

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

#### Mario Carneiro (Mar 28 2020 at 01:41):

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

#### Mario Carneiro (Mar 28 2020 at 01:42):

I guess this is usually proven using the pigeonhole principle

Yes.

#### Reid Barton (Mar 28 2020 at 01:42):

I was about to say exactly the same thing

#### 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.

#### 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

#### 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

#### Mario Carneiro (Mar 28 2020 at 01:44):

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