Equivariance of the continuous-flow Oseledets filtration at every real time

The discrete Oseledets multiplicative ergodic theorem produces, for the time-1 generator A 1 over the time-1 dynamics φ 1, a filtration V that is equivariant under the cocycle one integer step at a time. This file upgrades that to equivariance under the flow at every real time t₀ : ℝ: almost everywhere, Submodule.map (toEuclideanCLM (A t₀ x)) (V i x) = V i (φ t₀ x).

The route is purely analytic and follows the canonical growth characterization Oseledets.IsOseledetsFiltration.ae_mem_iff_limsup_le: a vector lies in the level V i iff it is zero or its discrete-time Lyapunov growth rate is ≤ lam i. The fixed-time matrix A t₀ x is a bounded (operator-norm-comparable to a constant in n) bijection, so applying it to a vector changes the discrete-time limsup growth rate by o(1), hence not at all. Membership in the growth sublevel set is therefore preserved, which is exactly equivariance.

Main results

• Oseledets.norm_clm_pos: for invertible M and nonzero v, 0 < ‖toEuclideanCLM M v‖.
• Oseledets.ae_tendsto_logNorm_fixedTime_zero: almost everywhere, the fixed-time log-norms n⁻¹ · log ‖A t₀ (φ (n:ℝ) x)‖ and n⁻¹ · log ‖(A t₀ (φ (n:ℝ) x))⁻¹‖ tend to 0.
• Oseledets.glim_shift: almost everywhere, the discrete-time growth limsup is unchanged by applying toEuclideanCLM (A t₀ x) to the test vector.
• Oseledets.ae_flow_equivariant: almost everywhere, the Oseledets filtration is equivariant under the flow at the real time t₀.

S0: local positivity of the image norm

theorem Oseledets.norm_clm_pos {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) (hM : M.det ≠ 0) {v : EuclideanSpace ℝ (Fin d)} (hv : v ≠ 0) : 0 < ‖(Matrix.toEuclideanCLM M) v‖

Local positivity. For an invertible matrix M and a nonzero vector v, the image toEuclideanCLM M v is nonzero, hence has positive norm. The continuous linear map toEuclideanCLM M has the two-sided inverse toEuclideanCLM M⁻¹, so it is injective.

S1: the fixed-time log-norm is sublinear, almost everywhere

The core difficulty is integrability of a dominator for |log ‖A t₀ y‖|. We build, for every real time, an integrable function dominating both log⁺ ‖A t₀ y‖ and log⁺ ‖(A t₀ y)⁻¹‖; the two-sided log-norm bound abs_log_norm_le then turns this into an integrable dominator for the absolute log-norm, and the orbital tail estimate finishes the squeeze.

