The Furstenberg–Kesten theorem (extremal Lyapunov exponents)

Applying Kingman's subadditive ergodic theorem to gₙ = log‖A⁽ⁿ⁾‖ (a subadditive cocycle by submultiplicativity of the operator norm) yields the top Lyapunov exponent λ₁ = lim (1/n) log‖A⁽ⁿ⁾(x)‖; applying it to the inverse cocycle gₙ = log‖(A⁽ⁿ⁾)⁻¹‖ yields the (negative of the) bottom exponent λ_k. These are the extremal cases of the Oseledets spectrum.

The proofs build the two subadditive cocycles, verify the three hypotheses of tendsto_kingman_ergodic (subadditivity, integrability of each level, bounded-below normalized means), and read off the a.e.-constant limit. The cocycle entries are required to be invertible (det ≠ 0) and both log⁺‖A‖ and log⁺‖A⁻¹‖ are required to be integrable; the second integrability hypothesis is what keeps the bounded-below proviso (hence the limit) finite in ℝ for the top exponent.

Main results

• Oseledets.furstenbergKesten_norm: for an ergodic measure-preserving T and an everywhere-invertible measurable generator A with integrable log⁺‖A‖ and log⁺‖A⁻¹‖, the normalized log norms (1/n) log‖A⁽ⁿ⁾(x)‖ converge μ-a.e. to a constant (the top Lyapunov exponent).
• Oseledets.furstenbergKesten_norm_inv: the analogous a.e. limit for the inverse cocycle (1/n) log‖(A⁽ⁿ⁾(x))⁻¹‖ (the negative of the bottom Lyapunov exponent).
• Oseledets.isSubadditiveCocycle_logNorm and Oseledets.isSubadditiveCocycle_logNorm_inv: subadditivity of the two log-norm cocycles.
• Oseledets.logNorm_cocycle_le_birkhoffSum and Oseledets.neg_birkhoffSum_le_logNorm_cocycle: Birkhoff-sum sandwich bounds, driving both the integrability and the bounded-below hypotheses.

References

• H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31 (1960), 457–469.

Positivity of the iterate norms (needs invertibility and NeZero d)

