---

Source: published paper, printed p. 221, Lemma 2.4.

Statement

A finite $1$-separated $K\subset\mathbb R^n$ has, for every $s\ge1$, an $s$-separated subset $K'$ with

$$|K'|\ge |K|/(2s+1)^n.$$

Full proof

Choose a remaining point, put it in $K'$, and remove all remaining points at distance at most $s$ from it. By Lemma 2.2, each step removes at most $(2s+1)^n$ points, including the chosen point. Repeat until none remain. Distinct chosen points have distance greater than $s$, and hence at least $s$. The number of steps is at least $|K|/(2s+1)^n$.

In particular $s=5$ gives a $5$-separated subset with $|K'|\ge11^{-n}|K|$, as needed in the main theorem.

Related proof pages. lemma 2 2.

Bears on. Problem 188.