Measurability of the intersection subbundle

For the two-sided Oseledets splitting one forms, at each point, the intersection K ⊓ L of a forward subspace K and a backward subspace L. This module shows that the assignment x ↦ K x ⊓ L x is a MeasurableSubspace whenever K and L are.

The route avoids any von Neumann alternating-projection theorem (absent from Mathlib). Writing P_K, P_L for the orthogonal projections, the self-adjoint contraction S := P_K P_L P_K satisfies S v = v ↔ v ∈ K ⊓ L, its eigenvalues lie in [0, 1], and cⁿ → 0 for c ∈ [0, 1). Hence the operator powers Sⁿ converge to the orthogonal projection onto the intersection, and the matrix powers (orthProjMatrix K · orthProjMatrix L · orthProjMatrix K)ⁿ converge entrywise to orthProjMatrix (K ⊓ L). Entrywise measurability of the powers and measurable_of_tendsto_metrizable then assemble the MeasurableSubspace statement, exactly as the continuous-functional-calculus measurability arguments in Oseledets.Lyapunov.Measurable.

Main results

• Oseledets.inner_projComp_eq — ⟪v, P_K (P_L (P_K v))⟫ = ‖P_L (P_K v)‖².
• Oseledets.one_eigenspace_projComp — P_K (P_L (P_K v)) = v ↔ v ∈ K ⊓ L.
• Oseledets.tendsto_pow_orthProj_inf — the matrix powers of P_K P_L P_K tend to the projection matrix onto K ⊓ L.
• Oseledets.MeasurableSubspace.inf — x ↦ K x ⊓ L x is a MeasurableSubspace.

The self-adjoint contraction P_K P_L P_K and its fixed points

theorem Oseledets.inner_projComp_eq {d : ℕ} (K L : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (v : EuclideanSpace ℝ (Fin d)) : inner ℝ v (K.starProjection (L.starProjection (K.starProjection v))) = ‖L.starProjection (K.starProjection v)‖ ^ 2

The key inner-product identity. For orthogonal projections P_K, P_L, ⟪v, P_K (P_L (P_K v))⟫ = ‖P_L (P_K v)‖². This makes S := P_K P_L P_K positive semidefinite and identifies its quadratic form.

theorem Oseledets.one_eigenspace_projComp {d : ℕ} (K L : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (v : EuclideanSpace ℝ (Fin d)) : K.starProjection (L.starProjection (K.starProjection v)) = v ↔ v ∈ K ⊓ L

Fixed points of S = P_K P_L P_K are exactly K ⊓ L. P_K (P_L (P_K v)) = v ↔ v ∈ K ⊓ L. The forward direction uses the norm chain ‖v‖² = ‖P_L (P_K v)‖² ≤ ‖P_K v‖² ≤ ‖v‖² forced to be an equality, hence each projection fixes v.

The operator toEuclideanCLM (P_K P_L P_K)

Eigendata of S = P_K P_L P_K

Convergence of the operator powers

Matrix-power convergence and the measurable intersection

theorem Oseledets.tendsto_pow_orthProj_inf {d : ℕ} (K L : Submodule ℝ (EuclideanSpace ℝ (Fin d))) : Filter.Tendsto (fun (n : ℕ) => (orthProjMatrix K * orthProjMatrix L * orthProjMatrix K) ^ n) Filter.atTop (nhds (orthProjMatrix (K ⊓ L)))

The matrix powers of P_K P_L P_K converge to the projection onto K ⊓ L. (orthProjMatrix K · orthProjMatrix L · orthProjMatrix K)ⁿ → orthProjMatrix (K ⊓ L) (entrywise). This is the von Neumann alternating-projection limit, obtained from the operator-power convergence tendsto_pow_projComp_apply by reading off coordinates of the standard basis vectors.

theorem Oseledets.MeasurableSubspace.inf {d : ℕ} {X : Type u_1} [MeasurableSpace X] {K L : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hK : MeasurableSubspace K) (hL : MeasurableSubspace L) : MeasurableSubspace fun (x : X) => K x ⊓ L x

The intersection of two measurable subspace families is measurable. If K and L are MeasurableSubspaces, then so is x ↦ K x ⊓ L x. The projection matrix onto K x ⊓ L x is the entrywise limit of the measurable matrix powers (orthProjMatrix (K x) · orthProjMatrix (L x) · orthProjMatrix (K x))ⁿ, so measurable_of_tendsto_metrizable applies entrywise.