Measurability of the orthogonal projector onto the finite-step cocycle kernel

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), whose bottom space is the eventual kernel ⨆ n, cocycleKer A T n x. Quas' Theorem 2 demands a measurable choice of each flag space; a robust way to make a subspace-valued map x ↦ K x measurable, used throughout this development, is to show that its orthogonal-projection matrix x ↦ orthProjMatrix (K x) is measurable (the Oseledets.MeasurableSubspace notion of Oseledets.Lyapunov.MeasurableSubspace).

This file delivers exactly that for each fixed step n: the orthogonal projector onto the n-step cocycle kernel — viewed as a subspace cocycleKerEuclid A T n x of the Euclidean space EuclideanSpace ℝ (Fin d) — depends measurably on x. The eventual kernel is the (monotone) union of these finite-step kernels (Oseledets.eventualKer), so this per-step projector measurability is the analytic engine for the measurability of the bottom flag space.

Strategy

The kernel projector is realised spectrally, so its measurability reduces to the already-proven Oseledets.measurable_spectralProjector (no new measurable-selection theorem is needed). Set S x := (cocycle A T n x)ᵀ * (cocycle A T n x). Then:

• S x is Hermitian and positive semidefinite (Matrix.isHermitian_conjTranspose_mul_self, Matrix.posSemidef_conjTranspose_mul_self; for real matrices conjTranspose = transpose), so its spectrum lies in [0, ∞). It is measurable in x (a measurable cocycle composed with the entrywise transpose and the jointly-measurable matrix product, i.e. Oseledets.instMeasurableMul₂Matrix).
• ker S = ker (cocycle A T n x): S v = 0 ↔ ⟪v, S v⟫ = 0 ↔ ‖M v‖² = 0 ↔ M v = 0 (Matrix.inner_toEuclideanCLM, inner_self_eq_zero).
• The orthogonal projector onto ker S is the spectral ≤ 0 projector cfc (Set.indicator (Set.Iic 0) 1) (S x): this continuous-functional-calculus element is a self-adjoint idempotent (because the {0,1}-valued indicator squares to itself on the spectrum), hence a IsStarProjection, and its range is exactly ker S (one inclusion from S * P = 0, since id · indicator (Iic 0) 1 = 0 on [0, ∞); the other from (1 - P) v = (cfc h S) (S v) = 0 for v ∈ ker S, where h is any continuous extension with id · h = indicator (Ioi 0) 1 on the finite spectrum). Identifying orthProjMatrix with cfc via the star-algebra equivalence Matrix.toEuclideanCLM gives the pointwise bridge.

Main definitions

• Oseledets.cocycleKerEuclid: the n-step cocycle kernel transported to a subspace of EuclideanSpace ℝ (Fin d), i.e. LinearMap.ker (Matrix.toEuclideanCLM (cocycle A T n x)).

Main results

• Oseledets.orthProjMatrix_cocycleKerEuclid_eq_spectralProjector: the pointwise bridge orthProjMatrix (cocycleKerEuclid A T n x) = cfc (Set.indicator (Set.Iic 0) 1) (Sᴴ S).
• Oseledets.measurable_orthProjMatrix_cocycleKer: x ↦ orthProjMatrix (cocycleKerEuclid A T n x) is measurable, obtained by rewriting with the bridge and applying Oseledets.measurable_spectralProjector.

Remaining gap toward the measurable equivariant flag

This module makes the projector onto the finite-step kernel measurable. Assembling the full measurable bottom flag space x ↦ eventualKer A T x from these finite-step projectors (the projectors increase to the eventual-kernel projector as n → ∞, by kernel monotonicity), together with the measurability of the intermediate slow spaces V_j(ω) and their exponents from the Kingman/exterior-power machinery, is not carried out here; only the per-step kernel projector is made measurable.

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

The kernel of the n-step cocycle, transported to a subspace of EuclideanSpace ℝ (Fin d) via the star-algebra equivalence Matrix.toEuclideanCLM. This is the Euclidean-space avatar of Oseledets.cocycleKer, packaged so that orthProjMatrix (the orthogonal-projection matrix used by Oseledets.MeasurableSubspace) applies to it directly.

Equations

• Oseledets.cocycleKerEuclid A T n x = (↑(Matrix.toEuclideanCLM (Oseledets.cocycle A T n x))).ker

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

