Linear cocycles over a measure-preserving system

This file sets up the basic object of the Oseledets multiplicative ergodic theorem: the iterated linear cocycle generated by a matrix-valued map A : X → Matrix (Fin d) (Fin d) ℝ over a self-map T : X → X.

We use the convention that the newest factor is on the left: cocycle A T 0 x = 1 and cocycle A T (n+1) x = cocycle A T n (T x) * A x, so that cocycle A T n x = A (T^[n-1] x) * ⋯ * A (T x) * A x. With this convention the cocycle identity reads cocycle A T (m + n) x = cocycle A T m (T^[n] x) * cocycle A T n x.

The matrix norm is the (scoped) L2 operator norm Matrix.Norms.L2Operator, which is submultiplicative; vectors live in EuclideanSpace ℝ (Fin d) and the action is via Matrix.toEuclideanCLM.

Main definitions

• Oseledets.cocycle: the iterated linear cocycle generated by A over T.
• Oseledets.IntegrableLogNorm: the one-sided integrability hypothesis log⁺ ‖A‖ ∈ L¹(μ).
• Oseledets.instMeasurableSpaceMatrix: the entrywise (Pi) measurable structure on matrices.

Main results

• Oseledets.cocycle_add: the cocycle identity cocycle A T (m + n) x = cocycle A T m (T^[n] x) * cocycle A T n x.
• Oseledets.measurable_cocycle: each iterate of the cocycle is measurable when the generator A and the dynamics T are.

@[implicit_reducible]

instance Oseledets.instMeasurableSpaceMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [MeasurableSpace α] : MeasurableSpace (Matrix m n α)

The (entrywise) Pi measurable structure on matrices, induced from the entry type α. A matrix is a function m → n → α, and this is the natural σ-algebra for matrix-valued maps (for finitely many entries over a Borel α, it agrees with the Borel σ-algebra). Mathlib does not yet register this instance because Matrix is a def, not reducibly the Pi type, so the ambient Pi instance does not transfer.

Equations

• Oseledets.instMeasurableSpaceMatrix = Oseledets.instMeasurableSpaceMatrix._aux_1

noncomputable def Oseledets.cocycle {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) : ℕ → X → Matrix (Fin d) (Fin d) ℝ

The iterated linear cocycle generated by A over T, newest factor on the left.

cocycle A T 0 x = 1, cocycle A T (n + 1) x = cocycle A T n (T x) * A x.

Equations

• Oseledets.cocycle A T 0 x✝ = 1
• Oseledets.cocycle A T n.succ x✝ = Oseledets.cocycle A T n (T x✝) * A x✝

@[simp]

theorem Oseledets.cocycle_zero {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) : cocycle A T 0 x = 1

theorem Oseledets.cocycle_succ {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) : cocycle A T (n + 1) x = cocycle A T n (T x) * A x

@[simp]

theorem Oseledets.cocycle_one {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) : cocycle A T 1 x = A x

theorem Oseledets.cocycle_add {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (m n : ℕ) (x : X) : cocycle A T (m + n) x = cocycle A T m (T^[n] x) * cocycle A T n x

The cocycle identity A⁽ᵐ⁺ⁿ⁾(x) = A⁽ᵐ⁾(Tⁿ x) · A⁽ⁿ⁾(x).

def Oseledets.IntegrableLogNorm {X : Type u_1} {d : ℕ} [MeasurableSpace X] (A : X → Matrix (Fin d) (Fin d) ℝ) (μ : MeasureTheory.Measure X) : Prop

The one-sided integrability hypothesis: log⁺‖A‖ ∈ L¹(μ).

Equations

• Oseledets.IntegrableLogNorm A μ = MeasureTheory.Integrable (fun (x : X) => ‖A x‖.posLog) μ

instance Oseledets.instMeasurableMul₂Matrix {m : Type u_2} {α : Type u_3} [Fintype m] [MeasurableSpace α] [NonUnitalNonAssocSemiring α] [MeasurableMul₂ α] [MeasurableAdd₂ α] : MeasurableMul₂ (Matrix m m α)

Matrix multiplication on Matrix m m α is measurable in both arguments jointly. Each entry of a product is the finite sum (A * B) i j = ∑ k, A i k * B k j (Matrix.mul_apply), and the entry-coordinate projections are measurable because the matrix space carries the Pi measurable structure (instMeasurableSpaceMatrix).

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

Measurability of each iterate of the cocycle, given a measurable generator.