theorem Oseledets.det_cocycle_ne_zero {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (n : ℕ) (x : X) : (cocycle A T n x).det ≠ 0

det (cocycle A T n x) ≠ 0 when the generator is everywhere invertible.

theorem Oseledets.norm_cocycle_pos {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (n : ℕ) (x : X) : 0 < ‖cocycle A T n x‖

The norm of every cocycle iterate is strictly positive (needs NeZero d).

theorem Oseledets.norm_inv_cocycle_pos {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (n : ℕ) (x : X) : 0 < ‖(cocycle A T n x)⁻¹‖

The norm of every inverse cocycle iterate is strictly positive (needs NeZero d).

theorem Oseledets.norm_one_matrix {d : ℕ} [NeZero d] : ‖1‖ = 1

‖(1 : Matrix (Fin d) (Fin d) ℝ)‖ = 1 for the L2 operator norm when d ≠ 0.

Measurability of the (inverse) log-norm cocycle

theorem Oseledets.measurable_logNorm_cocycle {X : Type u_1} {T : X → X} {d : ℕ} [MeasurableSpace X] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : Measurable A) (hT : Measurable T) (n : ℕ) : Measurable fun (x : X) => Real.log ‖cocycle A T n x‖

x ↦ log‖A⁽ⁿ⁾(x)‖ is measurable.

theorem Oseledets.measurable_logNorm_inv_cocycle {X : Type u_1} {T : X → X} {d : ℕ} [MeasurableSpace X] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : Measurable A) (hT : Measurable T) (n : ℕ) : Measurable fun (x : X) => Real.log ‖(cocycle A T n x)⁻¹‖

x ↦ log‖(A⁽ⁿ⁾(x))⁻¹‖ is measurable.

Subadditivity of the two log-norm cocycles

theorem Oseledets.isSubadditiveCocycle_logNorm {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] : IsSubadditiveCocycle T fun (n : ℕ) (x : X) => Real.log ‖cocycle A T n x‖

The top subadditive cocycle. gₙ = log‖A⁽ⁿ⁾‖ is subadditive over T.

theorem Oseledets.isSubadditiveCocycle_logNorm_inv {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] : IsSubadditiveCocycle T fun (n : ℕ) (x : X) => Real.log ‖(cocycle A T n x)⁻¹‖

The bottom subadditive cocycle. gₙ = log‖(A⁽ⁿ⁾)⁻¹‖ is subadditive over T.

Birkhoff-sum sandwich bounds (drive integrability and bounded-below)

theorem Oseledets.logNorm_cocycle_le_birkhoffSum {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (n : ℕ) (x : X) : Real.log ‖cocycle A T n x‖ ≤ birkhoffSum T (fun (y : X) => ‖A y‖.posLog) n x

Upper Fekete bound: log‖A⁽ⁿ⁾(x)‖ ≤ birkhoffSum T (log⁺‖A‖) n x.

theorem Oseledets.logNorm_inv_cocycle_le_birkhoffSum {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (n : ℕ) (x : X) : Real.log ‖(cocycle A T n x)⁻¹‖ ≤ birkhoffSum T (fun (y : X) => ‖(A y)⁻¹‖.posLog) n x

Upper Fekete bound for the inverse cocycle: log‖(A⁽ⁿ⁾(x))⁻¹‖ ≤ birkhoffSum T (log⁺‖A⁻¹‖) n x.

theorem Oseledets.neg_birkhoffSum_le_logNorm_cocycle {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (n : ℕ) (x : X) : -birkhoffSum T (fun (y : X) => ‖(A y)⁻¹‖.posLog) n x ≤ Real.log ‖cocycle A T n x‖

Lower bound on the (forward) log-norm via the inverse Birkhoff sum: - birkhoffSum T (log⁺‖A⁻¹‖) n x ≤ log‖A⁽ⁿ⁾(x)‖.

Integrability of each level, and the Birkhoff integral identity

theorem Oseledets.integral_birkhoffSum {X : Type u_1} {T : X → X} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (hT : MeasureTheory.MeasurePreserving T μ μ) {f : X → ℝ} (hf : MeasureTheory.Integrable f μ) (n : ℕ) : ∫ (x : X), birkhoffSum T f n x ∂μ = n • ∫ (x : X), f x ∂μ

The integral of a Birkhoff sum equals n times the integral, for measure-preserving T (each composition with T^[k] is integral-preserving).

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

Integrability of each top level gₙ = log‖A⁽ⁿ⁾‖, by domination by the (integrable) sum of the two Birkhoff sums birkhoffSum (log⁺‖A‖) n + birkhoffSum (log⁺‖A⁻¹‖) n.

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

Integrability of each bottom level gₙ = log‖(A⁽ⁿ⁾)⁻¹‖. The inverse cocycle is the forward cocycle of the generator A⁻¹ reflected; we dominate directly by the two Birkhoff sums (the upper bound is birkhoffSum (log⁺‖A⁻¹‖) n, the lower bound comes from ‖(A⁽ⁿ⁾)⁻¹‖ · ‖A⁽ⁿ⁾‖ ≥ 1).

The two Furstenberg–Kesten theorems

theorem Oseledets.furstenbergKesten_norm {X : Type u_1} {T : X → X} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure 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)⁻¹) μ) : ∃ (lam : ℝ), ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖cocycle A T n x‖) Filter.atTop (nhds lam)

Furstenberg–Kesten, top exponent. For an ergodic measure-preserving T, an everywhere-invertible measurable cocycle generator with log⁺‖A‖, log⁺‖A⁻¹‖ ∈ L¹, the normalized log operator norm of the cocycle converges μ-a.e. to a constant λ₁ (the top Lyapunov exponent).

theorem Oseledets.furstenbergKesten_norm_inv {X : Type u_1} {T : X → X} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure 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)⁻¹) μ) : ∃ (lam : ℝ), ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(cocycle A T n x)⁻¹‖) Filter.atTop (nhds lam)

Furstenberg–Kesten, bottom exponent. With the additional log⁺‖A⁻¹‖ ∈ L¹ hypothesis (so the cocycle is in GL), the normalized log norm of the inverse cocycle converges μ-a.e. to a constant; equivalently the bottom Lyapunov exponent λ_k = -lim (1/n) log‖A⁽ⁿ⁾(x)⁻¹‖ exists and is finite.