Invertibility infrastructure for the two-sided Oseledets theorem

For the two-sided multiplicative ergodic theorem the base dynamics is an invertible measure-preserving system, encoded as a MeasurableEquiv T : X ≃ᵐ X (with inverse T.symm). The forward generator A is an everywhere-invertible matrix-valued map, and the relevant backward object is the cocycle of the backward generator backwardGen A T x = (A (T.symm x))⁻¹ over T.symm.

This file collects the backward infrastructure: the backward generator and its hypothesis transfer (nonzero determinant, measurability, both L¹-log-norm integrabilities), the companion cocycle recursion cocycle_succ' (newest factor on the right), the two backward cocycle identities B⁽ⁿ⁾(x) = (A⁽ⁿ⁾(T⁻ⁿ x))⁻¹ and B⁽ⁿ⁾(Tⁿ y) = (A⁽ⁿ⁾ y)⁻¹, and the extraction of a conull set that is invariant under both T and T.symm. A convenience bundle backwardData packages the four standing hypotheses on the pair (⇑T.symm, backwardGen A T) so that the one-sided theorems can be instantiated for the backward system in one line.

Main definitions

• Oseledets.backwardGen: the backward generator x ↦ (A (T.symm x))⁻¹.
• Oseledets.BackwardData: the bundled standing hypotheses for the backward system.

Main results

• Oseledets.backwardGen_det_ne_zero, Oseledets.measurable_backwardGen: hypothesis transfer (invertibility and measurability) for the backward generator.
• Oseledets.integrableLogNorm_backwardGen, Oseledets.integrableLogNorm_backwardGen_inv: transfer of the two L¹-log-norm integrabilities.
• Oseledets.cocycle_succ': the cocycle recursion with the newest factor on the right.
• Oseledets.cocycle_backwardGen, Oseledets.cocycle_backwardGen_iterate: the two backward cocycle identities.
• Oseledets.exists_conull_biinvariant: a conull set inside a given conull set that is invariant under both T and T.symm.

noncomputable def Oseledets.backwardGen {X : Type u_1} [MeasurableSpace X] {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X ≃ᵐ X) : X → Matrix (Fin d) (Fin d) ℝ

The backward generator B x = (A (T⁻¹ x))⁻¹, whose cocycle over T.symm implements the backward iterates of the invertible cocycle generated by A.

Equations

• Oseledets.backwardGen A T x = (A (T.symm x))⁻¹

theorem Oseledets.backwardGen_det_ne_zero {X : Type u_1} [MeasurableSpace X] {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (T : X ≃ᵐ X) (x : X) : (backwardGen A T x).det ≠ 0

The determinant of the backward generator is nonzero whenever A is everywhere invertible.

theorem Oseledets.measurable_backwardGen {X : Type u_1} [MeasurableSpace X] {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hAmeas : Measurable A) (T : X ≃ᵐ X) : Measurable (backwardGen A T)

The backward generator is measurable whenever A is.

theorem Oseledets.integrableLogNorm_backwardGen {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X ≃ᵐ X} (hTm : MeasureTheory.MeasurePreserving (⇑T) μ μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : IntegrableLogNorm (backwardGen A T) μ

Integrability transfer for the backward generator: log⁺‖B‖ ∈ L¹ from log⁺‖A⁻¹‖ ∈ L¹, by composing with the measure-preserving T.symm.

theorem Oseledets.integrableLogNorm_backwardGen_inv {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) {T : X ≃ᵐ X} (hTm : MeasureTheory.MeasurePreserving (⇑T) μ μ) (hint : IntegrableLogNorm A μ) : IntegrableLogNorm (fun (x : X) => (backwardGen A T x)⁻¹) μ

Integrability transfer for the inverse of the backward generator: log⁺‖B⁻¹‖ ∈ L¹ from log⁺‖A‖ ∈ L¹. The inverse of the backward generator is A ∘ T.symm (Matrix.nonsing_inv_nonsing_inv), so this is again composition with the measure-preserving T.symm.

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 = A (T^[n] x) * cocycle A T n x

The cocycle recursion with the newest factor on the right (the companion of cocycle_succ, which puts it on the left): A⁽ⁿ⁺¹⁾(x) = A(Tⁿ x) · A⁽ⁿ⁾(x).

theorem Oseledets.cocycle_backwardGen {X : Type u_1} [MeasurableSpace X] {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (T : X ≃ᵐ X) (n : ℕ) (x : X) : cocycle (backwardGen A T) (⇑T.symm) n x = (cocycle A (⇑T) n ((⇑T.symm)^[n] x))⁻¹

The backward cocycle identity: B⁽ⁿ⁾(x) = (A⁽ⁿ⁾(T⁻ⁿ x))⁻¹, where B = backwardGen A T runs over T.symm.

theorem Oseledets.cocycle_backwardGen_iterate {X : Type u_1} [MeasurableSpace X] {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (T : X ≃ᵐ X) (n : ℕ) (y : X) : cocycle (backwardGen A T) (⇑T.symm) n ((⇑T)^[n] y) = (cocycle A (⇑T) n y)⁻¹

Dual form of the backward cocycle identity at a forward point: B⁽ⁿ⁾(Tⁿ y) = (A⁽ⁿ⁾ y)⁻¹.

theorem Oseledets.exists_conull_biinvariant {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X ≃ᵐ X} (hTm : MeasureTheory.MeasurePreserving (⇑T) μ μ) {S : Set X} (hS : MeasurableSet S) (hconull : μ Sᶜ = 0) : ∃ S' ⊆ S, MeasurableSet S' ∧ μ S'ᶜ = 0 ∧ (∀ x ∈ S', T x ∈ S') ∧ ∀ x ∈ S', T.symm x ∈ S'

Biinvariant conull set extraction. Given a conull measurable set S, there is a conull measurable subset S' ⊆ S invariant under both T and T.symm.

Construction: S' = (⋂ₙ (T^[n])⁻¹' S) ∩ (⋂ₙ (T.symm^[n])⁻¹' S). Each iterate is measure-preserving, so each preimage is conull and a countable intersection of conull sets is conull. Bi-invariance is an index shift: applying T (resp. T.symm) reindexes the two families against each other, the cross term collapsing through T.symm ∘ T = id (resp. T ∘ T.symm = id).

structure Oseledets.BackwardData {X : Type u_1} [MeasurableSpace X] {d : ℕ} (μ : MeasureTheory.Measure X) (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X ≃ᵐ X) : Prop

The bundled standing hypotheses for the backward system (⇑T.symm, backwardGen A T): everywhere-nonzero determinant, measurability of the generator, and the two L¹-log-norm integrabilities. This lets the one-sided theorems be instantiated for the backward dynamics in a single step.

• det_ne_zero (x : X) : (backwardGen A T x).det ≠ 0

  The backward generator is everywhere invertible.

• measurable : Measurable (backwardGen A T)

  The backward generator is measurable.

• integrableLogNorm : IntegrableLogNorm (backwardGen A T) μ

  log⁺‖B‖ ∈ L¹(μ).

• integrableLogNorm_inv : IntegrableLogNorm (fun (x : X) => (backwardGen A T x)⁻¹) μ

  log⁺‖B⁻¹‖ ∈ L¹(μ).

theorem Oseledets.backwardData_of {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X ≃ᵐ X} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hTm : MeasureTheory.MeasurePreserving (⇑T) μ μ) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : BackwardData μ A T

Assemble the backward-system standing hypotheses from the forward-system data.