noncomputable def DeltaRegular.deltaCoveringNumber {d : ℕ} (δ : ℝ) (X : Set (EuclideanSpace ℝ (Fin d))) : ℕ∞

The δ-covering number |X|_δ of a set X ⊆ ℝ^d: the minimal number of δ-balls (with centers in the ambient space) needed to cover X.

def DeltaRegular.IsDeltaSRegular {d : ℕ} (δ s C : ℝ) (E : Set (EuclideanSpace ℝ (Fin d))) : Prop

A subset E of the unit ball in ℝ^d is a (δ, s, C)-set if for every ball B(x, r) of radius r ≥ δ, the covering number satisfies |E ∩ B(x, r)|_δ ≤ C r^s |E|_δ. This is the standard discretized notion of an s-dimensional set used throughout discretized projection theory.