The projector/range bridge for MeasurableSubspace

This module connects a self-adjoint idempotent matrix P to the MeasurableSubspace notion of Oseledets/Lyapunov/MeasurableSubspace.lean.

The key observation is purely linear-algebraic: if P is self-adjoint (Pᵀ = P, i.e. IsSelfAdjoint P) and idempotent (P * P = P), then the continuous linear map toEuclideanCLM P is a star projection (self-adjoint idempotent operator), hence equals the orthogonal projection starProjection onto its own range. Translating back through the toEuclideanCLM star-algebra equivalence shows orthProjMatrix (range (toEuclideanCLM P)) = P.

Consequently a measurable family of self-adjoint idempotent matrices induces a MeasurableSubspace family of range subspaces — the form consumed downstream by the spectral (CFC) construction of the Oseledets flag projections.

Main results

• orthProjMatrix_range_toEuclideanCLM — the projector/range bridge: for a self-adjoint idempotent P, the orthogonal-projection matrix of the range of toEuclideanCLM P is P.
• measurableSubspace_range_of_measurable — a measurable family of self-adjoint idempotent matrices induces a MeasurableSubspace family of range subspaces.

The crux uses the Mathlib lemma ContinuousLinearMap.isStarProjection_iff_eq_starProjection_range (a star projection equals the orthogonal projection onto its range).

theorem Oseledets.orthProjMatrix_range_toEuclideanCLM {d : ℕ} (P : Matrix (Fin d) (Fin d) ℝ) (hsa : IsSelfAdjoint P) (hidem : P * P = P) : orthProjMatrix (↑(Matrix.toEuclideanCLM P)).range = P

For a self-adjoint idempotent matrix P (IsSelfAdjoint P, P * P = P), the orthogonal projection onto the range of toEuclideanCLM P is toEuclideanCLM P itself, so orthProjMatrix (range …) = P.

theorem Oseledets.measurableSubspace_range_of_measurable {d : ℕ} {X : Type u_1} [MeasurableSpace X] (P : X → Matrix (Fin d) (Fin d) ℝ) (hP : Measurable P) (hsa : ∀ (x : X), IsSelfAdjoint (P x)) (hidem : ∀ (x : X), P x * P x = P x) : MeasurableSubspace fun (x : X) => (↑(Matrix.toEuclideanCLM (P x))).range

If x ↦ P x is a measurable family of self-adjoint idempotent matrices, the range subspaces form a MeasurableSubspace.