The trace/determinant identity: sum of all Lyapunov exponents = ∫ log|det|

This module is purely additive on top of the spectrum object Oseledets.exponents : Fin d → ℝ and the telescoping growth rate Oseledets.gammaK (both in Oseledets/Lyapunov/ExponentSums.lean / Spectrum.lean). It proves the classical determinant identity of multiplicative ergodic theory: under the standing hypotheses (hT : Ergodic T μ, hA : ∀ x, (A x).det ≠ 0, hAmeas : Measurable A, hint : IntegrableLogNorm A μ, hint' : IntegrableLogNorm (fun x => (A x)⁻¹) μ, together with [IsProbabilityMeasure μ]), the sum of all Lyapunov exponents (counted with multiplicity) equals the integral of log|det| of the generator:

∑ i, exponents i = ∫ x, log |(A x).det| ∂μ.

The proof is the standard composition:

1. Volume = product of all singular values. The product of all d singular values of a matrix equals the absolute value of its determinant: sprod A T d n x = |det(A⁽ⁿ⁾)|. This is proved via the squared-singular-value/Gram-eigenvalue bridge (sq_singularValues_eq_gram_eigenvalue) and det = ∏ eigenvalues for the symmetric Gram operator (LinearMap.IsSymmetric.det_eq_prod_eigenvalues): sprod_d² = det(MᵀM) = (det M)², hence sprod_d = |det M|.
2. log|det| is an additive (Birkhoff) cocycle. Because det is multiplicative (Matrix.det_mul), log|det(A⁽ⁿ⁾)| = ∑_{k<n} log|det(A(Tᵏx))|, i.e. the exact Birkhoff sum of log|det A| (the equality analogue of the submultiplicative log-norm sandwich).
3. Birkhoff ergodic theorem. (1/n) log|det(A⁽ⁿ⁾)| → ∫ log|det A| μ-a.e., using that log|det A| is integrable (it equals log sprod_d at n = 1, integrable by integrable_logSprod).
4. Telescoping at k = d. The same normalized quantity also converges to Γ_d = ∑ i, exponents i (gammaK_eq_sum_top_exponents). Uniqueness of limits gives the identity.

Main results

• Oseledets.sprod_d_eq_abs_det — product of all singular values = |det|.
• Oseledets.integrable_log_abs_det — log|det A| ∈ L¹(μ).
• Oseledets.log_abs_det_cocycle_eq_birkhoffSum — log|det(A⁽ⁿ⁾)| is the Birkhoff sum of log|det A|.
• Oseledets.tendsto_log_abs_det_cocycle — (1/n) log|det(A⁽ⁿ⁾)| → ∑ i, exponents i a.e.
• Oseledets.sumAllExp_eq_integral_log_abs_det — the determinant identity ∑ i, exponents i = ∫ x, log |(A x).det| ∂μ.
• Oseledets.tendsto_abs_det_cocycle_atTop_zero — volume contraction: if the sum of all exponents is negative, then |det(A⁽ⁿ⁾)| → 0 μ-a.e.

References

• D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58.
• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

Step 1: the product of all singular values is the absolute determinant

theorem Oseledets.det_toEuclideanLin {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) : LinearMap.det (Matrix.toEuclideanLin M) = M.det

The determinant as a linear map equals the matrix determinant for toEuclideanLin. toEuclideanLin is Matrix.toLin for the standard orthonormal basis, so the determinant of the associated endomorphism is the matrix determinant (LinearMap.det_toLin).

theorem Oseledets.sprod_d_eq_abs_det {X : Type u_1} {d : ℕ} [NeZero d] {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} (n : ℕ) (x : X) : sprod A T d n x = |(cocycle A T n x).det|

Product of all singular values = |det| (deterministic, every n, x). The product of all d singular values of the cocycle iterate equals the absolute value of its determinant. Proof: square it, use σᵢ² = eigenvalue_i(MᵀM) (sq_singularValues_eq_gram_eigenvalue) and det = ∏ eigenvalues for the symmetric Gram operator, giving sprod_d² = det(MᵀM) = (det M)²; then take the (nonnegative) square root. No invertibility is required: the identity holds for every matrix (both sides are nonnegative and have equal squares).

Step 2: log|det(A⁽ⁿ⁾)| is the Birkhoff sum of log|det A|

theorem Oseledets.log_abs_det_cocycle_eq_birkhoffSum {X : Type u_1} {d : ℕ} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (n : ℕ) (x : X) : Real.log |(cocycle A T n x).det| = birkhoffSum T (fun (y : X) => Real.log |(A y).det|) n x

log|det(A⁽ⁿ⁾)| is an additive (Birkhoff) cocycle. Since det is multiplicative (Matrix.det_mul), the log of the absolute determinant of the cocycle iterate is exactly the Birkhoff sum of log|det A| (the equality analogue of the submultiplicative log-norm sandwich logNorm_cocycle_le_birkhoffSum).

Step 3: integrability of log|det A|

theorem Oseledets.integrable_log_abs_det {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) [MeasureTheory.IsFiniteMeasure μ] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : MeasureTheory.Integrable (fun (x : X) => Real.log |(A x).det|) μ

log|det A| ∈ L¹(μ). Identifying |det A| with the product of all singular values of A (sprod A T d 1 = |det(A⁽¹⁾)| = |det A|), integrability follows from the integrability of log sprod_d (integrable_logSprod at k = d, n = 1), which is dominated by the two Furstenberg–Kesten log-norm cocycles d·(log⁺‖A‖ + log⁺‖A⁻¹‖).

Step 4: the a.e. growth limit and the determinant identity

theorem Oseledets.tendsto_log_abs_det_cocycle {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log |(cocycle A T n x).det|) Filter.atTop (nhds (sumAllExp hT hA hAmeas hint hint'))

The a.e. determinant growth limit. For μ-a.e. x, the normalized log absolute determinant of the cocycle iterate converges to the sum of all Lyapunov exponents: (1/n) log|det(A⁽ⁿ⁾)| → ∑ i, exponents i. Two ingredients: the Birkhoff a.e. limit of the additive cocycle log|det A| (which is ∫ log|det A|) and the telescoping growth rate Γ_d = ∑ i, exponents i (gammaK), tied together via sprod_d = |det|. This route identifies the limit as the exponent sum; the value ∫ log|det A| is recorded in sumAllExp_eq_integral_log_abs_det.

theorem Oseledets.sumAllExp_eq_integral_log_abs_det {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : sumAllExp hT hA hAmeas hint hint' = ∫ (x : X), Real.log |(A x).det| ∂μ

The determinant identity. The sum of all Lyapunov exponents (counted with multiplicity) equals the integral of log|det| of the generator: ∑ i, exponents i = ∫ x, log |(A x).det| ∂μ. Proved by identifying the two a.e. limits of (1/n) log|det(A⁽ⁿ⁾)|: the Birkhoff limit ∫ log|det A| (via log_abs_det_cocycle_eq_ birkhoffSum + the ergodic Birkhoff theorem) and the exponent sum (tendsto_log_abs_det_ cocycle); uniqueness of limits closes the identity.

Volume contraction corollary

theorem Oseledets.tendsto_abs_det_cocycle_atTop_zero {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) (hneg : sumAllExp hT hA hAmeas hint hint' < 0) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => |(cocycle A T n x).det|) Filter.atTop (nhds 0)

Volume contraction. If the sum of all Lyapunov exponents is negative, then for μ-a.e. x the absolute determinant (the volume-scaling factor) of the cocycle iterate tends to 0: |det(A⁽ⁿ⁾)| → 0. Since (1/n) log|det(A⁽ⁿ⁾)| → ∑ exp < 0, the log absolute determinant tends to -∞, so its exponential tends to 0.