The top Lyapunov exponent of an arbitrary constant cocycle

The companion module Oseledets.Lyapunov.Extensions.ConstantCocycle identifies the full Lyapunov spectrum of a constant cocycle only in the symmetric case (exponents_const, for Mᵀ = M). This module removes the symmetry hypothesis for the top exponent: for an arbitrary real matrix M, the top Lyapunov exponent of the constant cocycle x ↦ M is the logarithm of the spectral radius of M, i.e. the log of the maximal modulus of an eigenvalue of M taken over ℂ.

The route is Gelfand's formula. The top exponent of the constant cocycle is lim_n (1/n) log ‖Mⁿ‖ (the operator-norm growth rate, recovered from the top singular value of the cocycle iterate). By Gelfand's formula in the complex Banach algebra Matrix (Fin d) (Fin d) ℂ (with its L2 operator norm), ‖(M_ℂ)ⁿ‖^{1/n} converges to the spectral radius of the complexification M_ℂ = M.map (algebraMap ℝ ℂ). The L2 operator norm is preserved by complexification (Oseledets.l2_opNorm_map_ofReal), so the real growth rate is exactly the log of spectralRadius ℂ M_ℂ.

Main results

• Oseledets.l2_opNorm_map_ofReal — the L2 operator norm of a real matrix equals the L2 operator norm of its complexification M.map (algebraMap ℝ ℂ).
• Oseledets.tendsto_pow_norm_one_div_spectralRadius — ‖Mⁿ‖^{1/n} → (spectralRadius ℂ M_ℂ).toReal.
• Oseledets.tendsto_log_opNorm_pow_log_spectralRadius — (1/n) log ‖Mⁿ‖ → Real.log (spectralRadius ℂ M_ℂ).toReal.
• Oseledets.topExponent_constantCocycle_eq_log_spectralRadius — for ergodic T and an invertible (not necessarily symmetric) M, the top Lyapunov exponent of the constant cocycle equals Real.log (spectralRadius ℂ M_ℂ).toReal.

References

• I. M. Gelfand, Normierte Ringe, Mat. Sb. 9 (1941), 3–24.
• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

Complexification preserves the L2 operator norm

theorem Oseledets.l2_opNorm_map_ofReal {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) : ‖M.map ⇑(algebraMap ℝ ℂ)‖ = ‖M‖

Complexification preserves the L2 operator norm. For a real square matrix M, the L2 operator norm of M equals the L2 operator norm of its complexification M_ℂ = M.map (algebraMap ℝ ℂ).

For z : EuclideanSpace ℂ (Fin d) with real/imaginary parts the real vectors u, v (u i = (z i).re, v i = (z i).im), the i-th coordinate of M_ℂ *ᵥ z is (M *ᵥ u) i + (M *ᵥ v) i • I (since M is real), so ‖(M_ℂ *ᵥ z) i‖² = (M *ᵥ u) i² + (M *ᵥ v) i² and summing gives ‖M_ℂ z‖² = ‖M u‖² + ‖M v‖² ≤ ‖M‖²(‖u‖² + ‖v‖²) = ‖M‖² ‖z‖²; the reverse inequality is the restriction to real vectors.

Finiteness and positivity of the spectral radius

theorem Oseledets.map_ofReal_pow {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) (n : ℕ) : (M ^ n).map ⇑(algebraMap ℝ ℂ) = M.map ⇑(algebraMap ℝ ℂ) ^ n

The complexification of a real matrix power is the power of the complexification: (Mⁿ).map (algebraMap ℝ ℂ) = (M.map (algebraMap ℝ ℂ))ⁿ.

theorem Oseledets.spectralRadius_map_ofReal_ne_top {d : ℕ} [NeZero d] (M : Matrix (Fin d) (Fin d) ℝ) : spectralRadius ℂ (M.map ⇑(algebraMap ℝ ℂ)) ≠ ⊤

For a real matrix with d ≠ 0, the complex spectral radius of the complexification is finite (bounded by the norm; the complex matrix algebra is a nontrivial CStarRing, hence a NormOneClass).

