Covering and packing numbers

References

• Vershynin, High-Dimensional Probability (section 4.2)

def IsCover {α : Type u_1} [Dist α] (C : Set α) (r : ℝ) (A : Set α) : 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 r A = ∀ a ∈ A, ∃ c ∈ C, dist a c ≤ r

def IsSeparated {α : Type u_1} [Dist α] (C : Set α) (r : ℝ) : 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 : α), a ∈ C → b ∈ C → r < dist a b

@[simp]

theorem isSeparated_empty {α : Type u_1} [Dist α] (r : ℝ) : IsSeparated ∅ r

noncomputable def externalCoveringNumber {α : Type u_1} [Dist α] (r : ℝ) (A : Set α) : ℕ∞

Equations

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

noncomputable def internalCoveringNumber {α : Type u_1} [Dist α] (r : ℝ) (A : Set α) : ℕ∞

Equations

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

noncomputable def packingNumber {α : Type u_1} [Dist α] (r : ℝ) (A : Set α) : ℕ∞

Equations

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

theorem exists_finset_card_eq_internalCoveringNumber {α : Type u_1} {r : ℝ} {A : Set α} [Dist α] (h : internalCoveringNumber r A < ⊤) : ∃ (C : Finset α), ↑C ⊆ A ∧ IsCover (↑C) r A ∧ ↑C.card = internalCoveringNumber r A

noncomputable def minimalCover {α : Type u_1} [Dist α] (r : ℝ) (A : Set α) : Finset α

An internal r-cover of A with minimal cardinal.

Equations

• minimalCover r A = if h : internalCoveringNumber r A < ⊤ then ⋯.choose else ∅

theorem minimalCover_subset {α : Type u_1} {r : ℝ} {A : Set α} [Dist α] : ↑(minimalCover r A) ⊆ A

theorem isCover_minimalCover {α : Type u_1} {r : ℝ} {A : Set α} [Dist α] (h : internalCoveringNumber r A < ⊤) : IsCover (↑(minimalCover r A)) r A

theorem card_minimalCover {α : Type u_1} {r : ℝ} {A : Set α} [Dist α] (h : internalCoveringNumber r A < ⊤) : ↑(minimalCover r A).card = internalCoveringNumber r A

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

noncomputable def maximalSeparatedSet {α : Type u_1} [Dist α] (r : ℝ) (A : Set α) : Finset α

A maximal r-separated finite subset of A.

Equations

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

theorem maximalSeparatedSet_subset {α : Type u_1} {r : ℝ} {A : Set α} [Dist α] : ↑(maximalSeparatedSet r A) ⊆ A

theorem isSeparated_maximalSeparatedSet {α : Type u_1} {r : ℝ} {A : Set α} [Dist α] : IsSeparated (↑(maximalSeparatedSet r A)) r

theorem card_maximalSeparatedSet {α : Type u_1} {r : ℝ} {A : Set α} [Dist α] (h : packingNumber r A < ⊤) : ↑(maximalSeparatedSet r A).card = packingNumber r A

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

theorem isCover_maximalSeparatedSet {α : Type u_1} {r : ℝ} {A : Set α} [PseudoMetricSpace α] (h : packingNumber r A < ⊤) (hr : 0 ≤ r) : IsCover (↑(maximalSeparatedSet r A)) r A

theorem internalCoveringNumber_le_packingNumber {α : Type u_1} [PseudoMetricSpace α] (r : ℝ) (A : Set α) (hr : 0 ≤ r) : internalCoveringNumber r A ≤ packingNumber r A

theorem packingNumber_two_le_externalCoveringNumber {α : Type u_1} [Dist α] (r : ℝ) (A : Set α) : packingNumber (2 * r) A ≤ externalCoveringNumber r A

theorem externalCoveringNumber_le_internalCoveringNumber {α : Type u_1} [Dist α] (r : ℝ) (A : Set α) : externalCoveringNumber r A ≤ internalCoveringNumber r A

theorem internalCoveringNumber_two_le_externalCoveringNumber {α : Type u_1} [PseudoMetricSpace α] (r : ℝ) (A : Set α) (hr : 0 ≤ r) : internalCoveringNumber (2 * r) A ≤ externalCoveringNumber r A