Definition 1.17: ε-net

Fix K ⊂ ℝ^d and ε > 0. A set N is called an ε-net of K with respect to a distance d(·,·) on ℝ^d, if N ⊂ K and for any z ∈ K, there exists x ∈ N such that d(x, z) ≤ ε.

We formalize this for a general pseudo-metric space α, which specializes to ℝ^d when α = EuclideanSpace ℝ (Fin d).

Main definitions

• IsEpsilonNet K N ε: N is an ε-net of K (Definition 1.17).

Relation to Mathlib

Mathlib defines Metric.IsCover ε K N (the covering/net property without the subset requirement) and Metric.coveringNumber ε K (minimum cardinality of an internal ε-cover). Our IsEpsilonNet K N ε is equivalent to N ⊆ K ∧ Metric.IsCover ε K N.

We provide bridge lemmas toIsCover and of_isCover_subset to convert between the two formulations.

References

• Rigollet, High-Dimensional Statistics, Definition 1.17.
• [R. Vershynin, High-Dimensional Probability][vershynin2018high], Section 4.2.

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

A set N is an ε-net of K if N ⊆ K and every point of K is within distance ε of some point in N.

This is Definition 1.17 in Rigollet's High-Dimensional Statistics.

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

The empty set is an ε-net of the empty set.

theorem IsEpsilonNet.self {α : Type u_1} [PseudoMetricSpace α] {ε : ℝ} (K : Set α) (hε : 0 ≤ ε) : IsEpsilonNet K K ε

Every set is an ε-net of itself for any ε ≥ 0.

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

An ε-net is a subset of the original set.

theorem IsEpsilonNet.exists_dist_le {α : Type u_1} [PseudoMetricSpace α] {K N : Set α} {ε : ℝ} (h : IsEpsilonNet K N ε) {z : α} (hz : z ∈ K) : ∃ x ∈ N, dist x z ≤ ε

The covering property of an ε-net: every point of K is within distance ε of some point in N.

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

Monotonicity in ε: an ε-net is also an ε'-net for any ε' ≥ ε.

theorem IsEpsilonNet.anti {α : Type u_1} [PseudoMetricSpace α] {K N : Set α} {ε : ℝ} (h : IsEpsilonNet K N ε) {K' : Set α} (hK' : K' ⊆ K) (hN : N ⊆ K') : IsEpsilonNet K' N ε

An ε-net of K restricts to an ε-net of any subset K' ⊆ K, provided N ⊆ K'.

theorem IsEpsilonNet.mono_net {α : Type u_1} [PseudoMetricSpace α] {K N : Set α} {ε : ℝ} (h : IsEpsilonNet K N ε) {N' : Set α} (hNN' : N ⊆ N') (hN'K : N' ⊆ K) : IsEpsilonNet K N' ε

An ε-net grows with the net set: if N ⊆ N' and N' ⊆ K, then N' is also an ε-net, since the covering by N implies covering by N'.

Bridge to Mathlib's Metric.IsCover

theorem IsEpsilonNet.toIsCover {α : Type u_1} [PseudoMetricSpace α] {K N : Set α} {ε : ℝ} (h : IsEpsilonNet K N ε) (hε : 0 ≤ ε) : Metric.IsCover ⟨ε, hε⟩ K N

An IsEpsilonNet with non-negative ε implies Mathlib's Metric.IsCover.

theorem IsEpsilonNet.of_isCover_subset {α : Type u_1} [PseudoMetricSpace α] {K N : Set α} {ε : ℝ} {ε' : NNReal} (hN : N ⊆ K) (hcov : Metric.IsCover ε' K N) (hε : ↑ε' ≤ ε) : IsEpsilonNet K N ε

Mathlib's Metric.IsCover together with the subset condition gives an IsEpsilonNet.