Measurability of the finite-step Gram sublevel spectral subspace

For a non-invertible (singular) cocycle the Oseledets multiplicative ergodic theorem degenerates from a direct-sum decomposition to a measurable filtration ℝ^d = V₁(ω) ⊇ ⋯ ⊇ V_{k+1}(ω) = {0} (Quas, Multiplicative Ergodic Theorems and Applications, Universidade de São Paulo lecture notes, 2013, Theorem 2; after Oseledec and Raghunathan). The intermediate slow spaces V_j(ω) are the spans of the singular directions whose singular value lies below the j-th gap, i.e. the spectral subspaces of the cocycle Gram matrix (cocycle A T n x)ᵀ (cocycle A T n x) corresponding to eigenvalues ≤ t for the appropriate threshold t = (gap)². This file delivers, for each fixed step n and arbitrary threshold t ≥ 0, a measurable choice of that finite-step approximant — the direct generalization of the bottom kernel stratum (Oseledets.cocycleKerEuclid, threshold 0) to an arbitrary sublevel t.

Strategy

The construction reuses the entire SingularKernelProjector.lean engine verbatim, replacing the threshold 0 by a free parameter t: the Gram matrix cocycleGram A T n x is unchanged, and the spectral projector cfc (Set.indicator (Set.Iic t) 1) onto its ≤ t eigenspace is again a self-adjoint idempotent — because the {0,1}-valued indicator squares to itself on the (finite) spectrum (indicator_mul_self), and cfc is multiplicative (idempotent_cfc_indicator) and preserves self-adjointness (isSelfAdjoint_cfc_indicator). None of these facts uses positivity of t. Its measurability in x is exactly Oseledets.measurable_spectralProjector for the measurable, self-adjoint Gram family (measurable_cocycleGram, cocycleGram_isHermitian), and the range-subspace measurability follows from the projector/range bridge Oseledets.measurableSubspace_range_of_measurable — precisely the pattern of vslow.

Main definitions

• Oseledets.cocycleSublevelEuclid: the n-step Gram sublevel spectral subspace at threshold t, i.e. the range of the spectral ≤ t projector cfc (Set.indicator (Set.Iic t) 1) (Gram), transported to a subspace of EuclideanSpace ℝ (Fin d). At t = 0 this is the cocycle kernel.

Main results

• Oseledets.measurableSubspace_cocycleSublevelEuclid: for each fixed n and threshold t, the family x ↦ cocycleSublevelEuclid A T n t x is a MeasurableSubspace.

gap

The threshold t is here a free parameter: it is not yet identified with a concrete Lyapunov/singular-value gap of the cocycle. Pinning t to the j-th spectral gap requires the exterior-power exponents from the Kingman subadditive machinery (the singular-value asymptotics), which is not in this module. Likewise the monotone limit in n — the analogue of Oseledets.eventualKer for the bottom stratum that assembles the genuine, n-independent flag space V_j(ω) — is deferred to a follow-up; this module supplies only the per-step, per-threshold measurable approximant.

noncomputable def Oseledets.cocycleSublevelEuclid {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (t : ℝ) (x : X) : Submodule ℝ (EuclideanSpace ℝ (Fin d))

The n-step Gram sublevel spectral subspace at threshold t: the range of the spectral ≤ t projector cfc (Set.indicator (Set.Iic t) 1) of the cocycle Gram matrix (cocycle A T n x)ᵀ (cocycle A T n x), transported to a subspace of EuclideanSpace ℝ (Fin d).

It is the span of the singular directions of cocycle A T n x whose squared singular value is ≤ t — the finite-step approximant of an intermediate slow space V_j(ω) of the singular Oseledets flag (Quas, Multiplicative Ergodic Theorems and Applications, 2013, Theorem 2). At t = 0 it is the cocycle kernel cocycleKerEuclid A T n x.

Equations

• Oseledets.cocycleSublevelEuclid A T n t x = (↑(Matrix.toEuclideanCLM (cfc ((Set.Iic t).indicator 1) (Oseledets.cocycleGram A T n x)))).range

theorem Oseledets.measurableSubspace_cocycleSublevelEuclid {X : Type u_1} {d : ℕ} [MeasurableSpace X] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : Measurable A) {T : X → X} (hT : Measurable T) (n : ℕ) (t : ℝ) : MeasurableSubspace fun (x : X) => cocycleSublevelEuclid A T n t x

Measurability of the n-step Gram sublevel spectral subspace. For each fixed step n and threshold t, the family x ↦ cocycleSublevelEuclid A T n t x is a MeasurableSubspace.

The defining matrix cfc (Set.indicator (Set.Iic t) 1) (cocycleGram A T n x) is, for every x, a self-adjoint idempotent (isSelfAdjoint_cfc_indicator, idempotent_cfc_indicator), and it is measurable in x by Oseledets.measurable_spectralProjector applied to the measurable, self-adjoint Gram family (measurable_cocycleGram, cocycleGram_isHermitian). The projector/range bridge Oseledets.measurableSubspace_range_of_measurable then makes the range subspaces measurable — exactly the vslow pattern.

This is the per-step, per-threshold analytic engine for the measurability of an intermediate slow space of the singular (non-invertible) Oseledets filtration (Quas, Multiplicative Ergodic Theorems and Applications, 2013, Theorem 2).