The sharp anisotropic one-step covering count #
This module proves the sharp, anisotropic covering-count estimate that the isotropic volume
bound of Oseledets.Entropy.Ruelle.LocalCovering left open (Liao–Qiu,
Margulis–Ruelle inequality for general manifolds, §3, Lemmas 3.2–3.3).
For a linear map L : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d) (the derivative of
one dynamical step) and ε > 0, the ε-covering number of the image L '' closedBall x ε of a
small ball is bounded by a dimensional constant times the positive-part singular-value product:
$$N_\varepsilon\big(L(B(x,\varepsilon))\big)\;\le\; C_d \cdot \prod_i \max(1,\sigma_i),$$
where σ₀ ≥ σ₁ ≥ ⋯ are the singular values of L. This is sharp: a thin pancake (some
σᵢ ≪ 1) is covered by few balls along its thin directions, which the isotropic bound
(2‖L‖ + 1)^d (seeing only σ₀ = ‖L‖) cannot detect.
The route taken here: SVD ellipsoid domination + determinant volume #
The lossy ‖L‖-only volume bound is replaced by a genuine singular-value decomposition
(svd_exists): orthonormal bases b (eigenbasis of Lᵀ L in the domain) and c (an extension of
the normalised image frame σᵢ⁻¹ • L bᵢ) of EuclideanSpace ℝ (Fin d) such that L bᵢ = σᵢ • cᵢ
for all i. In these coordinates L '' closedBall 0 ε is the axis-aligned ellipsoid with
semi-axes ε σᵢ.
The δ-thickening of this ellipsoid is contained in the dilated ellipsoid
c.repr.symm '' (diagMap (2(ε σ + δ)) '' B(0,1))
(cthickening_image_closedBall_subset_ellipsoid, a weighted-L² triangle inequality:
‖·‖ₐ ≤ ‖signal‖ₐ + ‖noise‖ₐ ≤ ½ + ½ with aᵢ = 2(ε σᵢ + δ)). Transporting the volume through the
measure-preserving frame isometry c.repr.symm and applying the diagonal determinant law
MeasureTheory.Measure.addHaar_image_linearMap gives the volume
∏ᵢ 2(ε σᵢ + δ) · volume(B 0 1) (volume_cthickening_image_closedBall_le_volProd). With
δ = ε/2,
Oseledets.MeasureTheory.CoveringFromVolume's volume → covering bound divides by (ε/2)^d · volume(B 0 1):
the dimensional constant cancels and ∏ᵢ 2(ε σᵢ + ε/2)/(ε/2)^d = ∏ᵢ (4 σᵢ + 2) ≤ 6^d ∏ᵢ max(1, σᵢ)
(prod_four_mul_add_two_le). The general centre x is reduced to the origin by the
covering-number isometry invariance under the translation y ↦ L x + y.
Main results #
Oseledets.svd_exists— the constructive singular-value decompositionL bᵢ = σᵢ • cᵢwith orthonormal basesb, c, identifyingσᵢwithLinearMap.singularValues.Oseledets.cthickening_image_closedBall_subset_ellipsoid— the ellipsoid domination of the thickened image (the geometric heart, the weighted-L²triangle inequality).Oseledets.volume_cthickening_image_closedBall_le_volProd— the anisotropic volumevolume(cthickening δ (L '' B(0,ε))) ≤ ∏ᵢ 2(ε σᵢ + δ) · volume(B 0 1).Oseledets.coveringCount_image_ball_le_volProd— the sharp anisotropic one-step covering countcoveringNumber ε (L '' B(x,ε)) ≤ 6^d · ∏ᵢ max(1, σᵢ(L)).
Singular value decomposition (existence form). For a linear self-map L of
EuclideanSpace ℝ (Fin d) there are an orthonormal basis b (the eigenbasis of the Gram operator
Lᵀ L, i.e. the right singular vectors), an orthonormal basis c (the left singular vectors), and
a nonnegative antitone sequence σ (the singular values) such that L bᵢ = σᵢ • cᵢ for every i,
and σᵢ² = ⟪L bᵢ, L bᵢ⟫ so that σᵢ = ‖L bᵢ‖.
This is the constructive SVD that pinned Mathlib's singularValues API stops short of: it exposes
the factorisation L = c.repr.symm ∘ Diag σ ∘ b.repr the sharp covering count needs.
The left frame c is built by normalising the nonzero L bᵢ and extending to an orthonormal basis
(Orthonormal.exists_orthonormalBasis_extension_of_card_eq).
The diagonal scaling map and its image of the unit ball #
The sharp anisotropic covering count #
The ellipsoid containment (geometric heart). With singular data b, c, σ of L
(svd_exists) and aᵢ := 2(ε σᵢ + δ) (ε, δ > 0), the δ-thickening of the image of the unit
ε-ball (centred at origin) is contained in the ellipsoid c.repr.symm '' (diagMap a '' B(0,1)).
This is the weighted-L² triangle inequality: for w within δ of z = L y, ‖y‖ ≤ ε, the
coordinates tᵢ := ⟪cᵢ, w⟫ / aᵢ satisfy ∑ tᵢ² ≤ 1 because ‖t‖ ≤ ‖t_z‖ + ‖t_{w-z}‖, where the
"signal" part has ∑ σᵢ²(Ry)ᵢ²/aᵢ² ≤ ‖y‖²/(2ε)² ≤ ¼ (using aᵢ ≥ 2ε σᵢ) and the "noise" part has
∑ ⟪cᵢ, w-z⟫²/aᵢ² ≤ ‖w-z‖²/(2δ)² ≤ ¼ (using aᵢ ≥ 2δ), giving ‖t‖ ≤ ½ + ½ = 1.
Anisotropic thickened-image volume bound (at the origin). For ε, δ > 0, the volume of the
δ-thickening of the image L '' closedBall 0 ε of a small ball under a continuous linear self-map
L of EuclideanSpace ℝ (Fin d) is bounded by ∏ᵢ 2(ε σᵢ + δ) · volume(ball 0 1), where σᵢ are
the singular values of L (via the SVD svd_exists).
This is the sharp anisotropic replacement for the isotropic
MeasureTheory.addHaar_cthickening_image_closedBall_le (which sees only ‖L‖ = σ₀): the thin
directions (σᵢ ≪ 1) genuinely shrink the product. The proof dominates the thickened ellipsoid
L '' closedBall 0 ε ⊕ ball δ by the ellipsoid c.repr.symm '' (diagMap (2(ε σ + δ)) '' ball 0 1)
(cthickening_image_closedBall_subset_ellipsoid), transports the volume through the measure-
preserving frame isometry c.repr.symm (measure_preimage of the inverse isometry), and applies
the determinant volume law addHaar_image_diagMap.
The per-factor anisotropic bound 4σᵢ + 2 ≤ 6 · max(1, σᵢ) packaged as a product:
∏ᵢ (4σᵢ + 2) ≤ 6^d · ∏ᵢ max(1, σᵢ). Each factor: if σᵢ ≤ 1 then 4σᵢ + 2 ≤ 6 = 6 · 1; if
σᵢ ≥ 1 then 4σᵢ + 2 ≤ 6σᵢ. This converts the explicit covering count into the canonical
positive-part singular-value product ∏ᵢ max(1, σᵢ) with the dimensional constant 6^d.
The sharp anisotropic one-step covering count. For a continuous linear self-map L of
EuclideanSpace ℝ (Fin d) and ε > 0, the ε-covering number of the image L '' closedBall x ε
of a small ball is bounded by 6^d · ∏ᵢ max(1, σᵢ(L)), the dimensional constant times the
positive-part singular-value product of L.
This is the genuinely sharp anisotropic Liao–Qiu one-step count (§3, Lemmas 3.2–3.3): a thin
pancake (σᵢ ≪ 1) needs few balls along its thin directions, in contrast to the isotropic
(2‖L‖ + 1)^d of Metric.coveringCount_image_ball_linear_le which sees only σ₀ = ‖L‖.
The proof: at origin, the SVD (svd_exists) + ellipsoid domination + determinant volume law give
volume(cthickening (ε/2) (L '' B(0,ε))) ≤ ∏ᵢ 2(ε σᵢ + ε/2) · volume(B 0 1)
(volume_cthickening_image_closedBall_le_volProd); the volume → covering bound
Metric.coveringNumber_le_addHaar_div_of_addHaar_le divides by (ε/2)^d · volume(B 0 1), the
dimensional constant cancels and ∏ᵢ 2(ε σᵢ + ε/2)/(ε/2)^d = ∏ᵢ (4 σᵢ + 2) ≤ 6^d ∏ᵢ max(1, σᵢ)
(prod_four_mul_add_two_le). The general centre x is reduced to the origin by the
covering-number isometry invariance Isometry.coveringNumber_image under y ↦ L x + y.