Positive-part volume distortion: the singular-value product the covering count consumes

This module proves the algebraic identity at the heart of the positive-part volume distortion appearing in the Margulis–Ruelle covering-count estimate (Liao–Qiu, Margulis–Ruelle inequality for general manifolds, §3, Lemmas 3.2–3.3): the local volume expansion factor counting only the expanding directions of a linear map is

$$\prod_{i} \max(1, \sigma_i) \;=\; \sup_{0 \le k \le d} \prod_{i < k} \sigma_i \;=\; \sup_{0 \le k \le d} \lVert C_k(M) \rVert,$$

where σ₀ ≥ σ₁ ≥ ⋯ are the singular values and C_k(M) is the k-th compound matrix.

Geometrically, the cthickening of a thin box M '' B is covered by a number of unit cells comparable to ∏ᵢ max(1, σᵢ M) (Lemma 3.2 bounds the cover of a box with sides aᵢ by c · ∏ᵢ max(aᵢ, 1); for a thickened image the relevant sides are σᵢ), and Lemma 3.3 packages this as the operator norm of the exterior power ‖(D_x g)^∧‖ = max_κ ‖(D_x g)^{∧κ}‖, i.e. the maximal compound operator norm. This is exactly the form (b) requested: it bridges |det M| = ∏ σᵢ (the full product, the k = d term) with the ∏ max(1, σᵢ) that the count needs, by selecting the optimal truncation k of the singular-value product.

Main results

• Oseledets.prod_max_one_eq_sup_prod_range — the abstract algebraic identity for any antitone, nonnegative sequence: ∏_{i<d} max(1, σᵢ) = ⨆_{k≤d} ∏_{i<k} σᵢ (Finset.sup').
• Oseledets.prod_max_one_singularValues_eq_sup_prod_range — its specialization to the singular values of a linear map between finite-dimensional inner product spaces.
• Oseledets.prod_max_one_singularValues_eq_sup_opNorm_compound — the compound bridge: for a square matrix M, ∏_{i<d} max(1, σᵢ(M)) = ⨆_{k≤d} ‖C_k(M)‖, the maximal compound operator norm that the covering count consumes.

Implementation notes

The abstract identity is proved by an antichain/prefix argument. Antitonicity makes the index set {i < d : 1 ≤ σ i} an initial segment range k*, where k* := #{i < d : 1 ≤ σ i}. The partial product ∏_{i<k*} σ i then equals ∏_{i<d} max(1, σ i) (the truncated factors σ i < 1 contribute max(1, σ i) = 1), and it dominates every other partial product ∏_{i<k} σ i by monotonicity of products over [0,1]-padded factors. The compound bridge is then immediate from the repository identity Oseledets.ExteriorNorm.prod_singularValues_eq_l2_opNorm_compound.

The abstract algebraic identity for an antitone nonnegative sequence

theorem Oseledets.range_filter_one_le_eq_range {σ : ℕ → ℝ} (hanti : Antitone σ) (d : ℕ) : {i ∈ Finset.range d | 1 ≤ σ i} = Finset.range {i ∈ Finset.range d | 1 ≤ σ i}.card

The prefix {i < d : 1 ≤ σ i} of an antitone sequence is an initial segment range k. Its cardinality k = #{i < d : 1 ≤ σ i} is the number of singular values that are ≥ 1, i.e. the expanding directions.

theorem Oseledets.prod_max_one_eq_sup_prod_range {σ : ℕ → ℝ} (hanti : Antitone σ) (hpos : ∀ (i : ℕ), 0 ≤ σ i) (d : ℕ) : ∏ i ∈ Finset.range d, max 1 (σ i) = (Finset.range (d + 1)).sup' ⋯ fun (k : ℕ) => ∏ i ∈ Finset.range k, σ i

The positive-part singular-value product as a supremum of partial products (abstract). For an antitone nonnegative sequence σ and a horizon d, the product of the positive parts ∏_{i<d} max(1, σ i) equals the supremum over truncations 0 ≤ k ≤ d of the partial products ∏_{i<k} σ i. The optimal truncation k* = #{i < d : 1 ≤ σ i} keeps exactly the expanding factors.

Specialization to singular values

theorem Oseledets.prod_max_one_singularValues_eq_sup_prod_range {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (f : E →ₗ[ℝ] F) (d : ℕ) : ∏ i ∈ Finset.range d, max 1 (f.singularValues i) = (Finset.range (d + 1)).sup' ⋯ fun (k : ℕ) => ∏ i ∈ Finset.range k, f.singularValues i

The positive-part singular-value product as a supremum of partial products. For a linear map f between finite-dimensional real inner product spaces, the positive-part product ∏_{i<d} max(1, σᵢ(f)) equals the supremum over truncations 0 ≤ k ≤ d of the top-k singular value products ∏_{i<k} σᵢ(f). This is the local volume-expansion factor counting only the expanding directions, written in the truncated-product form the covering count uses.

The compound bridge

theorem Oseledets.prod_max_one_singularValues_eq_sup_opNorm_compound {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) (n : ℕ) : ∏ i ∈ Finset.range n, max 1 ((Matrix.toEuclideanLin M).singularValues i) = (Finset.range (n + 1)).sup' ⋯ fun (k : ℕ) => ‖ExteriorNorm.compoundMatrix k M‖

The positive-part volume distortion as the maximal compound operator norm. For a square matrix M, the positive-part singular-value product ∏_{i<n} max(1, σᵢ(M)) equals the supremum over 0 ≤ k ≤ n of the operator norms of the compound matrices ‖C_k(M)‖. This is the form the Margulis–Ruelle covering count consumes (Liao–Qiu §3, Lemma 3.3): the cover of the thickened image is controlled by ‖(toEuclideanLin M)^∧‖ = max_κ ‖C_κ(M)‖, the maximal exterior-power operator norm. It bridges |det M| = ∏ σᵢ (the k = n term) with the truncated ∏ max(1, σᵢ) the count needs.

(Retained for reference: the realised sharp covering count Oseledets.coveringCount_image_ball_le_volProd of Oseledets.Entropy.Ruelle.SharpCovering reaches ∏ max(1, σᵢ) through a direct SVD ellipsoid volume bound rather than this compound-norm form, so this bridge is not on the live path.)