Covering numbers

We define covering numbers of sets in a pseudo-metric space, which are minimal cardinalities of ε-covers of sets by closed balls. We also define the packing number, which is the maximal cardinality of an ε-separated set.

We prove inequalities between these covering and packing numbers.

Main definitions

• externalCoveringNumber: the extenal covering number of a set A for radius ε is the minimal cardinality (in ℕ∞) of an ε-cover.
• coveringNumber: the covering number (or internal covering number) of a set A for radius ε is the minimal cardinality (in ℕ∞) of an ε-cover contained in A.
• packingNumber: the packing number of a set A for radius ε is the maximal cardinality of an ε-separated set in A.

We define sets achieving these minimal/maximal cardinalities when they exist:

• minimalCover: a finite internal ε-cover of a set A by closed balls with minimal cardinality.
• maximalSeparatedSet: a finite ε-separated subset of a set A with maximal cardinality.

Main statements

We have the following inequalities between covering and packing numbers:

• externalCoveringNumber_le_coveringNumber: external covering number ≤ covering number.
• packingNumber_two_mul_le_externalCoveringNumber: packing number for 2 * ε ≤ external covering number for ε.
• coveringNumber_le_packingNumber: covering number ≤ packing number.
• coveringNumber_two_mul_le_externalCoveringNumber: covering number for 2 * ε ≤ external covering number for ε.

The covering number is not monotone for set inclusion (because the cover must be contained in the set), but we have the following inequality:

• coveringNumber_subset_le: if A ⊆ B, then coveringNumber ε A ≤ coveringNumber (ε / 2) B.

References

• [R. Vershynin, High-dimensional probability][vershynin2018high]

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

The external covering number of a set A in X for radius ε is the minimal cardinality (in ℕ∞) of an ε-cover by points in X (not necessarily in A).

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

The covering number (or internal covering number) of a set A for radius ε is the minimal cardinality (in ℕ∞) of an ε-cover contained in A.

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

The packing number of a set A for radius ε is the maximal cardinality (in ℕ∞) of an ε-separated set in A.

@[simp]

theorem Metric.externalCoveringNumber_empty {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) : externalCoveringNumber ε ∅ = 0

@[simp]

theorem Metric.coveringNumber_empty {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) : coveringNumber ε ∅ = 0

@[simp]

theorem Metric.packingNumber_empty {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) : packingNumber ε ∅ = 0

@[simp]

theorem Metric.externalCoveringNumber_eq_zero {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} : externalCoveringNumber ε A = 0 ↔ A = ∅

@[simp]

theorem Metric.externalCoveringNumber_pos_iff {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} : 0 < externalCoveringNumber ε A ↔ A.Nonempty

@[simp]

theorem Metric.coveringNumber_eq_zero {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} : coveringNumber ε A = 0 ↔ A = ∅

@[simp]

theorem Metric.coveringNumber_pos_iff {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} : 0 < coveringNumber ε A ↔ A.Nonempty

@[simp]

theorem Metric.packingNumber_eq_zero {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} : packingNumber ε A = 0 ↔ A = ∅

@[simp]

theorem Metric.packingNumber_pos_iff {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} : 0 < packingNumber ε A ↔ A.Nonempty

