Problem 1.7: Covering and packing number inequality

Informal statement (Rigollet, Problem 1.7): For any K ⊂ ℝ^d, distance d on ℝ^d, and ε > 0:

• The ε-covering number C(ε) of K is the cardinality of the smallest ε-net of K.
• The ε-packing number P(ε) of K is the cardinality of the largest set 𝒫 ⊂ K such that d(z, z') > ε for all z, z' ∈ 𝒫, z ≠ z'.

Show that: C(2ε) ≤ P(2ε) ≤ C(ε).

Key ideas for both inequalities:

• C(2ε) ≤ P(2ε): Any maximal 2ε-separated (packing) set is automatically a 2ε-net (cover). If some point of K were farther than 2ε from all packing points, we could add it to the packing, contradicting maximality. So the minimum cover size C(2ε) ≤ size of any maximal packing ≤ P(2ε).
• P(2ε) ≤ C(ε): Given any ε-net N, map each point of a 2ε-separated set to its nearest point in N. By the triangle inequality, this map is injective (two points at distance > 2ε cannot both be within ε of the same net point). So P(2ε) ≤ |N|, and minimizing over N gives P(2ε) ≤ C(ε).

Formalization approach

We generalize from ℝ^d to any PseudoEMetricSpace. The covering and packing numbers are defined using Mathlib's Metric.coveringNumber and Metric.packingNumber. The proof follows directly from Mathlib lemmas:

• Metric.coveringNumber_le_packingNumber for the first inequality
• Metric.packingNumber_two_mul_le_externalCoveringNumber composed with Metric.externalCoveringNumber_le_coveringNumber for the second

References

• Rigollet, High-Dimensional Statistics, Problem 1.7.

ε-separated subsets

def IsEpsilonSeparated {α : Type u_1} [PseudoMetricSpace α] (K S : Set α) (ε : ℝ) : Prop

A set S is ε-separated within K if S ⊆ K and any two distinct points of S have distance strictly greater than ε. This is the companion notion to IsEpsilonNet for packing.

theorem IsEpsilonSeparated.subset_set {α : Type u_1} [PseudoMetricSpace α] {K S : Set α} {ε : ℝ} (h : IsEpsilonSeparated K S ε) : S ⊆ K

An ε-separated set is a subset of the ambient set.

theorem IsEpsilonSeparated.dist_gt {α : Type u_1} [PseudoMetricSpace α] {K S : Set α} {ε : ℝ} (h : IsEpsilonSeparated K S ε) {z z' : α} (hz : z ∈ S) (hz' : z' ∈ S) (hne : z ≠ z') : dist z z' > ε

The separation property: distinct points have distance > ε.

theorem IsEpsilonSeparated.empty {α : Type u_1} [PseudoMetricSpace α] (K : Set α) (ε : ℝ) : IsEpsilonSeparated K ∅ ε

The empty set is ε-separated in any set.

theorem IsEpsilonSeparated.mono_eps {α : Type u_1} [PseudoMetricSpace α] {K S : Set α} {ε : ℝ} (h : IsEpsilonSeparated K S ε) {ε' : ℝ} (hle : ε' ≤ ε) : IsEpsilonSeparated K S ε'

Monotonicity: an ε-separated set is ε'-separated for any ε' ≤ ε.

Covering and packing numbers

noncomputable def epsilonCoveringNumber {α : Type u_1} [PseudoEMetricSpace α] (ε : NNReal) (K : Set α) : ℕ∞

The ε-covering number of K is the minimum cardinality of an ε-net of K (an internal ε-cover, i.e., a subset N ⊆ K that ε-covers K).

This is Metric.coveringNumber from Mathlib, which computes ⨅ (C ⊆ K) (_ : IsCover ε K C), C.encard.

noncomputable def epsilonPackingNumber {α : Type u_1} [PseudoEMetricSpace α] (ε : NNReal) (K : Set α) : ℕ∞

The ε-packing number of K is the maximum cardinality of an ε-separated subset of K.

This is Metric.packingNumber from Mathlib, which computes ⨆ (S ⊆ K) (_ : IsSeparated ε S), S.encard.

Problem 1.7: The covering–packing inequality

theorem problem_1_7_covering_packing {α : Type u_1} (x✝ : PseudoEMetricSpace α) (K : Set α) (ε : NNReal) : epsilonCoveringNumber (2 * ε) K ≤ epsilonPackingNumber (2 * ε) K ∧ epsilonPackingNumber (2 * ε) K ≤ epsilonCoveringNumber ε K

Problem 1.7 (Covering–packing inequality). For any set K in a pseudo-extended-metric space and ε : ℝ≥0:

C(2ε) ≤ P(2ε) ≤ C(ε)

where C(ε) = epsilonCoveringNumber ε K is the ε-covering number and P(ε) = epsilonPackingNumber ε K is the ε-packing number.

The first inequality C(2ε) ≤ P(2ε) holds because any maximal (2ε)-separated subset is a (2ε)-net (by maximality, every point of K is within distance 2ε of some point in the set).

The second inequality P(2ε) ≤ C(ε) holds because given any ε-net N, the map sending each point of a (2ε)-separated set to its nearest point in N is injective (by the triangle inequality, two distinct points in the separated set cannot map to the same net point).