The non-ergodic Lyapunov spectrum (exponents as invariant functions)

This module is the non-ergodic relaxation of the singular-value layer. In the ergodic theory (Oseledets.tendsto_gammaK, Oseledets.exists_lam_tendsto_singularValue, Oseledets.exponents) the partial-sum limits Γ_k and the per-σ Lyapunov exponents λᵢ = Γ_{i+1} − Γ_i are almost-everywhere constants. Without ergodicity these limits still exist almost everywhere, but they are now T-invariant measurable functions rather than constants. (Heuristically the limit is the conditional expectation μ[log sprod_k(·, 1) | invariants T]; the theorems below prove only its existence, T-invariance, and integrability — not that identification.)

The whole development is a mechanical re-derivation swapping the ergodic Kingman theorem (Oseledets.tendsto_kingman_ergodic) for the non-ergodic one (Oseledets.tendsto_kingman): the latter produces a T-invariant integrable limit G instead of a constant c. Every integrability / positivity / subadditivity fact about log sprod_k that the ergodic proof discharged (integrable_logSprod, bddBelow_logSprod, sprod_pos, isSubadditiveCocycle_logSprod) is reused verbatim — only the Ergodic hypothesis is dropped in favour of bare MeasurePreserving. The pointwise telescoping that turns the Γ_k limits into per-σ exponents (tendsto_log_singularValue) is unchanged.

The ergodic results are recovered as the special case where the σ-algebra of T-invariants is trivial (so each invariant function is a.e. constant): see Oseledets.tendsto_gammaK_of_integrableLogNorm and Oseledets.exists_lam_tendsto_singularValue.

Main results

• Oseledets.tendsto_gammaK_nonergodic — the partial-sum limit Γ_k as a T-invariant integrable function G : X → ℝ, with (1/n) log sprod_k → G almost everywhere.
• Oseledets.exists_exponents_nonergodic — the full Lyapunov spectrum as a family of T-invariant integrable functions lam : ℕ → X → ℝ, each the a.e. limit of (1/n) log σᵢ(A⁽ⁿ⁾).
• Oseledets.exists_sumPosExp_nonergodic — the sum of the positive exponents, as a T-invariant integrable function obtained by summing the positive part of the spectrum.

References

• L. Arnold, Random Dynamical Systems, Springer Monographs in Mathematics, 1998.
• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

theorem Oseledets.tendsto_gammaK_nonergodic {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] [NeZero d] (hmp : MeasureTheory.MeasurePreserving 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) : ∃ (G : X → ℝ), G ∘ T =ᵐ[μ] G ∧ MeasureTheory.Integrable G μ ∧ ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (sprod A T k n x)) Filter.atTop (nhds (G x))

The non-ergodic partial-sum limit Γ_k. For a measure-preserving T, an everywhere-invertible measurable cocycle generator with log⁺‖A‖, log⁺‖A⁻¹‖ ∈ L¹, and k ≤ d, the normalized log sprod_k converges μ-a.e. to a T-invariant integrable function G (no ergodicity assumed). This is the non-ergodic analogue of tendsto_gammaK_of_integrableLogNorm: the constant Γ_k is replaced by the invariant function G.

theorem Oseledets.exists_exponents_nonergodic {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] [NeZero d] (hmp : MeasureTheory.MeasurePreserving 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)⁻¹) μ) : ∃ (lam : ℕ → X → ℝ), (∀ (i : ℕ), lam i ∘ T =ᵐ[μ] lam i) ∧ (∀ (i : ℕ), MeasureTheory.Integrable (lam i) μ) ∧ ∀ i < d, ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues i)) Filter.atTop (nhds (lam i x))

The non-ergodic Lyapunov spectrum. For a measure-preserving T, an everywhere-invertible measurable cocycle generator with log⁺‖A‖, log⁺‖A⁻¹‖ ∈ L¹, there is a family of T-invariant integrable functions lam : ℕ → X → ℝ (supported on [0, d)) such that, for each i < d and μ-a.e. x, the normalized log of the i-th singular value of A⁽ⁿ⁾ converges to lam i x. Without ergodicity the exponents are invariant measurable functions instead of the constants of exists_lam_tendsto_singularValue.

The functions are built as σ-differences lam i = G_{i+1} − G_i of the partial-sum limits of tendsto_gammaK_nonergodic; the per-σ telescoping (tendsto_log_singularValue) is the same pointwise argument used in the ergodic case.

theorem Oseledets.exists_sumPosExp_nonergodic {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] [NeZero d] (hmp : MeasureTheory.MeasurePreserving 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)⁻¹) μ) : ∃ (lam : ℕ → X → ℝ) (Gpos : X → ℝ), Gpos ∘ T =ᵐ[μ] Gpos ∧ MeasureTheory.Integrable Gpos μ ∧ (∀ (x : X), Gpos x = ∑ i ∈ Finset.range d, max (lam i x) 0) ∧ ∀ i < d, ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues i)) Filter.atTop (nhds (lam i x))

The non-ergodic sum of positive exponents. Summing the positive parts max (lam i x) 0 of the non-ergodic spectrum over i < d yields a single T-invariant integrable function G₊ : X → ℝ, the non-ergodic analogue of lyapPosSum. (Without ergodicity this is an invariant function, not a constant.)