Measurability of the lambdaBar-sublevel slow space for singular cocycles

For a possibly-singular (non-invertible, det A = 0 allowed) matrix cocycle generator A : X → Matrix (Fin d) (Fin d) ℝ, the intermediate slow space of the singular forward Oseledets filtration at a Lyapunov cut c is the lambdaBar-sublevel

lambdaSublevel A T x c = {v : lambdaBar A T x v ≤ c} (det-free; lambdaBar is det-free,

Oseledets/Lyapunov/GrowthFunction.lean). Track 6B asks the last open measurability question of the unconditional singular flag: is x ↦ {v : lambdaBar A T x v ≤ c} a MeasurableSubspace?

This module resolves the measurability question to a single, precisely-named convergence input and lands the reduction sorry-free and det-free, then pins exactly why the input cannot be supplied unconditionally for singular cocycles.

The reduction (sorry-free, det-free)

The finite-step slow approximants vSlowSingularStep A T c n x — the range of the slow qpow spectral projector cfc (𝟙_{(-∞,c]}) (qpow A T n x), where qpow A T n x = (Gₙ)^{1/(2n)} is the renormalized Gram (SingularSlowSpace.lean) — are everywhere measurable in x, per fixed n (measurableSubspace_vSlowSingularStep), unconditionally. If those finite-step projector matrices converge — for every x — to the projector matrix of the lambdaBar-sublevel, then the limit is measurable as a pointwise limit of measurable matrix-valued maps (measurable_of_tendsto_metrizable, entrywise). We package:

• Oseledets.measurableSubspace_of_tendsto_orthProjMatrix — the fully general soft lemma: a family V whose orthProjMatrix is, for every x, the pointwise (in n) limit of a sequence of measurable matrix families is a MeasurableSubspace. (The same measurable_of_tendsto_metrizable template as Oseledets.MeasurableSubspace.inf and Oseledets.measurable_orthProjMatrix_eventualKer.)

• Oseledets.measurableSubspace_lambdaSublevel_of_tendsto — the det-free reduction: if for every x the slow projectors orthProjMatrix (vSlowSingularStep A T c n x) converge to orthProjMatrix (lambdaSublevel A T x c), then MeasurableSubspace (fun x => lambdaSublevel A T x c). No det ≠ 0. The measurability of {v : lambdaBar A T x v ≤ c} is thereby reduced exactly to the convergence-to-the-right-limit hypothesis hconv.

The wall (precisely pinned — why hconv is not unconditional)

hconv is the conjunction of two facts, both of which fail det-free for singular cocycles:

1. The slow projectors converge at all. orthProjMatrix (vSlowSingularStep A T c n x) = 1 − bandProjector A T (𝟙_{(c,∞)}) n x (orthProjMatrix_vSlowSingularStep), so their convergence is exactly the fast band-projector convergence. By Oseledets.bandProjector_increment_eq_aperture (SingularSlowSpaceUnconditional.lean) the per-step band increment ‖Pₙ₊₁ − Pₙ‖ is the aperture ‖V Vᵀ − U Uᵀ‖ between the top-k right-singular frames of cocycle n x and cocycle (n+1) x = B·(cocycle n x), B = A(Tⁿx); Davis–Kahan governs it by the condition number of the single step B (the inverse ‖(compound k B)⁻¹‖), not by any forward singular ratio. A single rank-dropping step (σ_k(B) = 0, allowed when det B = 0) makes the increment O(1), breaking summability. This is the Cauchy/aperture wall, already proved walled (bandProjector_increment_eq_aperture).

2. The limit is the lambdaBar-sublevel. Even granting convergence, identifying the limit slow space with {lambdaBar ≤ c} is the per-vector spectral upper bound Oseledets.limsup_le_of_mem_vslow (vslow ⊆ lambdaSublevel, Oseledets/Lyapunov/LimitSlowSpaceSpectralBound.lean), whose only route is the full Ruelle Lemma 1.4 cofactor chain on the orthogonal change of basis between the time-n Gram eigenbasis and the limit eigenbasis of Λ = oseledetsLimit — and Λ itself exists only for invertible cocycles (tendsto_oseledetsLimit carries hA : ∀ x, (A x).det ≠ 0), because the per-σ exponent limit tendsto_log_singularValue needs every σ_i > 0 (singularValues_cocycle_pos hA, sprod_pos hA). A singular cocycle's bottom singular values hit 0, log 0 is junk, and the renormalized eigenvalues at the bottom do not converge.

So hconv is supplied — and {v : lambdaBar ≤ c} is measurable — exactly on the tempered class where the compound condition number is subexponential (tendsto_vSlowSingularStep_of_tempered, SingularSlowSpaceUnconditional.lean, which delivers the convergence half of hconv, modulo the limit-identification half), and the unconditional case stays walled at the aperture (bandProjector_increment_eq_aperture) and at the Λ-eigenbasis (the missing Mathlib fact: continuity of sorted Hermitian eigenvalues/eigenvectors and a normalized renormalized-Gram limit for singular matrices — neither in Mathlib, and the latter mathematically false at the kernel stratum where the limsup growth is 0, not −∞).

Main results

