Covering and packing numbers

This file defines covering and packing numbers of a set in a metric space.

For a set s in a metric space and a real number ε > 0:

• the ε-covering number of s is the size of a minimal ε-net of s contained in s.
• the ε-packing number of s is the size of a maximak ε-separated subset of s.

References

High Dimensional Probability, Section 4.2.

Covering number

noncomputable def Metric.ecoveringNum {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (s : Set X) : ℕ∞

The ε-covering number of a set s is the minimum size of an ε-net of s that is also a subset of s. It is equal to ∞ if no such set exists.

If we do not require the net to be a subset of s, then we get a different but essentially equivalent number: the "exterior ε-covering number" of s is at least ecoveringNum (2 * ε) s and at most ecoveringNum ε s.

HDP 4.2.2

Equations

• Metric.ecoveringNum ε s = ⨅ (N : Set X), ⨅ (_ : N ⊆ s), ⨅ (_ : Metric.IsCover ε s N), N.encard

noncomputable def Metric.coveringNum {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (s : Set X) : ℕ

The ε-covering number of a set s is the minimum size of an ε-net of s that is also a subset of s. It is equal to 0 if no such set exists.

If we do not require the net to be a subset of s, then we get a different but essentially equivalent number: the "exterior ε-covering number" of s is at least coveringNum (2 * ε) s and at most coveringNum ε s.

HDP 4.2.2

Equations

• Metric.coveringNum ε s = (Metric.ecoveringNum ε s).toNat

theorem Metric.le_ecoveringNum_iff_forall_le_encard {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s : Set X} {n : ℕ∞} : n ≤ ecoveringNum ε s ↔ ∀ ⦃N : Set X⦄, N ⊆ s → IsCover ε s N → n ≤ N.encard

theorem Metric.le_ecoveringNum_iff_forall_le_card {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s : Set X} {n : ℕ∞} : n ≤ ecoveringNum ε s ↔ ∀ ⦃N : Finset X⦄, ↑N ⊆ s → IsCover ε s ↑N → n ≤ ↑N.card

theorem Metric.IsCover.ecoveringNum_le_encard {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s N : Set X} (hNs : N ⊆ s) (hsN : IsCover ε s N) : ecoveringNum ε s ≤ N.encard

@[simp]

theorem Metric.ecoveringNum_zero {X : Type u_1} [EMetricSpace X] (s : Set X) : ecoveringNum 0 s = s.encard

@[simp]

theorem Metric.coveringNum_zero {X : Type u_1} [EMetricSpace X] (s : Set X) : coveringNum 0 s = s.ncard

@[simp]

theorem Metric.ecoveringNum_lt_top {X : Type u_1} [MetricSpace X] [ProperSpace X] {ε : NNReal} {s : Set X} (hε : ε ≠ 0) : ecoveringNum ε s < ⊤ ↔ IsCompact (closure s)

A set in a proper metric space has finite covering number iff it is relatively compact.

HDP 4.2.3. Note that HDP 4.2.3 incorrectly claims that this holds without the ProperSpace X assumption, but this can't be: If the conclusion holds true, then the closure of a closed ball (ie the closed ball itself) should be compact since it admits a finite net (its center).

theorem Metric.ecoveringNum_ne_top {X : Type u_1} [MetricSpace X] [ProperSpace X] {ε : NNReal} {s : Set X} (hε : ε ≠ 0) : ecoveringNum ε s ≠ ⊤ ↔ IsCompact (closure s)

A set in a proper metric space has finite covering number iff it is relatively compact.

HDP 4.2.3. Note that HDP 4.2.3 incorrectly claims that this holds without the ProperSpace X assumption, but this can't be: If the conclusion holds true, then the closure of a closed ball (ie the closed ball itself) should be compact since it admits a finite net (its center).

@[simp]

theorem Metric.ecoveringNum_eq_top {X : Type u_1} [MetricSpace X] [ProperSpace X] {ε : NNReal} {s : Set X} (hε : ε ≠ 0) : ecoveringNum ε s = ⊤ ↔ ¬IsCompact (closure s)

A set in a proper metric space has infinite covering number iff it is not relatively compact.

HDP 4.2.3. Note that HDP 4.2.3 incorrectly claims that this holds without the ProperSpace X assumption, but this can't be: If the conclusion holds true, then the closure of a closed ball (ie the closed ball itself) should be compact since it admits a finite net (its center).

theorem Metric.ecoveringNum_eq_top_of_not_isCompact_closure {X : Type u_1} [MetricSpace X] [ProperSpace X] {ε : NNReal} {s : Set X} (hs : ¬IsCompact (closure s)) : ecoveringNum ε s = ⊤

A non-relatively compact set in a proper metric space has infinite covering number.

Packing number

noncomputable def Metric.epackingNum {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (s : Set X) : ℕ∞

The ε-packing number of a set s is the maximum size of an ε-separated of s. It is equal to ∞ if no maximal ε-separated set exists.

Equations

• Metric.epackingNum ε s = ⨆ (P : Set X), ⨆ (_ : P ⊆ s), ⨆ (_ : Metric.IsSeparated (↑ε) P), P.encard

theorem Metric.epackingNum_le_iff_forall_encard_le {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s : Set X} {n : ℕ∞} : epackingNum ε s ≤ n ↔ ∀ ⦃P : Set X⦄, P ⊆ s → IsSeparated (↑ε) P → P.encard ≤ n

theorem Metric.epackingNum_le_iff_forall_card_le {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s : Set X} {n : ℕ∞} : epackingNum ε s ≤ n ↔ ∀ ⦃P : Finset X⦄, ↑P ⊆ s → IsSeparated ↑ε ↑P → ↑P.card ≤ n

theorem Metric.IsSeparated.encard_le_epackingNum {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {P s : Set X} (hPs : P ⊆ s) (hP : IsSeparated (↑ε) P) : P.encard ≤ epackingNum ε s

noncomputable def Metric.packingNum {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (s : Set X) : ℕ

The ε-packing number of a set s is the maximum size of an ε-separated of s. It is equal to 0 if no maximal ε-separated set exists.

Equations

• Metric.packingNum ε s = (Metric.epackingNum ε s).toNat

theorem Metric.exists_isSeparated_encard_eq_packingNum {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s : Set X} (hs : epackingNum ε s ≠ ⊤) : ∃ (N : Set X) (_ : N ⊆ s) (_ : IsSeparated (↑ε) N), N.encard = epackingNum ε s

theorem Metric.ecoveringNum_le_epackingNum {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s : Set X} : ecoveringNum ε s ≤ epackingNum ε s

HDP 4.2.8

theorem Metric.epackingNum_two_mul_le_ecoveringNum {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s : Set X} : epackingNum (2 * ε) s ≤ ecoveringNum ε s

HDP 4.2.8

theorem Metric.epackingNum_le_ecoveringNum_div_two {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s : Set X} : epackingNum ε s ≤ ecoveringNum (ε / 2) s