Covering and packing numbers

References

• Vershynin, High-Dimensional Probability (section 4.2)

theorem TotallyBounded.coveringNumber_ne_top {E : Type u_1} [PseudoEMetricSpace E] {A : Set E} (hA : TotallyBounded A) {r : NNReal} (hr : r ≠ 0) : Metric.coveringNumber r A ≠ ⊤

theorem Isometry.isCover_image_iff {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} {F : Type u_2} [PseudoEMetricSpace F] {f : E → F} (hf : Isometry f) (C : Set E) : Metric.IsCover r (f '' A) (f '' C) ↔ Metric.IsCover r A C

theorem Isometry.coveringNumber_image' {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} {F : Type u_2} [PseudoEMetricSpace F] {f : E → F} (hf : Isometry f) (hf_inj : Set.InjOn f A) : Metric.coveringNumber r (f '' A) = Metric.coveringNumber r A

theorem Isometry.coveringNumber_image {r : NNReal} {E : Type u_2} {F : Type u_3} [EMetricSpace E] [PseudoEMetricSpace F] {f : E → F} (hf : Isometry f) {A : Set E} : Metric.coveringNumber r (f '' A) = Metric.coveringNumber r A

theorem coveringNumber_Icc_zero_one_le_one_div {ε : NNReal} (hε : ε ≤ 1) : ↑(Metric.coveringNumber ε (Set.Icc 0 1)) ≤ 1 / ↑ε

theorem EMetric.isCover_iff_subset_iUnion_closedBall {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s N : Set X} : Metric.IsCover ε s N ↔ s ⊆ ⋃ y ∈ N, Metric.closedEBall y ↑ε

theorem volume_le_of_isCover {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} {A C : Set E} (hC : Metric.IsCover ε A C) (hε : 0 < ε) : MeasureTheory.volume A ≤ ↑C.encard * MeasureTheory.volume (Metric.closedEBall 0 ↑ε)

theorem volume_le_externalCoveringNumber_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} (A : Set E) (hε : 0 < ε) : MeasureTheory.volume A ≤ ↑(Metric.externalCoveringNumber ε A) * MeasureTheory.volume (Metric.closedEBall 0 ↑ε)

theorem le_volume_of_isSeparated_of_countable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} {A C : Set E} (hC_count : C.Countable) (hC : Metric.IsSeparated (↑ε) C) (h_subset : C ⊆ A) : ↑C.encard * MeasureTheory.volume (Metric.closedEBall 0 (↑ε / 2)) ≤ MeasureTheory.volume (A + Metric.closedEBall 0 (↑ε / 2))

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

theorem volume_eq_top_of_packingNumber {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} (A : Set E) (hε : 0 < ε) (h : Metric.packingNumber ε A = ⊤) : MeasureTheory.volume (A + Metric.closedEBall 0 (↑ε / 2)) = ⊤

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

theorem volume_div_le_coveringNumber {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} (A : Set E) (hε : 0 < ε) : MeasureTheory.volume A / MeasureTheory.volume (Metric.closedEBall 0 ↑ε) ≤ ↑(Metric.coveringNumber ε A)

theorem coveringNumber_le_volume_div {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} (A : Set E) (hε₁ : 0 < ε) : ↑(Metric.coveringNumber ε A) ≤ MeasureTheory.volume (A + Metric.closedEBall 0 (↑ε / 2)) / MeasureTheory.volume (Metric.closedEBall 0 (↑ε / 2))

theorem coveringNumber_closedBall_ge {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ε : NNReal) (x : E) {r : NNReal} (hr : 0 < r) : (↑r / ↑ε) ^ Module.finrank ℝ E ≤ ↑(Metric.coveringNumber ε (Metric.closedEBall x ↑r))

theorem coveringNumber_closedBall_one_ge {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ε : NNReal) (x : E) : (↑ε)⁻¹ ^ Module.finrank ℝ E ≤ ↑(Metric.coveringNumber ε (Metric.closedEBall x 1))

theorem coveringNumber_closedBall_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ε : NNReal) (x : E) (r : NNReal) : ↑(Metric.coveringNumber ε (Metric.closedEBall x ↑r)) ≤ (2 * ↑r / ↑ε + 1) ^ Module.finrank ℝ E

theorem coveringNumber_closedBall_one_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ε : NNReal) (x : E) : ↑(Metric.coveringNumber ε (Metric.closedEBall x 1)) ≤ (2 / ↑ε + 1) ^ Module.finrank ℝ E

theorem coveringNumber_closedBall_le_three_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} [Nontrivial E] {x : E} {r : NNReal} (hr_zero : r ≠ 0) (hε : ε ≤ r) : ↑(Metric.coveringNumber ε (Metric.closedEBall x ↑r)) ≤ (3 * ↑r / ↑ε) ^ Module.finrank ℝ E