Graph measurability and a.e.-constant dimension of the Lyapunov sublevel filtration

This module assembles two facts about the forward Lyapunov sublevel filtration Oseledets.lambdaSublevel A T x c (the limsup flag of Oseledets.Lyapunov.Filtration): its graph is measurable in the pair (x, v), and its level dimension is μ-a.e. constant under an ergodic base dynamics. Both are prerequisites of the measurable selection of the slow flag {v | lambdaBar A T x v ≤ c} that drives the (singular) measurable forward Oseledets filtration of issue #6.

The membership criterion and the IsUltrametricGrowth gate

Oseledets.lambdaSublevel is defined totally, with the junk value ⊥ off the set where v ↦ lambdaBar A T x v is an IsUltrametricGrowth function. On the good set the membership criterion is the expected v ∈ lambdaSublevel A T x c ↔ v = 0 ∨ lambdaBar A T x v ≤ c (Oseledets.mem_lambdaSublevel); off it, only v = 0 lies in the level. Accordingly the graph theorem carries the everywhere hypothesis hUM : ∀ x, IsUltrametricGrowth (lambdaBar A T x) — the pointwise form of the a.e. fact Oseledets.isUltrametricGrowth_lambdaBar (it holds a.e. for an invertible cocycle, and everywhere whenever the Furstenberg–Kesten sandwich converges everywhere, e.g. for a bounded generator). Under it the graph is literally {p | p.2 = 0} ∪ {p | lambdaBar A T p.1 p.2 ≤ c}, measurable from Oseledets.jointMeasurable_lambdaBar plus the measurability of {v = 0}.

Main results

• Oseledets.measurableSet_graph_lambdaSublevel: the graph {p : X × EuclideanSpace ℝ (Fin d) | p.2 ∈ lambdaSublevel A T p.1 c} is measurable (given the everywhere IsUltrametricGrowth gate hUM).
• Oseledets.ae_dim_lambdaSublevel_eq_const: for ergodic measure-preserving T and an invertible measurable generator, there is a single k : ℕ with Module.finrank ℝ (lambdaSublevel A T x c) = k for μ-a.e. x.

Proof outline of the a.e.-constant dimension

The action A x maps the level-c space at x onto the level-c space at T x, a.e. (Oseledets.vflag_equivariant). As A x is injective (det A ≠ 0), Submodule.map preserves finrank (Submodule.equivMapOfInjective), so the integer-valued x ↦ finrank ℝ (lambdaSublevel A T x c) is a.e. T-invariant. It is also measurable (Oseledets.MeasurableSubspace.measurable_finrank applied to a threaded MeasurableSubspace witness), so ergodicity forces it a.e. constant (Ergodic.ae_eq_const_of_ae_eq_comp₀; ℕ is a countably-separated measurable space).

References

• D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58.
• A. Quas, Multiplicative Ergodic Theorems and Applications (Theorem 2, §3.1).

Graph measurability of the sublevel filtration

theorem Oseledets.measurableSet_graph_lambdaSublevel {X : Type u_1} [MeasurableSpace X] {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} (hA : Measurable A) (hT : Measurable T) (hUM : ∀ (x : X), IsUltrametricGrowth (lambdaBar A T x)) (c : ℝ) : MeasurableSet {p : X × EuclideanSpace ℝ (Fin d) | p.2 ∈ lambdaSublevel A T p.1 c}

The graph of the Lyapunov sublevel filtration is measurable. Given the everywhere IsUltrametricGrowth gate hUM (the pointwise form of Oseledets.isUltrametricGrowth_lambdaBar, which holds a.e.), the set {p : X × EuclideanSpace ℝ (Fin d) | p.2 ∈ lambdaSublevel A T p.1 c} is measurable.

Under hUM the membership criterion Oseledets.mem_lambdaSublevel turns the graph into the union {p | p.2 = 0} ∪ {p | lambdaBar A T p.1 p.2 ≤ c}. The first set is the preimage of the closed singleton {0} under the continuous p ↦ p.2; the second is measurable from the joint measurability Oseledets.jointMeasurable_lambdaBar and the measurable constant c.

A.e.-constant dimension of the sublevel filtration

theorem Oseledets.ae_dim_lambdaSublevel_eq_const {X : Type u_1} [MeasurableSpace X] {T : X → X} {d : ℕ} {μ : 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)⁻¹) μ) (c : ℝ) (hVmeas : MeasurableSubspace fun (x : X) => lambdaSublevel A T x c) : ∃ (k : ℕ), ∀ᵐ (x : X) ∂μ, Module.finrank ℝ ↥(lambdaSublevel A T x c) = k

The level dimension of the Lyapunov sublevel filtration is μ-a.e. constant. For an ergodic measure-preserving T and an invertible (det A ≠ 0) measurable generator with the forward and inverse log-norm integrability of the invertible MET, the function x ↦ Module.finrank ℝ (lambdaSublevel A T x c) equals a single k : ℕ for μ-a.e. x.

The map A x carries the level-c space at x onto that at T x a.e. (Oseledets.vflag_equivariant), and is injective by det A ≠ 0, so Submodule.map preserves finrank (Submodule.equivMapOfInjective); hence the dimension is a.e. T-invariant. With a MeasurableSubspace witness hVmeas for the level family the dimension is measurable (Oseledets.MeasurableSubspace.measurable_finrank), and ergodicity makes an a.e.-invariant measurable ℕ-valued function a.e. constant (Ergodic.ae_eq_const_of_ae_eq_comp₀).