theorem Metric.externalCoveringNumber_le_coveringNumber {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (A : Set X) : externalCoveringNumber ε A ≤ coveringNumber ε A

theorem Metric.IsCover.externalCoveringNumber_le_encard {X : Type u_1} [PseudoEMetricSpace X] {A C : Set X} {ε : NNReal} (hC : IsCover ε A C) : externalCoveringNumber ε A ≤ C.encard

theorem Metric.IsCover.coveringNumber_le_encard {X : Type u_1} [PseudoEMetricSpace X] {A C : Set X} {ε : NNReal} (h_subset : C ⊆ A) (hC : IsCover ε A C) : coveringNumber ε A ≤ C.encard

theorem Metric.IsSeparated.encard_le_packingNumber {X : Type u_1} [PseudoEMetricSpace X] {A C : Set X} {ε : NNReal} (h_subset : C ⊆ A) (hC : IsSeparated (↑ε) C) : C.encard ≤ packingNumber ε A

theorem Metric.externalCoveringNumber_le_encard_self {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} (A : Set X) : externalCoveringNumber ε A ≤ A.encard

theorem Metric.coveringNumber_le_encard_self {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} (A : Set X) : coveringNumber ε A ≤ A.encard

theorem Metric.packingNumber_le_encard_self {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} (A : Set X) : packingNumber ε A ≤ A.encard

theorem Metric.externalCoveringNumber_anti {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε δ : NNReal} (h : ε ≤ δ) : externalCoveringNumber δ A ≤ externalCoveringNumber ε A

theorem Metric.coveringNumber_anti {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε δ : NNReal} (h : ε ≤ δ) : coveringNumber δ A ≤ coveringNumber ε A

theorem Metric.externalCoveringNumber_mono_set {X : Type u_1} [PseudoEMetricSpace X] {A B : Set X} {ε : NNReal} (h : A ⊆ B) : externalCoveringNumber ε A ≤ externalCoveringNumber ε B

@[simp]

theorem Metric.externalCoveringNumber_zero {E : Type u_2} [EMetricSpace E] (A : Set E) : externalCoveringNumber 0 A = A.encard

@[simp]

theorem Metric.coveringNumber_zero {E : Type u_2} [EMetricSpace E] (A : Set E) : coveringNumber 0 A = A.encard

@[simp]

theorem Metric.packingNumber_zero {E : Type u_2} [EMetricSpace E] (A : Set E) : packingNumber 0 A = A.encard

theorem Metric.coveringNumber_eq_one_of_ediam_le {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (h_nonempty : A.Nonempty) (hA : ediam A ≤ ↑ε) : coveringNumber ε A = 1

theorem Metric.externalCoveringNumber_eq_one_of_ediam_le {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (h_nonempty : A.Nonempty) (hA : ediam A ≤ ↑ε) : externalCoveringNumber ε A = 1

theorem Metric.externalCoveringNumber_le_one_of_ediam_le {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (hA : ediam A ≤ ↑ε) : externalCoveringNumber ε A ≤ 1

theorem Metric.coveringNumber_le_one_of_ediam_le {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (hA : ediam A ≤ ↑ε) : coveringNumber ε A ≤ 1

@[simp]

theorem Metric.coveringNumber_singleton {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (x : X) : coveringNumber ε {x} = 1

@[simp]

theorem Metric.externalCoveringNumber_singleton {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (x : X) : externalCoveringNumber ε {x} = 1

@[simp]

theorem Metric.packingNumber_singleton {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (x : X) : packingNumber ε {x} = 1

theorem Metric.exists_set_encard_eq_coveringNumber {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (h : coveringNumber ε A ≠ ⊤) : ∃ C ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A

noncomputable def Metric.minimalCover {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (A : Set X) : Set X

A finite internal ε-cover of a set A by closed balls with minimal cardinality. It is defined as the empty set if no such finite cover exists.

theorem Metric.minimalCover_subset {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} : minimalCover ε A ⊆ A

theorem Metric.finite_minimalCover {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} : (minimalCover ε A).Finite

theorem Metric.isCover_minimalCover {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (h : coveringNumber ε A ≠ ⊤) : IsCover ε A (minimalCover ε A)

theorem Metric.encard_minimalCover {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (h : coveringNumber ε A ≠ ⊤) : (minimalCover ε A).encard = coveringNumber ε A

theorem Metric.exists_set_encard_eq_packingNumber {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (h : packingNumber ε A ≠ ⊤) : ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = packingNumber ε A

noncomputable def Metric.maximalSeparatedSet {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (A : Set X) : Set X

A finite ε-separated subset of a set A with maximal cardinality. It is defined as the empty set if no such finite subset exists.

theorem Metric.maximalSeparatedSet_subset {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} : maximalSeparatedSet ε A ⊆ A

theorem Metric.isSeparated_maximalSeparatedSet {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} : IsSeparated (↑ε) (maximalSeparatedSet ε A)

theorem Metric.encard_maximalSeparatedSet {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (h : packingNumber ε A ≠ ⊤) : (maximalSeparatedSet ε A).encard = packingNumber ε A

theorem Metric.encard_le_of_isSeparated {X : Type u_1} [PseudoEMetricSpace X] {A C : Set X} {ε : NNReal} (h_subset : C ⊆ A) (h_sep : IsSeparated (↑ε) C) (h : packingNumber ε A ≠ ⊤) : C.encard ≤ (maximalSeparatedSet ε A).encard

theorem Metric.isCover_maximalSeparatedSet {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (h : packingNumber ε A ≠ ⊤) : IsCover ε A (maximalSeparatedSet ε A)

The maximal separated set is a cover.

theorem Metric.packingNumber_two_mul_le_externalCoveringNumber {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (A : Set X) : packingNumber (2 * ε) A ≤ externalCoveringNumber ε A

The packing number of a set A for radius 2 * ε is at most the external covering number of A for radius ε.

theorem Metric.coveringNumber_le_packingNumber {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (A : Set X) : coveringNumber ε A ≤ packingNumber ε A

theorem Metric.coveringNumber_two_mul_le_externalCoveringNumber {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (A : Set X) : coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A

theorem Metric.coveringNumber_subset_le {X : Type u_1} [PseudoEMetricSpace X] {A B : Set X} {ε : NNReal} (h : A ⊆ B) : coveringNumber ε A ≤ coveringNumber (ε / 2) B