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 ≤ ε

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} [PseudoEMetricSpace E] (r : ENNReal) (A : Set E) : ℕ∞

Equations

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

theorem internalCoveringNumber_le_of_isCover {E : Type u_1} [EDist E] {C : Finset E} {r : ENNReal} {A : Set E} (C_sub : ↑C ⊆ A) (C_cov : IsCover (↑C) r A) : internalCoveringNumber r A ≤ ↑C.card

@[simp]

theorem IsCover.self {E : Type u_1} [PseudoEMetricSpace E] (A : Set E) (r : ENNReal) : IsCover A r A

theorem Set.Finite.internalCoveringNumber_le_ncard {E : Type u_1} [PseudoEMetricSpace E] (r : ENNReal) (A : Set E) (ha : A.Finite) : internalCoveringNumber r A ≤ ↑A.ncard

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 ε

theorem isCover_empty_iff {E : Type u_1} [EDist E] (ε : ENNReal) (A : Set E) : IsCover ∅ ε A ↔ A = ∅

theorem isCover_empty {E : Type u_1} [EDist E] (ε : ENNReal) : IsCover ∅ ε ∅

theorem not_isCover_empty {E : Type u_1} [EDist E] (ε : ENNReal) (A : Set E) (h_nonempty : A.Nonempty) : ¬IsCover ∅ ε A

@[simp]

theorem internalCoveringNumber_empty {E : Type u_1} [EDist E] (r : ENNReal) : internalCoveringNumber r ∅ = 0

@[simp]

theorem externalCoveringNumber_empty {E : Type u_1} [EDist E] (r : ENNReal) : externalCoveringNumber r ∅ = 0

theorem isCover_singleton_of_diam_le {E : Type u_1} [PseudoEMetricSpace E] {ε : ENNReal} {A : Set E} {a : E} (hA : EMetric.diam A ≤ ε) (ha : a ∈ A) : IsCover {a} ε A

theorem isCover_singleton_finset_of_diam_le {E : Type u_1} [PseudoEMetricSpace E] {ε : ENNReal} {A : Set E} {a : E} (hA : EMetric.diam A ≤ ε) (ha : a ∈ A) : IsCover (↑{a}) ε A

