Covering numbers from volume (Mañé's Lemma 12.5)

In a finite-dimensional real normed space E equipped with an additive Haar measure μ, the ε-covering number of a set S is controlled by the volume of S (more precisely by the volume of a closed thickening of S). This is the metric-entropy counterpart of the elementary fact that one cannot pack too many disjoint balls inside a set of finite measure.

The geometric core is a packing estimate: an ε-separated subset of S gives rise to pairwise disjoint closed balls of radius ε / 2, each contained in the closed ε/2-thickening of S. Summing the (centre-independent) volumes of these balls yields

packingNumber ε S * μ (closedBall 0 (ε/2)) ≤ μ (cthickening (ε/2) S).

Combining with Metric.coveringNumber_le_packingNumber and the Haar ball-volume scaling MeasureTheory.Measure.addHaar_closedBall turns this into an explicit dimensional bound

coveringNumber ε S ≤ V / (ε/2) ^ d * (constant),

stated below for EuclideanSpace ℝ (Fin d) as Metric.coveringNumber_le_addHaar_div_of_addHaar_le.

This is the abstract input behind Mañé's Lemma 12.5 (Ricardo Mañé, Ergodic theory and differentiable dynamics, Springer 1987), used in the Margulis–Ruelle inequality to bound the number of partition elements meeting the image of a box by the volume distortion of the map.

Main statements

• Metric.IsSeparated.pairwiseDisjoint_closedBall: an ε-separated set has pairwise disjoint closed balls of radius ε / 2.
• MeasureTheory.encard_mul_addHaar_closedBall_le_addHaar_cthickening: for a separated C ⊆ S, C.encard * μ (closedBall 0 (ε/2)) ≤ μ (cthickening (ε/2) S).
• MeasureTheory.packingNumber_mul_addHaar_closedBall_le_addHaar_cthickening: the packing-number form of the previous estimate.
• MeasureTheory.coveringNumber_mul_addHaar_closedBall_le_addHaar_cthickening: the covering-number form (via coveringNumber ≤ packingNumber).
• Metric.coveringNumber_le_addHaar_div_of_addHaar_le: the explicit dimensional bound coveringNumber ε S ≤ V / ((ε/2) ^ d * μ (ball 0 1)) on EuclideanSpace ℝ (Fin d).

theorem ENat.toENNReal_iSup_le {ι : Sort u_1} (g : ι → ℕ∞) : ↑(⨆ (i : ι), g i) ≤ ⨆ (i : ι), ↑(g i)

The coercion ℕ∞ → ℝ≥0∞ is sub-additive over suprema: ↑(⨆ i, g i) ≤ ⨆ i, ↑(g i).

This is the easy direction of ENat.toENNReal_iSup (the full equality lives in a Mathlib file not in this import closure). It is all that is needed for the supremum in packingNumber.

theorem ENat.toENNReal_iSup_mul_le {ι : Sort u_1} (g : ι → ℕ∞) (c V : ENNReal) (h : ∀ (i : ι), ↑(g i) * c ≤ V) : ↑(⨆ (i : ι), g i) * c ≤ V

If each coerced term times c is bounded by V, then so is the coerced supremum times c. A convenience wrapper used to pass a volume bound through the supremum in packingNumber.

theorem Metric.IsSeparated.pairwiseDisjoint_closedBall {E : Type u_1} [NormedAddCommGroup E] {ε : NNReal} {C : Set E} (hC : IsSeparated (↑ε) C) : C.PairwiseDisjoint fun (x : E) => closedBall x (↑ε / 2)

An ε-separated set gives pairwise disjoint closed balls of radius ε / 2.

If two points x ≠ y are ε-separated (ε < edist x y) then their closed balls of radius ε / 2 are disjoint: a common point z would force dist x y ≤ dist x z + dist z y ≤ ε, contradicting the separation.

theorem MeasureTheory.encard_mul_addHaar_closedBall_le_addHaar_cthickening {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] {ε : NNReal} {S C : Set E} (hCS : C ⊆ S) (hC : Metric.IsSeparated (↑ε) C) : ↑C.encard * μ (Metric.closedBall 0 (↑ε / 2)) ≤ μ (Metric.cthickening (↑ε / 2) S)

Packing-from-volume, set form. If C ⊆ S is ε-separated, the number of points in C times the volume of a closed ball of radius ε / 2 is at most the volume of the closed ε/2-thickening of S.

The closed balls of radius ε / 2 centred at points of C are pairwise disjoint (Metric.IsSeparated.pairwiseDisjoint_closedBall), each contained in cthickening (ε/2) S, and each of the (centre-independent) volume μ (closedBall 0 (ε/2)).

theorem MeasureTheory.packingNumber_mul_addHaar_closedBall_le_addHaar_cthickening {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] {ε : NNReal} (S : Set E) : ↑(Metric.packingNumber ε S) * μ (Metric.closedBall 0 (↑ε / 2)) ≤ μ (Metric.cthickening (↑ε / 2) S)

Packing-from-volume, packing-number form. The packing number of S for radius ε times the volume of a closed ball of radius ε / 2 is at most the volume of the closed ε/2-thickening of S.

theorem MeasureTheory.coveringNumber_mul_addHaar_closedBall_le_addHaar_cthickening {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] {ε : NNReal} (S : Set E) : ↑(Metric.coveringNumber ε S) * μ (Metric.closedBall 0 (↑ε / 2)) ≤ μ (Metric.cthickening (↑ε / 2) S)

Packing-from-volume, covering-number form. The covering number of S for radius ε times the volume of a closed ball of radius ε / 2 is at most the volume of the closed ε/2-thickening of S. Immediate from the packing form via Metric.coveringNumber_le_packingNumber.

theorem Metric.coveringNumber_le_addHaar_div_of_addHaar_le {d : ℕ} {ε : NNReal} {S : Set (EuclideanSpace ℝ (Fin d))} {V : ENNReal} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))) [μ.IsAddHaarMeasure] (hε : 0 < ε) (hV : μ (cthickening (↑ε / 2) S) ≤ V) : ↑(coveringNumber ε S) ≤ V / (ENNReal.ofReal ((↑ε / 2) ^ d) * μ (ball 0 1))

Covering number from volume (Mañé's Lemma 12.5), explicit dimensional form.

In EuclideanSpace ℝ (Fin d) with an additive Haar measure μ, if a set S has μ (cthickening (ε/2) S) ≤ V and ε > 0, then its ε-covering number is bounded by

V / ((ε / 2) ^ d * μ (ball 0 1)),

i.e. (up to the dimensional constant μ (ball 0 1)) by V / (ε/2) ^ d. In particular, since cthickening (ε/2) S has finite measure whenever S does, this gives an explicit finite covering number for bounded measurable sets.