Counting points of a discrete additive subgroup

This file gives a uniform bound on the number of points of a discrete additive subgroup in a set of bounded diameter. Translating one point of the intersection to the origin embeds the intersection into a closed ball of the same radius.

Main results

• AddSubgroup.finite_inter: a discrete additive subgroup meets a bounded set in a finite set.
• AddSubgroup.ncard_inter_le_ncard_closedBall_inter: a set of diameter at most r carries at most as many points of a discrete additive subgroup as the closed ball of radius r centred at the origin.

theorem AddSubgroup.finite_inter {E : Type u_1} [NormedAddCommGroup E] [ProperSpace E] (L : AddSubgroup E) [DiscreteTopology ↥L] {s : Set E} (hs : Bornology.IsBounded s) : (s ∩ ↑L).Finite

A discrete additive subgroup meets a bounded set in a finite set: it is closed and discrete, and the bounded set is contained in its compact closure.

theorem AddSubgroup.ncard_inter_le_ncard_closedBall_inter {E : Type u_1} [NormedAddCommGroup E] [ProperSpace E] (L : AddSubgroup E) [DiscreteTopology ↥L] {s : Set E} {r : ℝ} (hs : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ r) : (s ∩ ↑L).ncard ≤ (Metric.closedBall 0 r ∩ ↑L).ncard

A set whose points are pairwise at distance at most r carries at most as many points of a discrete subgroup as the closed ball of radius r centred at the origin does. Translating a point of the intersection to the origin is what makes the bound uniform over all such sets.