The two-sided Oseledets splitting

This is the two-sided Oseledets multiplicative ergodic theorem. It assembles the forward and backward one-sided Oseledets filtrations into a single measurable, A-equivariant splitting ℝᵈ = E₁(x) ⊕ ⋯ ⊕ E_k(x) with two-sided growth: for a nonzero v ∈ Eᵢ(x) the forward cocycle grows at rate λᵢ and the backward cocycle at rate −λᵢ.

The pieces consumed are:

• oseledets_filtration_dims, instantiated for the forward system (T, A) and (via backwardData_of) for the backward system (T.symm, backwardGen A T), giving the forward data lam0, V and the backward data mu0, W, each with its dimension formula;
• ae_crux and ae_counting (the transversality crux and the resulting counting bound);
• sum_mu0_eq_neg_sum_lam0, reflect_of_counting_and_sum and the reflection corollaries (numExp_eq_of_counting, expEnum_eq_neg_rev_of_counting, backward_count_eq_of_counting), which align the backward index to the forward one (l = k, μ_{sᵢ} = −λᵢ);
• MeasurableSubspace.inf for the measurability of the intersection bundle.

The internal-direct-sum structure is obtained from a pure telescoping-flag lattice lemma (flag_iSupIndep_and_iSup): the split subspaces Eᵢ = V i.castSucc ⊓ W (sidx i).castSucc satisfy V i.castSucc = Eᵢ ⊔ V i.succ and Eᵢ ⊓ V i.succ = ⊥, which telescope a ⊤-to-⊥ flag into an internal direct sum.

Main results

• Oseledets.oseledets_splitting_dim_zero — the trivial d = 0 case.
• Oseledets.oseledets_splitting — the headline two-sided splitting theorem.

References

• V. I. Oseledets, A multiplicative ergodic theorem. Lyapunov characteristic numbers for dynamical systems, Trans. Moscow Math. Soc. 19 (1968), 197–231.
• D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58.
• L. Arnold, Random Dynamical Systems, Springer Monographs in Mathematics, 1998.

A pure telescoping-flag lattice lemma

The aligned backward index and the transported backward equivariance

noncomputable def Oseledets.sidx {d : ℕ} {lam0 mu0 : ℕ → ℝ} (hrefl : ∀ j < d, mu0 j = -lam0 (d - 1 - j)) (i : Fin (numExp lam0 d)) : Fin (numExp mu0 d)

The backward filtration index aligned to the forward level i, so that its exponent is −λᵢ: sidx i = cast (Fin.rev i) under numExp mu0 d = numExp lam0 d.

Equations

• Oseledets.sidx hrefl i = Fin.cast ⋯ i.rev

theorem Oseledets.sidx_exp {d : ℕ} {lam0 mu0 : ℕ → ℝ} (hrefl : ∀ j < d, mu0 j = -lam0 (d - 1 - j)) (i : Fin (numExp lam0 d)) : expEnum mu0 d (sidx hrefl i) = -expEnum lam0 d i

The aligned backward exponent is the negated forward one: μ_{sidx i} = −λᵢ.

theorem Oseledets.map_of_map_inv {d : ℕ} {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.det ≠ 0) {P Q : Submodule ℝ (EuclideanSpace ℝ (Fin d))} (h : Submodule.map (↑(Matrix.toEuclideanCLM M⁻¹)) Q = P) : Submodule.map (↑(Matrix.toEuclideanCLM M)) P = Q

Transport of equivariance through the inverse generator. If M is invertible and map (M⁻¹) Q = P, then map (M) P = Q. Used to convert the backward filtration's backwardGen-equivariance into forward A-equivariance.

Per-point dimension and lattice facts

