The exterior (wedge) cocycle and the growth-rate characterization

This module is purely additive on top of the spectrum object Oseledets.exponents : Fin d → ℝ and the partial sums Oseledets.gammaK (Γ_k), 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 μ]).

It realizes the exterior / wedge characterization of the partial sums of Lyapunov exponents. Three layers:

• The exterior cocycle is a cocycle. For each k, the k-th compound (exterior power) ExteriorNorm.compoundMatrix k (A ·) generates a matrix cocycle, and its iterate is the compound of the iterate: cocycle (extGen k A) T n x = compoundMatrix k (cocycle A T n x) (cocycle_extGen_eq_compound). This is precisely Cauchy–Binet (ExteriorNorm.compoundMatrix_mul) packaged dynamically.
• The k-volume growth rate. For μ-a.e. x, (1/n) log ‖compoundMatrix k (cocycle A T n x)‖ → Γ_k (tendsto_log_opNorm_compound_cocycle). The operator norm ‖compoundMatrix k (cocycle A T n x)‖ is exactly the product of the top-k singular values (ExteriorNorm.prod_singularValues_eq_l2_opNorm_compound), i.e. the norm of the largest k × k minor block — the k-dimensional volume growth rate. We take the scalar route (rewriting through sprod), which avoids re-establishing Furstenberg–Kesten integrability for the compound generator.
• The positive-exponent sum as a maximal partial sum. Since the partial sums Γ_k = ∑_{i<k} exponents i are partial sums of the antitone sequence exponents, they are maximized exactly at k₊ = #{i | 0 < exponents i}, the number of positive exponents. Hence sumPosExp = Γ_{k₊} (sumPosExp_eq_gammaK_card_pos).

Main definitions

• Oseledets.extGen — the k-th exterior (compound) cocycle generator x ↦ compoundMatrix k (A x).

Main results

• Oseledets.cocycle_extGen_eq_compound — the exterior power of the cocycle is the cocycle of the exterior power (Cauchy–Binet, packaged dynamically).
• Oseledets.tendsto_log_opNorm_compound_cocycle — the k-volume / largest-minor growth rate equals Γ_k.
• Oseledets.gammaK_eq_sum_top_exponents (re-exported from ExponentSums) — Γ_k is the sum of the top-k exponents.
• Oseledets.gammaK_one_eq_topExponent — Γ_1 is the top Lyapunov exponent.
• Oseledets.sumPosExp_eq_gammaK_card_pos — the positive-exponent sum is the partial sum at the number of positive exponents, i.e. the maximal partial sum.

Implementation notes

The compound generator extGen k A has values in the ⋀^k-finrank-indexed square matrices Matrix (Fin (finrank ℝ (⋀[ℝ]^k (EuclideanSpace ℝ (Fin d))))) … ℝ; the cocycle machinery (cocycle, cocycle_succ, cocycle_one) is generic over the matrix index type, so it applies verbatim.

The Furstenberg–Kesten-on-the-compound-generator route (feeding extGen k A to the top-exponent FK theorem) is not used and not required: it would demand its own integrability bound log⁺‖C_k(A)‖ ≤ k · log⁺‖A‖ + C. The scalar route through sprod is far cheaper and is what we use here. The cocycle structure (cocycle_extGen_eq_compound) is nonetheless proved, since it is the conceptual content of "the wedge of the cocycle is a cocycle".

References

• M. S. Raghunathan, A proof of Oseledec's multiplicative ergodic theorem, Israel J. Math. 32 (1979), 356–362.
• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

The exterior (compound) cocycle generator

noncomputable def Oseledets.extGen {X : Type u_1} {d : ℕ} (k : ℕ) (A : X → Matrix (Fin d) (Fin d) ℝ) : X → Matrix (Fin (Module.finrank ℝ ↥(⋀[ℝ]^k (EuclideanSpace ℝ (Fin d))))) (Fin (Module.finrank ℝ ↥(⋀[ℝ]^k (EuclideanSpace ℝ (Fin d))))) ℝ

The k-th exterior (compound) cocycle generator. It sends x to the k-th compound matrix C_k(A x) (whose entries are the k × k minors of A x). Its iterated cocycle is the compound of the iterated cocycle — see cocycle_extGen_eq_compound.

Equations

• Oseledets.extGen k A x = Oseledets.ExteriorNorm.compoundMatrix k (A x)

theorem Oseledets.cocycle_extGen_eq_compound {X : Type u_1} {d : ℕ} {T : X → X} (k : ℕ) (A : X → Matrix (Fin d) (Fin d) ℝ) (n : ℕ) (x : X) : cocycle (extGen k A) T n x = ExteriorNorm.compoundMatrix k (cocycle A T n x)

The exterior power of the cocycle is the cocycle of the exterior power. The iterate of the compound cocycle generator equals the compound of the cocycle iterate: cocycle (extGen k A) T n x = C_k(cocycle A T n x).

This is Cauchy–Binet (ExteriorNorm.compoundMatrix_mul) packaged dynamically: induction on n with compoundMatrix_one for the base and compoundMatrix_mul for the step. It shows that the k-th exterior power of a matrix cocycle is itself a matrix cocycle.

The k-volume / largest-minor growth rate

theorem Oseledets.tendsto_log_opNorm_compound_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)⁻¹) μ) {k : ℕ} (hk : k ≤ d) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖ExteriorNorm.compoundMatrix k (cocycle A T n x)‖) Filter.atTop (nhds (gammaK hT hA hAmeas hint hint' hk))

The k-volume growth rate equals Γ_k. For μ-a.e. x, (1/n) log ‖C_k(cocycle A T n x)‖ → Γ_k. The operator norm of the compound matrix is the product of the top-k singular values (ExteriorNorm.prod_singularValues_eq_l2_opNorm_compound), i.e. the largest k × k minor growth / k-dimensional volume growth; its growth rate is the partial sum Γ_k of the top-k Lyapunov exponents.

We rewrite ‖C_k(cocycle A T n x)‖ = sprod_k and apply gammaK_tendsto (the scalar route), avoiding any Furstenberg–Kesten integrability bound for the compound generator.

theorem Oseledets.gammaK_one_eq_topExponent {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)⁻¹) μ) (h1 : 1 ≤ d) : gammaK hT hA hAmeas hint hint' h1 = topExponent hT hA hAmeas hint hint'

Γ_1 is the top Lyapunov exponent. The first partial sum Γ_1 = ∑_{i<1} exponents i equals exponents 0 = topExponent.

The positive-exponent sum as a maximal partial sum

theorem Oseledets.sumPosExp_eq_gammaK_card_pos {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)⁻¹) μ) (hk : {i : Fin d | 0 < exponents hT hA hAmeas hint hint' i}.card ≤ d) : sumPosExp hT hA hAmeas hint hint' = gammaK hT hA hAmeas hint hint' hk

The positive-exponent sum is the maximal partial sum. Writing k₊ = #{i | 0 < exponents i} for the number of strictly positive Lyapunov exponents, the sum of the positive exponents equals the partial sum Γ_{k₊} = ∑_{i<k₊} exponents i.

Since exponents is antitone, its strictly positive entries are exactly the top k₊ indices, so the filtered positive sum coincides with the top-k₊ prefix sum, which is Γ_{k₊} by gammaK_eq_sum_top_exponents. Equivalently, among all partial sums Γ_k of the antitone sequence exponents, the maximum is attained exactly at k = k₊ (adding any non-positive exponent does not increase the sum).