Lemma 1.18: Covering number of the unit Euclidean ball

Fix ε ∈ (0,1). Then the unit Euclidean ball B₂ in ℝ^d has an ε-net N with |N| ≤ (3/ε)^d.

Proof outline (volume/packing argument)

1. Use Zorn's lemma to get a maximal ε-separated subset N of closedBall 0 1.
2. By maximality, N is an ε-net (every point is within distance ε of some point in N).
3. The ε/2-balls around the points of N are pairwise disjoint and contained in closedBall 0 (1 + ε/2).
4. Volume comparison gives |N| · (ε/2)^d ≤ (1 + ε/2)^d, hence |N| ≤ (3/ε)^d.

References

• Rigollet, High-Dimensional Statistics, Lemma 1.18.

Helper: ε-separated subsets of compact sets are finite

theorem separated_finite_of_compact {X : Type u_1} [PseudoMetricSpace X] {K : Set X} (hK : IsCompact K) {ε : ℝ} (hε : 0 < ε) {S : Set X} (hSK : S ⊆ K) (hSep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → ε < dist x y) : S.Finite

In a compact set, any ε-separated subset (pairwise distances > ε) is finite. This follows by pigeonhole: each ε/2-ball in a finite cover contains at most one element.

Helper: Zorn gives a maximal ε-separated ε-net

theorem exists_maximal_separated_net {X : Type u_1} [PseudoMetricSpace X] (K : Set X) (ε : ℝ) (hε : 0 < ε) : ∃ N ⊆ K, (∀ x ∈ N, ∀ y ∈ N, x ≠ y → ε < dist x y) ∧ ∀ z ∈ K, ∃ x ∈ N, dist x z ≤ ε

By Zorn's lemma, any set K contains a maximal ε-separated subset, which is automatically an ε-net: if some z ∈ K were farther than ε from all points in N, then N ∪ {z} would still be ε-separated, contradicting maximality.

Volume bound on ε-separated sets (packing bound)

theorem packing_card_le_real {d : ℕ} (ε : ℝ) (hε0 : 0 < ε) (hε1 : ε ≤ 1) (S : Finset (EuclideanSpace ℝ (Fin d))) (hS_sub : ↑S ⊆ Metric.closedBall 0 1) (hS_sep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → ε < dist x y) : ↑S.card ≤ (3 / ε) ^ d

Any ε-separated finite subset S of the unit ball in ℝ^d satisfies |S| ≤ (3/ε)^d. This follows from a volume comparison argument:

• The ε/2-balls around S-points are pairwise disjoint,
• Each is contained in B(0, 1 + ε/2),
• So |S| · vol(B(0, ε/2)) ≤ vol(B(0, 1 + ε/2)),
• Since vol(B(0, r)) = r^d · vol(B(0,1)), we get |S| ≤ ((2+ε)/ε)^d ≤ (3/ε)^d.

Main theorem

theorem lemma_1_18_covering_number_euclidean_ball {d : ℕ} (hd : 0 < d) (ε : ℝ) (hε_pos : 0 < ε) (hε_lt : ε < 1) : ∃ (N : Finset (EuclideanSpace ℝ (Fin d))), IsEpsilonNet (Metric.closedBall 0 1) (↑N) ε ∧ N.card ≤ ⌈(3 / ε) ^ d⌉₊

Lemma 1.18 (Rigollet). Fix ε ∈ (0,1). The unit Euclidean ball B₂ in ℝ^d has an ε-net N with |N| ≤ ⌈(3/ε)^d⌉.

The proof constructs a maximal ε-separated subset of the ball via Zorn's lemma. By maximality, this subset is an ε-net. The cardinality bound follows from the volume comparison argument in packing_card_le_real.