English
A finite approximation set distills near-distances between elements of a finite family by subtracting two distinct elements and using an admissible absolute value.
Русский
Конечное приближающее множество уменьшает расстояния между элементами конечной семьи через разности и допустимую норму.
LaTeX
$$zero_notMem ∈ finsetApprox$$
Lean4
/-- If we have a large enough set of elements in `R^ι`, then there will be a pair
whose remainders are close together. We'll show that all sets of cardinality
at least `cardM bS adm` elements satisfy this condition.
The value of `cardM` is not at all optimal: for specific choices of `R`,
the minimum cardinality can be exponentially smaller.
-/
noncomputable def cardM : ℕ :=
adm.card (normBound abv bS ^ (-1 / Fintype.card ι : ℝ)) ^ Fintype.card ι
