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 coveringNumber_Icc_zero_one_le_one_div {ε : NNReal} (hε : ε ≤ 1) : ↑(Metric.coveringNumber ε (Set.Icc 0 1)) ≤ 1 / ↑ε

theorem Metric.measure_le_of_isCover {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {ε : NNReal} {A C : Set E} (hC : IsCover ε A C) (hε : ε ≠ 0) : μ A ≤ ↑C.encard * μ (closedEBall 0 ↑ε)

If C is an ε-cover of A, the measure of A is at most the cardinality of C times the measure of a ball of radius ε.

theorem Metric.measure_le_externalCoveringNumber_mul {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {ε : NNReal} (A : Set E) (hε : ε ≠ 0) : μ A ≤ ↑(externalCoveringNumber ε A) * μ (closedEBall 0 ↑ε)

The measure of A is at most the external covering number of A at scale ε times the measure of a ball of radius ε.

theorem Metric.le_measure_of_isSeparated {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {ε : NNReal} {A C : Set E} (hC : IsSeparated (↑ε) C) (h_subset : C ⊆ A) : ↑C.encard * μ (closedEBall 0 (↑ε / 2)) ≤ μ (A + closedEBall 0 (↑ε / 2))

If C ⊆ A is ε-separated, the cardinality of C times the measure of a ball of radius ε / 2 is at most the measure of the ε / 2-thickening of A.

theorem Metric.packingNumber_mul_le_measure {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (A : Set E) (ε : NNReal) : ↑(packingNumber ε A) * μ (closedEBall 0 (↑ε / 2)) ≤ μ (A + closedEBall 0 (↑ε / 2))

The packing number of A at scale ε times the measure of a ball of radius ε / 2 is at most the measure of the ε / 2-thickening of A.

theorem Metric.measure_eq_top_of_packingNumber {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {ε : NNReal} (A : Set E) (hε : ε ≠ 0) (h : packingNumber ε A = ⊤) : μ (A + closedEBall 0 (↑ε / 2)) = ⊤

theorem Metric.measure_div_le_externalCoveringNumber {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {ε : NNReal} (A : Set E) (hε : ε ≠ 0) : μ A / μ (closedEBall 0 ↑ε) ≤ ↑(externalCoveringNumber ε A)

The measure of A divided by the measure of a ball of radius ε is a lower bound for the external covering number of A at scale ε.

theorem Metric.measure_div_le_coveringNumber {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {ε : NNReal} (A : Set E) (hε : ε ≠ 0) : μ A / μ (closedEBall 0 ↑ε) ≤ ↑(coveringNumber ε A)

The measure of A divided by the measure of a ball of radius ε is a lower bound for the covering number of A at scale ε.

theorem Metric.coveringNumber_le_measure_div {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {ε : NNReal} [ProperSpace E] (A : Set E) (hε : ε ≠ 0) : ↑(coveringNumber ε A) ≤ μ (A + closedEBall 0 (↑ε / 2)) / μ (closedEBall 0 (↑ε / 2))

The measure of the ε / 2-thickening of A divided by the measure of a ball of radius ε / 2 is an upper bound for the covering number of A at scale ε.

theorem Metric.coveringNumber_closedEBall_ge {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (ε : NNReal) (x : E) {r : NNReal} (hr : r ≠ 0) : (↑r / ↑ε) ^ Module.finrank ℝ E ≤ ↑(coveringNumber ε (closedEBall x ↑r))

A ball of radius r in dimension d has covering number at least (r / ε) ^ d at scale ε.

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

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

A ball of radius r in dimension d has covering number at most (2 * r / ε + 1) ^ d at scale ε.

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

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

If ε ≤ r, a ball of radius r in dimension d has covering number at most (3 * r / ε) ^ d at scale ε.