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.

Main statements

• externalCoveringNumber_le_coveringNumber: the external covering number is less than or equal to the covering number.
• packingNumber_two_mul_le_externalCoveringNumber: the packing number with radius 2 * ε is less than or equal to the external covering number for ε.

References

• R. Vershynin, High-dimensional probability

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).

Equations

• Metric.externalCoveringNumber ε A = ⨅ (C : Set X), ⨅ (_ : Metric.IsCover ε A C), C.encard

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.

Equations

• Metric.coveringNumber ε A = ⨅ (C : Set X), ⨅ (_ : C ⊆ A), ⨅ (_ : Metric.IsCover ε A C), C.encard

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.

Equations

• Metric.packingNumber ε A = ⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : Metric.IsSeparated (↑ε) C), C.encard

@[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 : EMetric.diam 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 : EMetric.diam A ≤ ↑ε) : externalCoveringNumber ε A = 1

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

theorem Metric.coveringNumber_le_one_of_ediam_le {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (hA : EMetric.diam 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.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 ε.