theorem Oseledets.ae_tendsto_logNorm_fixedTime_zero {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (A : FlowCocycle φ d) {g g' : X → ℝ} (hg : MeasureTheory.Integrable g μ) (hg' : MeasureTheory.Integrable g' μ) (hgb : ∀ s ∈ Set.Icc 0 1, ∀ (y : X), ‖A.toFun s y‖.posLog ≤ g y) (hg'b : ∀ s ∈ Set.Icc 0 1, ∀ (y : X), ‖(A.toFun s y)⁻¹‖.posLog ≤ g' y) (t₀ : ℝ) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖A.toFun t₀ (φ.toFun (↑n) x)‖) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(A.toFun t₀ (φ.toFun (↑n) x))⁻¹‖) Filter.atTop (nhds 0)

S1: the fixed-time log-norm is sublinear, almost everywhere. For any real time t₀, almost every x satisfies that both n⁻¹ · log ‖A t₀ (φ (n:ℝ) x)‖ and n⁻¹ · log ‖(A t₀ (φ (n:ℝ) x))⁻¹‖ tend to 0.

We dominate both absolute log-norms by an integrable function G (built from the two-sided log-norm bound and the integrable dominator exists_integrable_dom), apply the orbital tail estimate to G along the integer orbit of φ 1, and squeeze.

S2: the discrete growth limsup is shift-invariant under A t₀ x

The discrete-time growth rate n⁻¹ · log ‖cocycle … n x · u‖ is unchanged when the test vector is pushed through the fixed bijection toEuclideanCLM (A t₀ x). We first establish a.e. two-sided boundedness of this growth average (via the Furstenberg–Kesten Fekete bounds and the Birkhoff ergodic theorem), then conclude with the perturbation lemma limsup_eq_of_sub_tendsto_zero.

theorem Oseledets.glim_shift {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] (φ : MeasurePreservingFlow μ) (A : FlowCocycle φ d) {g g' : X → ℝ} (hg : MeasureTheory.Integrable g μ) (hg' : MeasureTheory.Integrable g' μ) (hgb : ∀ s ∈ Set.Icc 0 1, ∀ (y : X), ‖A.toFun s y‖.posLog ≤ g y) (hg'b : ∀ s ∈ Set.Icc 0 1, ∀ (y : X), ‖(A.toFun s y)⁻¹‖.posLog ≤ g' y) (t₀ : ℝ) : ∀ᵐ (x : X) ∂μ, ∀ (u : EuclideanSpace ℝ (Fin d)), Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle (fun (y : X) => A.toFun 1 y) (φ.toFun 1) n (φ.toFun t₀ x))) ((Matrix.toEuclideanCLM (A.toFun t₀ x)) u)‖) Filter.atTop = Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle (fun (y : X) => A.toFun 1 y) (φ.toFun 1) n x)) u‖) Filter.atTop

S2: the discrete growth limsup is shift-invariant under A t₀ x. Almost everywhere, for every test vector u, the discrete-time growth limsup of cocycle … n x applied to u equals that of cocycle … n (φ t₀ x) applied to the pushed-forward vector toEuclideanCLM (A t₀ x) u. The fixed bijection A t₀ x perturbs the per-step log-norm only by o(n), by the fixed-time sublinearity ae_tendsto_logNorm_fixedTime_zero.

S3: per-time equivariance of the Oseledets filtration

theorem Oseledets.ae_flow_equivariant {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (φ : MeasurePreservingFlow μ) (A : FlowCocycle φ d) {g g' : X → ℝ} (hg : MeasureTheory.Integrable g μ) (hg' : MeasureTheory.Integrable g' μ) (hgb : ∀ s ∈ Set.Icc 0 1, ∀ (y : X), ‖A.toFun s y‖.posLog ≤ g y) (hg'b : ∀ s ∈ Set.Icc 0 1, ∀ (y : X), ‖(A.toFun s y)⁻¹‖.posLog ≤ g' y) {k : ℕ} {lam : Fin k → ℝ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hV : IsOseledetsFiltration μ (φ.toFun 1) (fun (x : X) => A.toFun 1 x) k lam V) (t₀ : ℝ) : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (k + 1)), Submodule.map (↑(Matrix.toEuclideanCLM (A.toFun t₀ x))) (V i x) = V i (φ.toFun t₀ x)

Equivariance of the Oseledets filtration at every real time. Let V be the Oseledets filtration produced by the discrete theorem for the time-1 generator A 1 over the time-1 dynamics φ 1. Then for every real time t₀, almost everywhere the filtration is equivariant under the flow: Submodule.map (toEuclideanCLM (A t₀ x)) (V i x) = V i (φ t₀ x).

The proof combines the canonical growth characterization IsOseledetsFiltration.ae_mem_iff_limsup_le at x and (pulled back) at φ t₀ x, the shift-invariance of the growth limsup under A t₀ x (glim_shift), and the fact that toEuclideanCLM (A t₀ x) is a bijection. The bottom level V (Fin.last k) is ⊥, which maps to ⊥; each other level is handled by le_antisymm of the two membership characterizations.