Pigeon hole principle in the real numbers?

Stream: Is there code for X?

[Jovan Gerbscheid]

Is there code that says the following:

(1) For n positive, if a set of points has more than n points inside of an open real interval I of length d, then there is a pair of points in I that are less than d/n appart from eachother.

(2) For n positive, if a set of points has less than n points inside of an open real interval I of length d, then there is an open subinterval of length d/n containing no points of the set.

These can be proved using the pigeon hole principle. (1) is sphere packing in 1 dimension, while (2) is like a sphere not-packing in 1 dimension.

These could also be generalized to higher dimensions, in which case the bound will not be the best possible, but it's a constant factor away from the optimal bound.

[Yaël Dillies]

Something similar was needed for diophantine approximation. @Oliver Nash, do you remember?

[Oliver Nash]

I did do some work on Diophantine approximation a few years ago but it was slightly different. We have results like docs#AddCircle.addWellApproximable_ae_empty_or_univ docs#Real.exists_rat_abs_sub_le_and_den_le but I don't believe we have exactly what Jovan wants.

[Yury G. Kudryashov]

For (1) you can consider the map x ↦ Int.floor (n * x) and take 2 pts that have the same image.

[Yury G. Kudryashov]

For (2), you just need the fact that the semi-open intervals are pairwise disjoint.