The one-step local covering count (geometric heart of the sharp Margulis–Ruelle bound)

This module bounds the covering number of the image of a small ball under a continuous linear map on Euclidean space. It is the geometric heart of the sharp Margulis–Ruelle inequality (Liao–Qiu, Margulis–Ruelle inequality for general manifolds, §3, Lemmas 3.2–3.3): the entropy contribution of one dynamical step is controlled by how many balls of radius ~ε are needed to cover g '' B(x, ε), and Liao–Qiu's Lemma 3.3 shows this count is ≲ ‖(D_x g)^∧‖, i.e. the positive-part singular-value product ∏ᵢ max(1, σᵢ(D_x g)).

The route taken here

We use the volume → covering route named in the design:

• Oseledets.MeasureTheory.CoveringFromVolume turns a bound on the volume of the closed thickening of a set into a bound on its covering number: coveringNumber ε S ≤ V / ((ε/2) ^ d * μ (ball 0 1)) once μ (cthickening (ε/2) S) ≤ V.
• The image L '' closedBall x ε of a ball under a continuous linear map L lies in the ball closedBall (L x) (‖L‖ * ε) (operator-norm bound), so its ε/2-thickening is exactly closedBall (L x) (ε/2 + ‖L‖ ε) (Metric.cthickening_closedBall), of Haar volume (ε/2 + ‖L‖ ε) ^ d · μ (ball 0 1).

Dividing, the dimensional constant μ (ball 0 1) cancels and one obtains the clean isotropic covering count coveringNumber ε (L '' closedBall x ε) ≤ (2 ‖L‖ + 1) ^ d, with no smallness hypothesis on ε beyond positivity and no C¹ linearisation error, since L is genuinely linear. This is the k = d (top) truncation of the positive-part product ∏ᵢ max(1, σᵢ) = ⨆_{k≤d} ∏_{i<k} σᵢ (Oseledets.Entropy.Ruelle.VolumeDistortion): writing σ₀ = ‖L‖, ∏ᵢ max(1, σᵢ) ≤ (1 + σ₀) ^ d, so the isotropic bound is a valid but non-sharp upper bound for the positive-part product (Oseledets.prod_max_one_le_one_add_top_pow).

The isotropic count here vs. the sharp anisotropic count

The genuinely sharp count ≲ ∏ᵢ max(1, σᵢ(L)) (anisotropic: a thin pancake needs few balls along its thin directions) cannot be reached by the isotropic volume bound above, which only sees ‖L‖ = σ₀. The sharp count instead goes through a constructive SVD diagonalisation L = U Σ Vᵀ with U, V orthogonal: covering L '' ball = U (Σ '' ball) reduces, by isometry-invariance of covering numbers, to covering the axis-aligned ellipsoid Σ '' ball, an explicit product box of sides σᵢ ε covered by ∏ᵢ ⌈…⌉ ≲ ∏ᵢ max(1, σᵢ) boxes (Mañé's Lemma 12.5).

That sharp anisotropic count is fully proved in-tree in the sibling module Oseledets.Entropy.Ruelle.SharpCovering (Oseledets.coveringCount_image_ball_le_volProd, via the constructive Oseledets.svd_exists + an ellipsoid-domination volume bound, with dimensional constant 6^d). The present module records the simpler isotropic specialisation (2 ‖L‖ + 1) ^ d together with the explicit ∏ᵢ max(1, σᵢ) ≤ (1 + ‖L‖) ^ d comparison that locates it as the k = d extreme of the positive-part product; the sharp track uses the SharpCovering count.

Main results

• Metric.cthickening_image_closedBall_subset — the thickened linear image lies in a single ball: cthickening δ (L '' closedBall x ε) ⊆ closedBall (L x) (δ + ‖L‖ * ε).
• MeasureTheory.addHaar_cthickening_image_closedBall_le — its Haar volume bound.
• Metric.coveringCount_image_ball_linear_le — the isotropic one-step covering count: coveringNumber ε (L '' closedBall x ε) ≤ ENNReal.ofReal ((2 * ‖L‖ + 1) ^ d).
• Oseledets.prod_max_one_le_one_add_top_pow — the comparison ∏ᵢ max(1, σᵢ(L)) ≤ (1 + ‖L‖) ^ d, placing the sharp positive-part product below the isotropic count.

theorem Metric.image_closedBall_subset_closedBall_opNorm {d : ℕ} (L : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) (ε : ℝ) : ⇑L '' closedBall x ε ⊆ closedBall (L x) (‖L‖ * ε)

The image of a closed ball under a continuous linear map lies in a single closed ball of radius scaled by the operator norm: L '' closedBall x ε ⊆ closedBall (L x) (‖L‖ * ε).

theorem Metric.cthickening_image_closedBall_subset {d : ℕ} (L : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) {ε δ : ℝ} (hε : 0 ≤ ε) (hδ : 0 ≤ δ) : cthickening δ (⇑L '' closedBall x ε) ⊆ closedBall (L x) (δ + ‖L‖ * ε)

The thickened linear image lies in a single ball. The closed δ-thickening of the image of closedBall x ε under a continuous linear map L is contained in closedBall (L x) (δ + ‖L‖ * ε): the operator-norm bound puts the image inside closedBall (L x) (‖L‖ ε), and Metric.cthickening_closedBall enlarges the radius by exactly δ.

theorem MeasureTheory.addHaar_cthickening_image_closedBall_le {d : ℕ} (μ : Measure (EuclideanSpace ℝ (Fin d))) [μ.IsAddHaarMeasure] (L : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) {ε δ : ℝ} (hε : 0 ≤ ε) (hδ : 0 ≤ δ) : μ (Metric.cthickening δ (⇑L '' Metric.closedBall x ε)) ≤ ENNReal.ofReal ((δ + ‖L‖ * ε) ^ d) * μ (Metric.ball 0 1)

Haar volume of the thickened linear image. The Haar measure of the closed δ-thickening of L '' closedBall x ε is bounded by (δ + ‖L‖ ε) ^ d · μ (ball 0 1) — the volume of the enclosing ball closedBall (L x) (δ + ‖L‖ ε) from Metric.cthickening_image_closedBall_subset.

theorem Metric.coveringCount_image_ball_linear_le {d : ℕ} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))) [μ.IsAddHaarMeasure] (L : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) {ε : NNReal} (hε : 0 < ε) : ↑(coveringNumber ε (⇑L '' closedBall x ↑ε)) ≤ ENNReal.ofReal ((2 * ‖L‖ + 1) ^ d)