theorem Oseledets.spectrum_map_ofReal_nonempty {d : ℕ} [NeZero d] (M : Matrix (Fin d) (Fin d) ℝ) : (spectrum ℂ (M.map ⇑(algebraMap ℝ ℂ))).Nonempty

For a real square matrix with d ≠ 0, the complexification has nonempty spectrum over ℂ.

theorem Oseledets.spectralRadius_map_ofReal_pos {d : ℕ} [NeZero d] {M : Matrix (Fin d) (Fin d) ℝ} (hdet : M.det ≠ 0) : 0 < (spectralRadius ℂ (M.map ⇑(algebraMap ℝ ℂ))).toReal

For an invertible real matrix M (with d ≠ 0), the complex spectral radius of the complexification is strictly positive: every spectral value is nonzero (0 ∉ spectrum, as M_ℂ is a unit), and the spectral radius is attained at one such value.

The Gelfand limit for the L2 operator norm of a real matrix

theorem Oseledets.tendsto_pow_norm_one_div_spectralRadius {d : ℕ} [NeZero d] (M : Matrix (Fin d) (Fin d) ℝ) : Filter.Tendsto (fun (n : ℕ) => ‖M ^ n‖ ^ (1 / ↑n)) Filter.atTop (nhds (spectralRadius ℂ (M.map ⇑(algebraMap ℝ ℂ))).toReal)

Gelfand's formula for a real matrix (L2 operator norm). For any real square matrix M, ‖Mⁿ‖^{1/n} → (spectralRadius ℂ M_ℂ).toReal, where M_ℂ = M.map (algebraMap ℝ ℂ). Obtained from Gelfand's formula in the complex Banach algebra Matrix (Fin d) (Fin d) ℂ (spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius), transported to the real norm via l2_opNorm_map_ofReal (complexification preserves the L2 operator norm).

theorem Oseledets.tendsto_log_opNorm_pow_log_spectralRadius {d : ℕ} [NeZero d] {M : Matrix (Fin d) (Fin d) ℝ} (hdet : M.det ≠ 0) : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖M ^ n‖) Filter.atTop (nhds (Real.log (spectralRadius ℂ (M.map ⇑(algebraMap ℝ ℂ))).toReal))

The log-norm growth rate of a real matrix is the log spectral radius. For an invertible real matrix M (with d ≠ 0), (1/n) log ‖Mⁿ‖ → Real.log (spectralRadius ℂ M_ℂ).toReal. This is the logarithm of tendsto_pow_norm_one_div_spectralRadius, valid because the spectral radius is strictly positive (spectralRadius_map_ofReal_pos).

The top Lyapunov exponent of a constant cocycle

theorem Oseledets.topExponent_constantCocycle_eq_log_spectralRadius {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] [NeZero d] (hT : Ergodic T μ) {M : Matrix (Fin d) (Fin d) ℝ} (hdet : M.det ≠ 0) : topExponent hT ⋯ ⋯ ⋯ ⋯ = Real.log (spectralRadius ℂ (M.map ⇑(algebraMap ℝ ℂ))).toReal

The top Lyapunov exponent of an arbitrary constant cocycle is the log spectral radius. For an ergodic, probability-preserving (X, μ, T) and any real square matrix M with d ≠ 0 and det M ≠ 0 (no symmetry assumption), the top Lyapunov exponent of the constant cocycle x ↦ M equals Real.log of the spectral radius of M, i.e. the log of the maximal modulus of an eigenvalue of M taken over ℂ.

The top exponent exponents … 0 is the a.e. limit of (1/n) log σ₀(toEuclideanLin Mⁿ) (exponents_tendsto_log_singularValue at index 0), and σ₀(toEuclideanLin Mⁿ) = ‖Mⁿ‖ (top_singularValue_eq_opNorm), so a.e. (1/n) log ‖Mⁿ‖ → topExponent. This deterministic sequence also tends to log (spectralRadius ℂ M_ℂ).toReal by Gelfand's formula (tendsto_log_opNorm_pow_log_spectralRadius); uniqueness of limits closes the gap.