Measure-preserving flows and continuous-time linear cocycles

This file lays the foundation for a continuous-flow version of the Oseledets multiplicative ergodic theorem (MET). The discrete-time MET is stated over a single measure-preserving self-map T : X → X; the continuous-time version replaces T by a measure-preserving one-parameter flow φ : ℝ → X → X and the iterated matrix cocycle by a continuous-time linear cocycle A : ℝ → X → Matrix (Fin d) (Fin d) ℝ.

No topology on X is assumed: the flow is only required to be a measurable group action of (ℝ, +) that preserves the measure μ, and the cocycle is only required to be measurable in the state for each fixed time.

Main definitions

• Oseledets.MeasurePreservingFlow: a measure-preserving one-parameter flow.
• Oseledets.FlowCocycle: a continuous-time linear cocycle over such a flow, valued in d × d real matrices with the newest factor on the left (matching Oseledets.cocycle).

Main results

• Oseledets.MeasurePreservingFlow.natCast_eq_iterate: at integer times the flow is the iterate of its time-1 map, φ (n : ℝ) = (φ 1)^[n].
• Oseledets.FlowCocycle.toCocycle_eq: the reduction identity. At integer times the continuous-time cocycle agrees with the discrete iterated cocycle generated by its time-1 map over the time-1 flow, A (n : ℝ) x = cocycle (A 1 ·) (φ 1) n x. This reduces the continuous MET at integer times to the discrete MET.

structure Oseledets.MeasurePreservingFlow {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) : Type u_1

A measure-preserving one-parameter flow on the measurable space X for the measure μ: a measurable action of the additive group (ℝ, +) that preserves μ. No topology on X is assumed.

The fields encode φ 0 = id, φ (s + t) = φ s ∘ φ t, and that each time-t map is measure-preserving.

• toFun : ℝ → X → X

  The underlying time-indexed family of self-maps t ↦ φ t.

• map_zero' : self.toFun 0 = id

  The time-zero map is the identity.

• map_add' (s t : ℝ) : self.toFun (s + t) = self.toFun s ∘ self.toFun t

  The flow is additive: φ (s + t) = φ s ∘ φ t.

• measurePreserving' (t : ℝ) : MeasureTheory.MeasurePreserving (self.toFun t) μ μ

  Every time-t map preserves the measure μ.

@[implicit_reducible]

instance Oseledets.MeasurePreservingFlow.instCoeFunForallRealForall {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} : CoeFun (MeasurePreservingFlow μ) fun (x : MeasurePreservingFlow μ) => ℝ → X → X

Equations

• Oseledets.MeasurePreservingFlow.instCoeFunForallRealForall = { coe := Oseledets.MeasurePreservingFlow.toFun }

@[simp]

theorem Oseledets.MeasurePreservingFlow.map_zero {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) : φ.toFun 0 = id

The time-zero map of the flow is the identity.

@[simp]

theorem Oseledets.MeasurePreservingFlow.apply_zero {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (x : X) : φ.toFun 0 x = x

The time-zero map of the flow fixes every point.

theorem Oseledets.MeasurePreservingFlow.map_add {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (s t : ℝ) : φ.toFun (s + t) = φ.toFun s ∘ φ.toFun t

The flow is additive in time: φ (s + t) = φ s ∘ φ t.

theorem Oseledets.MeasurePreservingFlow.apply_add {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (s t : ℝ) (x : X) : φ.toFun (s + t) x = φ.toFun s (φ.toFun t x)

Pointwise additivity in time: φ (s + t) x = φ s (φ t x).

theorem Oseledets.MeasurePreservingFlow.measurePreserving {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (t : ℝ) : MeasureTheory.MeasurePreserving (φ.toFun t) μ μ

Every time-t map of the flow preserves the measure μ.

theorem Oseledets.MeasurePreservingFlow.measurable {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (t : ℝ) : Measurable (φ.toFun t)

Every time-t map of the flow is measurable.

theorem Oseledets.MeasurePreservingFlow.natCast_eq_iterate {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (n : ℕ) : φ.toFun ↑n = (φ.toFun 1)^[n]

At integer times the flow is the iterate of its time-1 map: φ (n : ℝ) = (φ 1)^[n].

structure Oseledets.FlowCocycle {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (d : ℕ) : Type u_1

A continuous-time linear cocycle over a measure-preserving flow φ, valued in d × d real matrices, with the newest factor on the left (matching Oseledets.cocycle).

The fields encode A 0 x = 1, the cocycle identity A (t + s) x = A t (φ s x) * A s x, invertibility of each A t x, and measurability of each time-t map A t.

• toFun : ℝ → X → Matrix (Fin d) (Fin d) ℝ

  The underlying time-indexed family of matrix-valued maps t ↦ A t.

• map_zero' (x : X) : self.toFun 0 x = 1

  The time-zero cocycle is the identity matrix.

• cocycle' (s t : ℝ) (x : X) : self.toFun (t + s) x = self.toFun t (φ.toFun s x) * self.toFun s x

  The cocycle identity, newest factor on the left: A (t + s) x = A t (φ s x) * A s x.

• det_ne_zero' (t : ℝ) (x : X) : (self.toFun t x).det ≠ 0

  Each cocycle matrix is invertible.

• measurable' (t : ℝ) : Measurable (self.toFun t)

  Each time-t map of the cocycle is measurable.

@[implicit_reducible]

instance Oseledets.FlowCocycle.instCoeFunForallRealForallMatrixFin {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {φ : MeasurePreservingFlow μ} : CoeFun (FlowCocycle φ d) fun (x : FlowCocycle φ d) => ℝ → X → Matrix (Fin d) (Fin d) ℝ

Equations

• Oseledets.FlowCocycle.instCoeFunForallRealForallMatrixFin = { coe := Oseledets.FlowCocycle.toFun }

@[simp]

theorem Oseledets.FlowCocycle.map_zero {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {φ : MeasurePreservingFlow μ} (A : FlowCocycle φ d) (x : X) : A.toFun 0 x = 1

The time-zero cocycle is the identity matrix.

theorem Oseledets.FlowCocycle.cocycle_apply {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {φ : MeasurePreservingFlow μ} (A : FlowCocycle φ d) (s t : ℝ) (x : X) : A.toFun (t + s) x = A.toFun t (φ.toFun s x) * A.toFun s x

The cocycle identity, newest factor on the left: A (t + s) x = A t (φ s x) * A s x.

theorem Oseledets.FlowCocycle.det_ne_zero {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {φ : MeasurePreservingFlow μ} (A : FlowCocycle φ d) (t : ℝ) (x : X) : (A.toFun t x).det ≠ 0

Each cocycle matrix is invertible (nonzero determinant).

theorem Oseledets.FlowCocycle.measurable {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {φ : MeasurePreservingFlow μ} (A : FlowCocycle φ d) (t : ℝ) : Measurable (A.toFun t)

Each time-t map of the cocycle is measurable.

theorem Oseledets.FlowCocycle.toCocycle_eq {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {φ : MeasurePreservingFlow μ} (A : FlowCocycle φ d) (n : ℕ) (x : X) : A.toFun (↑n) x = cocycle (fun (y : X) => A.toFun 1 y) (φ.toFun 1) n x

The reduction identity. At integer times the continuous-time cocycle agrees with the discrete iterated cocycle generated by its time-1 map A 1 (·) over the time-1 flow map φ 1: A (n : ℝ) x = cocycle (A 1 ·) (φ 1) n x.

This lets the continuous-flow MET at integer times be read off from the discrete MET applied to the generator A 1 and the dynamics φ 1.