Covering and packing numbers

References

• Vershynin, High-Dimensional Probability (section 4.2)

def IsCover {E : Type u_1} [EDist E] (C : Set E) (ε : ENNReal) (A : Set E) : Prop

A set C is an r-cover of another set A if every point in A belongs to a ball with radius r around a point of C.

Equations

• IsCover C ε A = ∀ a ∈ A, ∃ c ∈ C, edist a c ≤ ε

def IsSeparated {E : Type u_1} [EDist E] (C : Set E) (r : ENNReal) : Prop

A set C is a r-separated if all pairs of points a,b of C satisfy r < dist a b.

Equations

• IsSeparated C r = ∀ (a b : E), a ∈ C → b ∈ C → r < edist a b

noncomputable def externalCoveringNumber {E : Type u_1} [EDist E] (r : ENNReal) (A : Set E) : ℕ∞

Equations

• externalCoveringNumber r A = ⨅ (C : Finset E), ⨅ (_ : IsCover (↑C) r A), ↑C.card

noncomputable def internalCoveringNumber {E : Type u_1} [EDist E] (r : ENNReal) (A : Set E) : ℕ∞

Equations

• internalCoveringNumber r A = ⨅ (C : Finset E), ⨅ (_ : ↑C ⊆ A), ⨅ (_ : IsCover (↑C) r A), ↑C.card

noncomputable def packingNumber {E : Type u_1} [EDist E] (r : ENNReal) (A : Set E) : ℕ∞

Equations

• packingNumber r A = ⨆ (C : Finset E), ⨆ (_ : ↑C ⊆ A), ⨆ (_ : IsSeparated (↑C) r), ↑C.card

theorem EMetric.isCover_iff {E : Type u_1} [PseudoEMetricSpace E] {C : Set E} {ε : ENNReal} {A : Set E} : IsCover C ε A ↔ A ⊆ ⋃ x ∈ C, closedBall x ε

@[simp]

theorem isSeparated_empty {E : Type u_1} [EDist E] (r : ENNReal) : IsSeparated ∅ r

theorem subset_iUnion_of_isCover {E : Type u_1} [PseudoEMetricSpace E] {C : Set E} {ε : ENNReal} {A : Set E} (hC : IsCover C ε A) : A ⊆ ⋃ x ∈ C, EMetric.closedBall x ε

theorem TotallyBounded.exists_isCover {E : Type u_1} [PseudoEMetricSpace E] {A : Set E} (hA : TotallyBounded A) (r : ENNReal) (hr : 0 < r) : ∃ (C : Finset E), ↑C ⊆ A ∧ IsCover (↑C) r A

theorem IsCover.Nonempty {E : Type u_1} [PseudoEMetricSpace E] {C : Set E} {ε : ENNReal} {A : Set E} (hC : IsCover C ε A) (hA : A.Nonempty) : C.Nonempty

theorem exists_finset_card_eq_internalCoveringNumber {E : Type u_1} [PseudoEMetricSpace E] {A : Set E} (h : TotallyBounded A) (r : ENNReal) : ∃ (C : Finset E), ↑C ⊆ A ∧ IsCover (↑C) r A ∧ ↑C.card = internalCoveringNumber r A

noncomputable def minimalCover {E : Type u_1} [PseudoEMetricSpace E] (r : ENNReal) (A : Set E) : Finset E

An internal r-cover of A with minimal cardinal.

Equations

• minimalCover r A = if h : TotallyBounded A then ⋯.choose else ∅

theorem minimalCover_subset {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} {A : Set E} : ↑(minimalCover r A) ⊆ A

theorem isCover_minimalCover {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} {A : Set E} (h : TotallyBounded A) : IsCover (↑(minimalCover r A)) r A

theorem card_minimalCover {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} {A : Set E} (h : TotallyBounded A) : ↑(minimalCover r A).card = internalCoveringNumber r A

theorem exists_finset_card_eq_packingNumber {E : Type u_1} {r : ENNReal} {A : Set E} [EDist E] (h : packingNumber r A < ⊤) : ∃ (C : Finset E), ↑C ⊆ A ∧ IsSeparated (↑C) r ∧ ↑C.card = packingNumber r A

noncomputable def maximalSeparatedSet {E : Type u_1} [EDist E] (r : ENNReal) (A : Set E) : Finset E

A maximal r-separated finite subset of A.

Equations

• maximalSeparatedSet r A = if h : packingNumber r A < ⊤ then ⋯.choose else ∅

theorem maximalSeparatedSet_subset {E : Type u_1} {r : ENNReal} {A : Set E} [EDist E] : ↑(maximalSeparatedSet r A) ⊆ A

theorem isSeparated_maximalSeparatedSet {E : Type u_1} {r : ENNReal} {A : Set E} [EDist E] : IsSeparated (↑(maximalSeparatedSet r A)) r

theorem card_maximalSeparatedSet {E : Type u_1} {r : ENNReal} {A : Set E} [EDist E] (h : packingNumber r A < ⊤) : ↑(maximalSeparatedSet r A).card = packingNumber r A

theorem card_le_of_isSeparated {E : Type u_1} {r : ENNReal} {A : Set E} [EDist E] {C : Finset E} (h_subset : ↑C ⊆ A) (h : IsSeparated (↑C) r) : C.card ≤ (maximalSeparatedSet r A).card

theorem isCover_maximalSeparatedSet {E : Type u_1} {r : ENNReal} {A : Set E} [PseudoEMetricSpace E] (h : packingNumber r A < ⊤) : IsCover (↑(maximalSeparatedSet r A)) r A

theorem internalCoveringNumber_le_packingNumber {E : Type u_1} [PseudoEMetricSpace E] (r : ENNReal) (A : Set E) : internalCoveringNumber r A ≤ packingNumber r A

theorem packingNumber_two_le_externalCoveringNumber {E : Type u_1} [EDist E] (r : ENNReal) (A : Set E) : packingNumber (2 * r) A ≤ externalCoveringNumber r A

theorem externalCoveringNumber_le_internalCoveringNumber {E : Type u_1} [EDist E] (r : ENNReal) (A : Set E) : externalCoveringNumber r A ≤ internalCoveringNumber r A

theorem internalCoveringNumber_two_le_externalCoveringNumber {E : Type u_1} [PseudoEMetricSpace E] (r : ENNReal) (A : Set E) : internalCoveringNumber (2 * r) A ≤ externalCoveringNumber r A