The Gram matrix of the n-step cocycle, (cocycle A T n x)ᵀ * (cocycle A T n x). It is Hermitian and positive semidefinite, and its kernel coincides with the kernel of the cocycle; its spectral ≤ 0 projector is the orthogonal projector onto that kernel.

Equations

• Oseledets.cocycleGram A T n x = (Oseledets.cocycle A T n x).transpose * Oseledets.cocycle A T n x

theorem Oseledets.cocycleGram_isHermitian {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) : (cocycleGram A T n x).IsHermitian

The Gram matrix (cocycle)ᵀ * cocycle is Hermitian (= self-adjoint): for real matrices the conjugate transpose is the transpose, so this is Matrix.isHermitian_conjTranspose_mul_self.

theorem Oseledets.cocycleGram_posSemidef {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) : (cocycleGram A T n x).PosSemidef

The Gram matrix (cocycle)ᵀ * cocycle is positive semidefinite, so its real spectrum lies in [0, ∞). (Matrix.posSemidef_conjTranspose_mul_self; conjTranspose = transpose for reals.)

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

The Gram-matrix family x ↦ (cocycle A T n x)ᵀ * (cocycle A T n x) is measurable: the cocycle is measurable, transpose is entrywise (hence measurable), and matrix multiplication is jointly measurable (Oseledets.instMeasurableMul₂Matrix).

theorem Oseledets.cocycleGram_spectrum_nonneg {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) {s : ℝ} (hs : s ∈ spectrum ℝ (cocycleGram A T n x)) : 0 ≤ s

The real spectrum of the (positive-semidefinite) Gram matrix lies in [0, ∞): any spectral value is nonnegative (StarOrderedRing.nonneg_iff_spectrum_nonneg applied to 0 ≤ Sᵀ S).

theorem Oseledets.ker_toEuclideanCLM_cocycleGram {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) : (↑(Matrix.toEuclideanCLM (cocycleGram A T n x))).ker = cocycleKerEuclid A T n x

Kernel of the Gram matrix = kernel of the cocycle. A vector v of Euclidean space is in the kernel of toEuclideanCLM (Sᵀ S) iff it is in the kernel of toEuclideanCLM S: indeed ⟪v, (Sᵀ S) v⟫ = ⟪S v, S v⟫ = ‖S v‖², which vanishes iff S v = 0.

theorem Oseledets.orthProjMatrix_cocycleKerEuclid_eq_spectralProjector {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) : orthProjMatrix (cocycleKerEuclid A T n x) = cfc ((Set.Iic 0).indicator 1) (cocycleGram A T n x)

The pointwise spectral bridge. The orthogonal-projection matrix onto the n-step cocycle kernel cocycleKerEuclid A T n x equals the spectral ≤ 0 projector cfc (Set.indicator (Set.Iic 0) 1) of the Gram matrix (cocycle A T n x)ᵀ * (cocycle A T n x).

The CFC element P = cfc (indicator (Iic 0) 1) S is a self-adjoint idempotent, hence a IsStarProjection of EuclideanSpace ℝ (Fin d) whose range is the cocycle kernel (range_toEuclideanCLM_kerProj with ker_toEuclideanCLM_cocycleGram); a star projection is the orthogonal projection onto its range (isStarProjection_iff_eq_starProjection_range), and transporting back through the star-algebra equivalence Matrix.toEuclideanCLM recovers orthProjMatrix.

theorem Oseledets.measurable_orthProjMatrix_cocycleKer {X : Type u_1} {d : ℕ} [MeasurableSpace X] [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : Measurable A) {T : X → X} (hT : Measurable T) (n : ℕ) : Measurable fun (x : X) => orthProjMatrix (cocycleKerEuclid A T n x)

Measurability of the finite-step cocycle-kernel projector. For each fixed step n, the orthogonal-projection matrix onto the n-step cocycle kernel cocycleKerEuclid A T n x is measurable in x. By the spectral bridge orthProjMatrix_cocycleKerEuclid_eq_spectralProjector it equals the spectral ≤ 0 projector cfc (indicator (Iic 0) 1) of the measurable, self-adjoint Gram family (cocycle A T n ·)ᵀ * (cocycle A T n ·), whose measurability is Oseledets.measurable_spectralProjector.

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