Joint measurability of the upper Lyapunov growth function

The upper Lyapunov growth function lambdaBar A T x v = limsup_n (1/n) · log ‖A⁽ⁿ⁾(x) · v‖ (Oseledets.lambdaBar, in Oseledets.Lyapunov.GrowthFunction) is known to be measurable in the base point x for each fixed vector v (Oseledets.measurable_lambdaBar_apply). The measurable singular forward Oseledets filtration, however, needs the joint measurability in the pair (x, v): the slow flag at x is the sublevel set {v | lambdaBar A T x v ≤ c}, and measurable selection of that set-valued map requires its graph {(x, v) | lambdaBar A T x v ≤ c} to be measurable in X × EuclideanSpace ℝ (Fin d), which follows at once from joint measurability of lambdaBar.

Main result

• Oseledets.jointMeasurable_lambdaBar: the map (x, v) ↦ lambdaBar A T x v is measurable on X × EuclideanSpace ℝ (Fin d), given a measurable cocycle generator A and a measurable base dynamics T.

Proof outline

lambdaBar A T x v is the limsup over n : ℕ of the per-step summands s n (x, v) = (n : ℝ)⁻¹ · log ‖toEuclideanCLM (cocycle A T n x) v‖. By Measurable.limsup it suffices to show each s n is jointly measurable, and for that it suffices to show (x, v) ↦ ‖toEuclideanCLM (cocycle A T n x) v‖ is jointly measurable.

The bridge to the existing Fin d → ℝ infrastructure is the identity toEuclideanCLM M v = toLp 2 (M *ᵥ ofLp v) (Mathlib's Matrix.ofLp_toEuclideanCLM together with WithLp.toLp_ofLp). Therefore the norm factors as

(x, v) ↦ (x, ofLp v) ↦ (cocycle A T n x) *ᵥ (ofLp v) ↦ toLp 2 (·) ↦ ‖·‖,

where:

• ofLp : EuclideanSpace ℝ (Fin d) → (Fin d → ℝ) is continuous, hence measurable;
• (x, w) ↦ (cocycle A T n x) *ᵥ w is jointly measurable (Oseledets.measurable_cocycleMulVec);
• toLp 2 : (Fin d → ℝ) → EuclideanSpace ℝ (Fin d) and the norm are continuous.

Source: S. Filip, Notes on the Multiplicative Ergodic Theorem (arXiv:1710.10694), §2.3 (measurability of the Lyapunov data underlying the Oseledets filtration).

theorem Oseledets.measurable_norm_toEuclideanCLM_cocycle {X : Type u_1} [MeasurableSpace X] {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : Measurable A) {T : X → X} (hT : Measurable T) (n : ℕ) : Measurable fun (p : X × EuclideanSpace ℝ (Fin d)) => ‖(Matrix.toEuclideanCLM (cocycle A T n p.1)) p.2‖

Joint measurability of the cocycle action norm. For each fixed step n, the map (x, v) ↦ ‖toEuclideanCLM (cocycle A T n x) v‖ is measurable on X × EuclideanSpace ℝ (Fin d).

The action is rewritten through the EuclideanSpace ≃ (Fin d → ℝ) linear isometry: by Matrix.ofLp_toEuclideanCLM and WithLp.toLp_ofLp, toEuclideanCLM M v = toLp 2 (M *ᵥ ofLp v), so the norm is the composition of the continuous ofLp, the jointly measurable matrix-vector action measurable_cocycleMulVec, the continuous toLp, and the continuous norm.

theorem Oseledets.jointMeasurable_lambdaBar {X : Type u_1} [MeasurableSpace X] {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : Measurable A) {T : X → X} (hT : Measurable T) : Measurable fun (p : X × EuclideanSpace ℝ (Fin d)) => lambdaBar A T p.1 p.2

Joint measurability of the upper Lyapunov growth function. The map (x, v) ↦ lambdaBar A T x v is measurable on X × EuclideanSpace ℝ (Fin d), given a measurable cocycle generator A and measurable base dynamics T.

lambdaBar A T x v is the limsup_n of the per-step summands (n : ℝ)⁻¹ · log ‖toEuclideanCLM (cocycle A T n x) v‖; each summand is jointly measurable (measurable_norm_toEuclideanCLM_cocycle, then Real.log, scaled by the constant n⁻¹), and Measurable.limsup lifts the per-step measurability to the limsup.