• Oseledets.measurableSubspace_of_tendsto_orthProjMatrix — soft pointwise-limit measurability of a subspace family (general, reusable).
• Oseledets.measurableSubspace_lambdaSublevel_of_tendsto — the det-free reduction of {v : lambdaBar ≤ c} measurability to the slow-projector convergence-to-the-sublevel hconv.
• Oseledets.orthProjMatrix_vSlowSingularStep_tendsto_iff_lambdaSublevel — hconv is equivalent to the convergence of the finite-step slow projectors to orthProjMatrix (lambdaSublevel A T x c), re-stated through the complement bridge 1 − bandProjector to expose the aperture wall.

References

• A. Quas, Multiplicative Ergodic Theorems and Applications (Theorem 2, §3.1).
• D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), Lemma 1.4.
• C. Davis, W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM J. Numer. Anal. 7 (1970), 1–46.

The general soft lemma: pointwise-limit measurability of a subspace family

A subspace family is a MeasurableSubspace whenever its orthProjMatrix is, for every base point, the pointwise (in the sequence index) limit of a sequence of measurable matrix-valued families. This is the entrywise measurable_of_tendsto_metrizable template, identical in shape to Oseledets.MeasurableSubspace.inf and Oseledets.measurable_orthProjMatrix_eventualKer; we isolate it so any convergent measurable projector sequence yields measurability of its limit subspace.

theorem Oseledets.measurableSubspace_of_tendsto_orthProjMatrix {X : Type u_1} [MeasurableSpace X] {d : ℕ} (V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))) (P : ℕ → X → Matrix (Fin d) (Fin d) ℝ) (hP : ∀ (n : ℕ), Measurable (P n)) (hconv : ∀ (x : X), Filter.Tendsto (fun (n : ℕ) => P n x) Filter.atTop (nhds (orthProjMatrix (V x)))) : MeasurableSubspace V

Pointwise-limit measurability of a subspace family. If V : X → Submodule … and there is a sequence P : ℕ → X → Matrix (Fin d) (Fin d) ℝ of measurable matrix families with, for every x, P n x → orthProjMatrix (V x) along atTop, then MeasurableSubspace V. The projector matrix of each V x is the pointwise limit of the measurable P n, so it is measurable entrywise (measurable_of_tendsto_metrizable).

The det-free reduction for the lambdaBar-sublevel slow space

The finite-step slow approximants vSlowSingularStep A T c n x have everywhere-measurable projector matrices (measurableSubspace_vSlowSingularStep, unconditional). Feeding them into the soft lemma reduces measurability of {v : lambdaBar A T x v ≤ c} = lambdaSublevel A T x c to a single hypothesis: that those finite-step projectors converge, for every x, to the projector of the sublevel.

theorem Oseledets.measurableSubspace_lambdaSublevel_of_tendsto {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : Measurable A) {T : X → X} (hT : Measurable T) (c : ℝ) (hconv : ∀ (x : X), Filter.Tendsto (fun (n : ℕ) => orthProjMatrix (vSlowSingularStep A T c n x)) Filter.atTop (nhds (orthProjMatrix (lambdaSublevel A T x c)))) : MeasurableSubspace fun (x : X) => lambdaSublevel A T x c

Det-free reduction of {lambdaBar ≤ c} measurability. If, for every x, the finite-step slow projectors orthProjMatrix (vSlowSingularStep A T c n x) converge to orthProjMatrix (lambdaSublevel A T x c), then x ↦ lambdaSublevel A T x c — the lambdaBar-sublevel slow space {v : lambdaBar A T x v ≤ c} — is a MeasurableSubspace. No det ≠ 0. The finite-step projectors are measurable per n unconditionally (measurableSubspace_vSlowSingularStep), so the conclusion follows from the pointwise-limit soft lemma measurableSubspace_of_tendsto_orthProjMatrix. The convergence hypothesis hconv is the genuine residual: it is the band-projector convergence (the aperture wall, bandProjector_increment_eq_aperture) together with the limit being the sublevel (the spectral upper bound limsup_le_of_mem_vslow); both are supplied only on the tempered class.

Exposing the aperture wall inside hconv

The complement bridge orthProjMatrix (vSlowSingularStep A T c n x) = 1 − bandProjector … (orthProjMatrix_vSlowSingularStep) re-states hconv as the convergence of 1 − bandProjector to the sublevel projector, equivalently of the fast band projector to its complement. This makes visible that the convergence half of hconv is the band-projector convergence whose per-step increment is the aperture between consecutive top-k singular frames (bandProjector_increment_eq_aperture), the precise quantity the inverse (condition number of the single step) is load-bearing for.

theorem Oseledets.orthProjMatrix_vSlowSingularStep_tendsto_iff_bandProjector {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (x : X) : Filter.Tendsto (fun (n : ℕ) => orthProjMatrix (vSlowSingularStep A T c n x)) Filter.atTop (nhds (orthProjMatrix (lambdaSublevel A T x c))) ↔ Filter.Tendsto (fun (n : ℕ) => bandProjector A T ((Set.Ioi c).indicator 1) n x) Filter.atTop (nhds (1 - orthProjMatrix (lambdaSublevel A T x c)))

hconv through the complement bridge. For every x, the finite-step slow projectors converge to orthProjMatrix (lambdaSublevel A T x c) iff the complements 1 − bandProjector A T (𝟙_{(c,∞)}) n x do — i.e. iff the fast band projectors converge to 1 − orthProjMatrix (lambdaSublevel A T x c). This re-expresses the residual convergence input of measurableSubspace_lambdaSublevel_of_tendsto directly on the fast band, where its per-step increment is the aperture bandProjector_increment_eq_aperture governed by the condition number of the step B = A(Tⁿx) (the inverse), pinning why it is not summable for a singular step.