theorem cover_eq_of_lt_iInf_edist {E : Type u_1} [PseudoEMetricSpace E] {C : Set E} {ε : ENNReal} {A : Set E} (hC : IsCover C ε A) (hC_subset : C ⊆ A) (hε : ε < ⨅ (s : ↑A), ⨅ (t : { t : ↑A // s ≠ t }), edist s ↑t) : C = A

theorem IsCover.mono {E : Type u_1} [EDist E] {C : Set E} {ε ε' : ENNReal} {A : Set E} (h : ε ≤ ε') (hC : IsCover C ε A) : IsCover C ε' A

theorem IsCover.subset {E : Type u_1} [EDist E] {C : Set E} {ε : ENNReal} {A B : Set E} (h : A ⊆ B) (hC : IsCover C ε B) : IsCover C ε A

theorem internalCoveringNumber_anti {E : Type u_1} [EDist E] {r r' : ENNReal} {A : Set E} (h : r ≤ r') : internalCoveringNumber r' A ≤ internalCoveringNumber r A

theorem internalCoveringNumber_eq_one_of_diam_le {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} {A : Set E} (h_nonempty : A.Nonempty) (hA : EMetric.diam A ≤ r) : internalCoveringNumber r A = 1

theorem externalCoveringNumber_eq_one_of_diam_le {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} {A : Set E} (h_nonempty : A.Nonempty) (hA : EMetric.diam A ≤ r) : externalCoveringNumber r A = 1

theorem internalCoveringNumber_le_one_of_diam_le {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} {A : Set E} (hA : EMetric.diam A ≤ r) : internalCoveringNumber r A ≤ 1

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] {r : ENNReal} {A : Set E} (h : TotallyBounded A) (hr : 0 < r) : ∃ (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) (hr : 0 < r) : Finset E

An internal r-cover of A with minimal cardinal.

Equations

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

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

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

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

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

noncomputable def maximalSeparatedSet {E : Type u_1} [PseudoEMetricSpace 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} [PseudoEMetricSpace E] : ↑(maximalSeparatedSet r A) ⊆ A

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

theorem card_maximalSeparatedSet {E : Type u_1} {r : ENNReal} {A : Set E} [PseudoEMetricSpace 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} [PseudoEMetricSpace E] {C : Finset E} (h_subset : ↑C ⊆ A) (h_sep : Metric.IsSeparated r ↑C) (h : packingNumber r A < ⊤) : 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} [PseudoEMetricSpace E] {r : ENNReal} (A : Set E) (hr : r ≠ ⊤) : 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

theorem externalCoveringNumber_mono_set {E : Type u_1} [EDist E] {r : ENNReal} {A B : Set E} (h : A ⊆ B) : externalCoveringNumber r A ≤ externalCoveringNumber r B

theorem internalCoveringNumber_subset_le {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} (hr : r ≠ ⊤) {A B : Set E} (h : A ⊆ B) : internalCoveringNumber r A ≤ internalCoveringNumber (r / 2) B

theorem internalCoveringNumber_le_encard {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} {A : Set E} (hr : 0 < r) : internalCoveringNumber r A ≤ A.encard

theorem internalCoveringNumber_smul {E : Type u_1} [NormedAddCommGroup E] [Module ℝ E] {r : ENNReal} {A : Set E} {c : NNReal} (hc : c ≠ 0) : internalCoveringNumber (↑c * r) (c • A) = internalCoveringNumber r A

theorem internalCoveringNumber_Icc_zero_one_le_one_div {ε : ENNReal} (hε : ε ≤ 1) : ↑(internalCoveringNumber ε (Set.Icc 0 1)) ≤ 1 / ε

theorem internalCoveringNumber_Ico_zero_one_le_one_div {ε : ENNReal} (hε : ε ≤ 1) : ↑(internalCoveringNumber ε (Set.Ico 0 1)) ≤ 1 / ε

theorem volume_le_of_isCover {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {A : Set E} {C : Finset E} {ε : ENNReal} (hC : IsCover (↑C) ε A) : MeasureTheory.volume A ≤ ↑C.card * MeasureTheory.volume (EMetric.closedBall 0 ε)

theorem volume_le_externalCoveringNumber_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (A : Set E) (ε : ENNReal) : MeasureTheory.volume A ≤ ↑(externalCoveringNumber ε A) * MeasureTheory.volume (EMetric.closedBall 0 ε)

theorem le_volume_of_isSeparated {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {A : Set E} {C : Finset E} {ε : ENNReal} (hC : Metric.IsSeparated ε ↑C) (h_subset : ↑C ⊆ A) : ↑C.card * MeasureTheory.volume (EMetric.closedBall 0 (ε / 2)) ≤ MeasureTheory.volume (A + EMetric.closedBall 0 (ε / 2))

theorem packingNumber_mul_le_volume {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (A : Set E) (ε : ENNReal) : ↑(packingNumber ε A) * MeasureTheory.volume (EMetric.closedBall 0 (ε / 2)) ≤ MeasureTheory.volume (A + EMetric.closedBall 0 (ε / 2))

theorem volume_div_le_internalCoveringNumber {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (A : Set E) (ε : ENNReal) : MeasureTheory.volume A / MeasureTheory.volume (EMetric.closedBall 0 ε) ≤ ↑(internalCoveringNumber ε A)

theorem internalCoveringNumber_le_volume_div {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (A : Set E) (ε : ENNReal) : ↑(internalCoveringNumber ε A) ≤ MeasureTheory.volume (A + EMetric.closedBall 0 (ε / 2)) / MeasureTheory.volume (EMetric.closedBall 0 (ε / 2))

theorem internalCoveringNumber_closedBall_ge {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ε : ENNReal) : ε⁻¹ ^ Module.finrank ℝ E ≤ ↑(internalCoveringNumber ε (EMetric.closedBall 0 1))

theorem internalCoveringNumber_closedBall_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ε : ENNReal) : ↑(internalCoveringNumber ε (EMetric.closedBall 0 1)) ≤ (2 / ε + 1) ^ Module.finrank ℝ E