The isotropic one-step covering count (linear version). For a continuous linear map L on EuclideanSpace ℝ (Fin d) and ε > 0, the ε-covering number of the image L '' closedBall x ε is bounded by (2 ‖L‖ + 1) ^ d.

This is the linear instance of Liao–Qiu's one-step covering count (§3, Lemma 3.3) obtained by the volume → covering route: the ε/2-thickening of the image fits inside closedBall (L x) (ε/2 + ‖L‖ ε) (cthickening_image_closedBall_subset), of Haar volume (ε/2 + ‖L‖ ε) ^ d · μ (ball 0 1), and coveringNumber_le_addHaar_div_of_addHaar_le divides by (ε/2) ^ d · μ (ball 0 1). The dimensional constant μ (ball 0 1) cancels and (ε/2 + ‖L‖ ε) / (ε/2) = 2 ‖L‖ + 1.

It is the k = d (isotropic, top) truncation of the sharp positive-part product ∏ᵢ max(1, σᵢ(L)); see Oseledets.prod_max_one_le_one_add_top_pow for the comparison ∏ᵢ max(1, σᵢ) ≤ (1 + ‖L‖) ^ d ≤ (2 ‖L‖ + 1) ^ d.

theorem Oseledets.prod_max_one_le_one_add_top_pow {σ : ℕ → ℝ} (hanti : Antitone σ) (hpos : ∀ (i : ℕ), 0 ≤ σ i) (d : ℕ) : ∏ i ∈ Finset.range d, max 1 (σ i) ≤ (1 + σ 0) ^ d

The positive-part product is dominated by the isotropic count (abstract). For an antitone, nonnegative sequence σ (the singular values are such), every term satisfies σᵢ ≤ σ₀, hence max(1, σᵢ) ≤ 1 + σ₀, so the positive-part product over range d is at most (1 + σ 0) ^ d.

Applied to the singular values of a continuous linear map L with σ₀ = ‖L‖, this locates the sharp anisotropic count ∏ᵢ max(1, σᵢ) (Liao–Qiu Lemma 3.3) below the isotropic count (2 ‖L‖ + 1) ^ d of Metric.coveringCount_image_ball_linear_le: ∏ᵢ max(1, σᵢ) ≤ (1 + σ₀) ^ d ≤ (2 σ₀ + 1) ^ d. This is the abstract antitone-sequence form, so it needs no operator-norm/singular-value bridge (σ₀ = ‖L‖) and keeps the import footprint light.