theorem Oseledets.finrank_Vsucc {d : ℕ} {lam0 : ℕ → ℝ} {Vx : Fin (numExp lam0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hVdim : ∀ (i : Fin (numExp lam0 d)), Module.finrank ℝ ↥(Vx i.castSucc) = {j ∈ Finset.range d | lam0 j ≤ expEnum lam0 d i}.card) (hVlast : Vx (Fin.last (numExp lam0 d)) = ⊥) (i : Fin (numExp lam0 d)) : Module.finrank ℝ ↥(Vx i.succ) = {j ∈ Finset.range d | lam0 j < expEnum lam0 d i}.card

The forward successor-level finrank equals the strict forward count below λᵢ.

theorem Oseledets.finrank_Wsidx {d : ℕ} {lam0 mu0 : ℕ → ℝ} (hrefl : ∀ j < d, mu0 j = -lam0 (d - 1 - j)) {Wx : Fin (numExp mu0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hWdim : ∀ (s : Fin (numExp mu0 d)), Module.finrank ℝ ↥(Wx s.castSucc) = {j ∈ Finset.range d | mu0 j ≤ expEnum mu0 d s}.card) (i : Fin (numExp lam0 d)) : Module.finrank ℝ ↥(Wx (sidx hrefl i).castSucc) = d - {j ∈ Finset.range d | lam0 j < expEnum lam0 d i}.card

The aligned backward-level finrank is d minus the strict forward count below λᵢ.

theorem Oseledets.crux_succ {d : ℕ} {lam0 mu0 : ℕ → ℝ} (hrefl : ∀ j < d, mu0 j = -lam0 (d - 1 - j)) {Vx : Fin (numExp lam0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {Wx : Fin (numExp mu0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hVlast : Vx (Fin.last (numExp lam0 d)) = ⊥) (hcrux : ∀ (i' : Fin (numExp lam0 d)) (s : Fin (numExp mu0 d)), expEnum lam0 d i' + expEnum mu0 d s < 0 → Vx i'.castSucc ⊓ Wx s.castSucc = ⊥) (i : Fin (numExp lam0 d)) : Vx i.succ ⊓ Wx (sidx hrefl i).castSucc = ⊥

Crux disjointness at the forward successor level.

theorem Oseledets.crux_succ_backward {d : ℕ} {lam0 mu0 : ℕ → ℝ} (hrefl : ∀ j < d, mu0 j = -lam0 (d - 1 - j)) {Vx : Fin (numExp lam0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {Wx : Fin (numExp mu0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hWlast : Wx (Fin.last (numExp mu0 d)) = ⊥) (hcrux : ∀ (i' : Fin (numExp lam0 d)) (s : Fin (numExp mu0 d)), expEnum lam0 d i' + expEnum mu0 d s < 0 → Vx i'.castSucc ⊓ Wx s.castSucc = ⊥) (i : Fin (numExp lam0 d)) : Vx i.castSucc ⊓ Wx (sidx hrefl i).succ = ⊥

Crux disjointness at the backward successor level.

noncomputable def Oseledets.esplitAt {d : ℕ} {lam0 mu0 : ℕ → ℝ} (hrefl : ∀ j < d, mu0 j = -lam0 (d - 1 - j)) {Vx : Fin (numExp lam0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {Wx : Fin (numExp mu0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (i : Fin (numExp lam0 d)) : Submodule ℝ (EuclideanSpace ℝ (Fin d))

The intersection-splitting subspace at forward level i (per-point).

Equations

• Oseledets.esplitAt hrefl i = Vx i.castSucc ⊓ Wx (Oseledets.sidx hrefl i).castSucc

theorem Oseledets.sup_eq_top {d : ℕ} {lam0 mu0 : ℕ → ℝ} (hrefl : ∀ j < d, mu0 j = -lam0 (d - 1 - j)) {Vx : Fin (numExp lam0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {Wx : Fin (numExp mu0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hVdim : ∀ (i : Fin (numExp lam0 d)), Module.finrank ℝ ↥(Vx i.castSucc) = {j ∈ Finset.range d | lam0 j ≤ expEnum lam0 d i}.card) (hWdim : ∀ (s : Fin (numExp mu0 d)), Module.finrank ℝ ↥(Wx s.castSucc) = {j ∈ Finset.range d | mu0 j ≤ expEnum mu0 d s}.card) (hVanti : Antitone Vx) (hVlast : Vx (Fin.last (numExp lam0 d)) = ⊥) (hcrux : ∀ (i' : Fin (numExp lam0 d)) (s : Fin (numExp mu0 d)), expEnum lam0 d i' + expEnum mu0 d s < 0 → Vx i'.castSucc ⊓ Wx s.castSucc = ⊥) (i : Fin (numExp lam0 d)) : Vx i.castSucc ⊔ Wx (sidx hrefl i).castSucc = ⊤

Totality at level i: Vx i.castSucc ⊔ Wx (sidx i).castSucc = ⊤.

theorem Oseledets.finrank_esplitAt {d : ℕ} {lam0 mu0 : ℕ → ℝ} (hrefl : ∀ j < d, mu0 j = -lam0 (d - 1 - j)) {Vx : Fin (numExp lam0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {Wx : Fin (numExp mu0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hVdim : ∀ (i : Fin (numExp lam0 d)), Module.finrank ℝ ↥(Vx i.castSucc) = {j ∈ Finset.range d | lam0 j ≤ expEnum lam0 d i}.card) (hWdim : ∀ (s : Fin (numExp mu0 d)), Module.finrank ℝ ↥(Wx s.castSucc) = {j ∈ Finset.range d | mu0 j ≤ expEnum mu0 d s}.card) (hVanti : Antitone Vx) (hVlast : Vx (Fin.last (numExp lam0 d)) = ⊥) (hcrux : ∀ (i' : Fin (numExp lam0 d)) (s : Fin (numExp mu0 d)), expEnum lam0 d i' + expEnum mu0 d s < 0 → Vx i'.castSucc ⊓ Wx s.castSucc = ⊥) (i : Fin (numExp lam0 d)) : Module.finrank ℝ ↥(esplitAt hrefl i) = {j ∈ Finset.range d | lam0 j ≤ expEnum lam0 d i}.card - {j ∈ Finset.range d | lam0 j < expEnum lam0 d i}.card

finrank (esplitAt i) = #{j | lam0 j ≤ λᵢ} − #{j | lam0 j < λᵢ}.

theorem Oseledets.esplitAt_inf_Vsucc {d : ℕ} {lam0 mu0 : ℕ → ℝ} (hrefl : ∀ j < d, mu0 j = -lam0 (d - 1 - j)) {Vx : Fin (numExp lam0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {Wx : Fin (numExp mu0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hVlast : Vx (Fin.last (numExp lam0 d)) = ⊥) (hcrux : ∀ (i' : Fin (numExp lam0 d)) (s : Fin (numExp mu0 d)), expEnum lam0 d i' + expEnum mu0 d s < 0 → Vx i'.castSucc ⊓ Wx s.castSucc = ⊥) (i : Fin (numExp lam0 d)) : esplitAt hrefl i ⊓ Vx i.succ = ⊥

esplitAt i ⊓ Vx i.succ = ⊥.

theorem Oseledets.Vcast_eq_esplitAt_sup_Vsucc {d : ℕ} {lam0 mu0 : ℕ → ℝ} (hrefl : ∀ j < d, mu0 j = -lam0 (d - 1 - j)) {Vx : Fin (numExp lam0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {Wx : Fin (numExp mu0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hVdim : ∀ (i : Fin (numExp lam0 d)), Module.finrank ℝ ↥(Vx i.castSucc) = {j ∈ Finset.range d | lam0 j ≤ expEnum lam0 d i}.card) (hWdim : ∀ (s : Fin (numExp mu0 d)), Module.finrank ℝ ↥(Wx s.castSucc) = {j ∈ Finset.range d | mu0 j ≤ expEnum mu0 d s}.card) (hVanti : Antitone Vx) (hVlast : Vx (Fin.last (numExp lam0 d)) = ⊥) (hcrux : ∀ (i' : Fin (numExp lam0 d)) (s : Fin (numExp mu0 d)), expEnum lam0 d i' + expEnum mu0 d s < 0 → Vx i'.castSucc ⊓ Wx s.castSucc = ⊥) (i : Fin (numExp lam0 d)) : Vx i.castSucc = esplitAt hrefl i ⊔ Vx i.succ

The telescoping identity Vx i.castSucc = esplitAt i ⊔ Vx i.succ.

theorem Oseledets.one_le_finrank_esplitAt {d : ℕ} {lam0 mu0 : ℕ → ℝ} (hrefl : ∀ j < d, mu0 j = -lam0 (d - 1 - j)) {Vx : Fin (numExp lam0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {Wx : Fin (numExp mu0 d + 1) → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hVdim : ∀ (i : Fin (numExp lam0 d)), Module.finrank ℝ ↥(Vx i.castSucc) = {j ∈ Finset.range d | lam0 j ≤ expEnum lam0 d i}.card) (hWdim : ∀ (s : Fin (numExp mu0 d)), Module.finrank ℝ ↥(Wx s.castSucc) = {j ∈ Finset.range d | mu0 j ≤ expEnum mu0 d s}.card) (hVanti : Antitone Vx) (hVlast : Vx (Fin.last (numExp lam0 d)) = ⊥) (hcrux : ∀ (i' : Fin (numExp lam0 d)) (s : Fin (numExp mu0 d)), expEnum lam0 d i' + expEnum mu0 d s < 0 → Vx i'.castSucc ⊓ Wx s.castSucc = ⊥) (i : Fin (numExp lam0 d)) : 1 ≤ Module.finrank ℝ ↥(esplitAt hrefl i)

The split subspace is nonzero: 1 ≤ finrank (esplitAt i).

The splitting in positive dimension

theorem Oseledets.oseledets_splitting_pos {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X ≃ᵐ X} (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)⁻¹) μ) : ∃ (k : ℕ) (lam : Fin k → ℝ) (E : Fin k → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))), StrictAnti lam ∧ (∀ (i : Fin k), MeasurableSubspace fun (x : X) => E i x) ∧ ∀ᵐ (x : X) ∂μ, (DirectSum.IsInternal fun (i : Fin k) => E i x) ∧ (∀ (i : Fin k), E i x ≠ ⊥) ∧ (∀ (i : Fin k), Submodule.map (↑(Matrix.toEuclideanCLM (A x))) (E i x) = E i (T x)) ∧ ∀ (i : Fin k), ∀ v ∈ E i x, v ≠ 0 → Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A (⇑T) n x)) v‖) Filter.atTop (nhds (lam i)) ∧ Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A (⇑T) n ((⇑T.symm)^[n] x))⁻¹) v‖) Filter.atTop (nhds (-lam i))

The two-sided Oseledets splitting (positive dimension). The headline statement, established for d > 0; the public oseledets_splitting adds the trivial d = 0 branch.

The dimension-zero case

theorem Oseledets.oseledets_splitting_dim_zero {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X ≃ᵐ X} (_hT : Ergodic (⇑T) μ) (A : X → Matrix (Fin 0) (Fin 0) ℝ) (_hA : ∀ (x : X), (A x).det ≠ 0) (_hAmeas : Measurable A) (_hint : IntegrableLogNorm A μ) (_hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : ∃ (k : ℕ) (lam : Fin k → ℝ) (E : Fin k → X → Submodule ℝ (EuclideanSpace ℝ (Fin 0))), StrictAnti lam ∧ (∀ (i : Fin k), MeasurableSubspace fun (x : X) => E i x) ∧ ∀ᵐ (x : X) ∂μ, (DirectSum.IsInternal fun (i : Fin k) => E i x) ∧ (∀ (i : Fin k), E i x ≠ ⊥) ∧ (∀ (i : Fin k), Submodule.map (↑(Matrix.toEuclideanCLM (A x))) (E i x) = E i (T x)) ∧ ∀ (i : Fin k), ∀ v ∈ E i x, v ≠ 0 → Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A (⇑T) n x)) v‖) Filter.atTop (nhds (lam i)) ∧ Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A (⇑T) n ((⇑T.symm)^[n] x))⁻¹) v‖) Filter.atTop (nhds (-lam i))

The two-sided Oseledets splitting, dimension-zero case. Trivial: k = 0, the empty internal direct sum of the zero module.

The two-sided Oseledets splitting

theorem Oseledets.oseledets_splitting {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X ≃ᵐ X} (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)⁻¹) μ) : ∃ (k : ℕ) (lam : Fin k → ℝ) (E : Fin k → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))), StrictAnti lam ∧ (∀ (i : Fin k), MeasurableSubspace fun (x : X) => E i x) ∧ ∀ᵐ (x : X) ∂μ, (DirectSum.IsInternal fun (i : Fin k) => E i x) ∧ (∀ (i : Fin k), E i x ≠ ⊥) ∧ (∀ (i : Fin k), Submodule.map (↑(Matrix.toEuclideanCLM (A x))) (E i x) = E i (T x)) ∧ ∀ (i : Fin k), ∀ v ∈ E i x, v ≠ 0 → Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A (⇑T) n x)) v‖) Filter.atTop (nhds (lam i)) ∧ Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A (⇑T) n ((⇑T.symm)^[n] x))⁻¹) v‖) Filter.atTop (nhds (-lam i))

The two-sided Oseledets multiplicative ergodic theorem (splitting form).

For an invertible ergodic measure-preserving system T : X ≃ᵐ X and a measurable everywhere-invertible cocycle generator A with log⁺‖A‖, log⁺‖A⁻¹‖ ∈ L¹(μ), there are k distinct Lyapunov exponents λ₀ > ⋯ > λ_{k-1} and a measurable, A-equivariant splitting ℝᵈ = E₀(x) ⊕ ⋯ ⊕ E_{k-1}(x) of EuclideanSpace ℝ (Fin d) such that, for μ-a.e. x, every nonzero v ∈ Eᵢ(x) grows forward at rate λᵢ and backward at rate −λᵢ: (1/n) log‖A⁽ⁿ⁾(x) v‖ → λᵢ and (1/n) log‖(A⁽ⁿ⁾(T⁻ⁿx))⁻¹ v‖ → −λᵢ.