Measurable families of subspaces

Mathlib has no measurable structure on Submodule/Module.Grassmannian/Flag, so we introduce a notion of a measurably-varying subspace.

A subspace K ≤ EuclideanSpace ℝ (Fin d) is encoded by the matrix of its orthogonal projection orthProjMatrix K, and a subspace-valued map V : X → Submodule … is declared MeasurableSubspace when x ↦ orthProjMatrix (V x) is measurable (matrices carry the Pi/Borel measurable structure, Oseledets.instMeasurableSpaceMatrix).

The lemmas relating this notion to spans, sums, and selections are developed in Oseledets.Lyapunov.Measurable.

Main definitions

• Oseledets.orthProjMatrix: the matrix of the orthogonal projection of EuclideanSpace ℝ (Fin d) onto a subspace.
• Oseledets.MeasurableSubspace: a subspace-valued map is measurable iff its orthogonal-projection matrix is.

noncomputable def Oseledets.orthProjMatrix {d : ℕ} (K : Submodule ℝ (EuclideanSpace ℝ (Fin d))) : Matrix (Fin d) (Fin d) ℝ

The matrix of the orthogonal projection of EuclideanSpace ℝ (Fin d) onto K. A subspace is determined by this matrix, which lives in a space with a measurable structure, so it is the vehicle for "measurably-varying subspace".

Equations

• Oseledets.orthProjMatrix K = Matrix.toEuclideanCLM.symm K.starProjection

def Oseledets.MeasurableSubspace {X : Type u_1} [MeasurableSpace X] {d : ℕ} (V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))) : Prop

A family of subspaces V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d)) depends measurably on x iff its orthogonal-projection matrix does.

Equations

• Oseledets.MeasurableSubspace V = Measurable fun (x : X) => Oseledets.orthProjMatrix (V x)