Measurability infrastructure for the Lyapunov filtration

This module develops the measurability tools for the Oseledets flag. The measurability of the flag is established through the concrete continuous-functional-calculus spectral projections of the Oseledets limit operator Λ x = lim_n ((A⁽ⁿ⁾)ᵀ A⁽ⁿ⁾)^{1/(2n)}, rather than through a measurable selection of an orthonormal frame for the abstract sublevel subspace (which would require a Kuratowski–Ryll-Nardzewski selection theorem).

Defining the i-th flag projection as the CFC element Pᵢ x := cfc gᵢ (Λ x) (with gᵢ a continuous gap function) makes orthProjMatrix (range (toEuclideanCLM (Pᵢ x))) = Pᵢ x definitionally — a self-adjoint idempotent equals the orthogonal projection onto its range — so MeasurableSubspace reduces to measurability of x ↦ cfc gᵢ (Λ x).

Main results

• Oseledets.measurable_lambdaBar_apply — for fixed v, x ↦ lambdaBar A T x v is measurable (the scalar measurability used by the later arguments).
• Oseledets.orthProjMatrix_apply / Oseledets.measurable_orthProjMatrix_iff — the projection matrix's entry formula and the resulting reduction of matrix measurability to projecting the fixed standard basis vectors.
• Oseledets.instMeasurableAdd₂Matrix, Oseledets.measurable_matrix_pow, Oseledets.measurable_aeval_matrix — matrix-algebra measurability (a polynomial in a measurable matrix is measurable).
• Oseledets.measurable_cfc_eqOn_polynomial — if a fixed polynomial q agrees with g on the spectrum of every (self-adjoint) M x, then x ↦ cfc g (M x) is measurable. This polynomial bypass uses only the bare Hermitian CFC instance, not the (absent for real matrices) IsometricContinuousFunctionalCalculus.
• Oseledets.measurable_cfc_continuous — for a continuous f and a measurable family of self-adjoint matrices M, x ↦ cfc f (M x) is measurable, via a per-point Weierstrass approximation.

The terminal MeasurableSubspace lemma for the concrete flag is assembled once the Oseledets limit Λ is available (in Oseledets.Lyapunov.OseledetsLimit), since it needs Measurable Λ and the fixed Lyapunov spectrum on which the gap function is interpolated by a polynomial.

@[implicit_reducible]

instance Oseledets.instMeasurableSpaceEuclideanSpace {d : ℕ} : MeasurableSpace (EuclideanSpace ℝ (Fin d))

The Borel measurable structure on EuclideanSpace ℝ (Fin d) (a metric space). Used to make sense of EuclideanSpace-valued measurable maps below.

Implementation note: this is the borel _ σ-algebra. It is propositionally equal to — but a syntactically different term from — Mathlib's own WithLp.measurableSpace on the same type. We therefore register borel _ explicitly here and pin the BorelSpace witness as ⟨rfl⟩ below (the rfl is exactly the definitional MeasurableSpace = borel _ this instance makes hold by fiat), so that downstream MeasurableSpace/BorelSpace typeclass resolution stays on a single coherent term and the Borel-measurability lemmas apply without coercion friction.

Equations

• Oseledets.instMeasurableSpaceEuclideanSpace = borel (EuclideanSpace ℝ (Fin d))

instance Oseledets.instBorelSpaceEuclideanSpace {d : ℕ} : BorelSpace (EuclideanSpace ℝ (Fin d))

Scalar measurability

theorem Oseledets.measurable_lambdaBar_apply {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} {d : ℕ} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hAmeas : Measurable A) (v : EuclideanSpace ℝ (Fin d)) : Measurable fun (x : X) => lambdaBar A T x v

For a fixed vector v, the upper Lyapunov growth x ↦ lambdaBar A T x v is measurable: it is the limsup of the measurable sequence x ↦ n⁻¹ · log ‖toEuclideanCLM (cocycle A T n x) v‖.

The projection-matrix entry formula and reduction

theorem Oseledets.orthProjMatrix_apply {d : ℕ} (K : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (i j : Fin d) : orthProjMatrix K i j = (K.starProjection (EuclideanSpace.single j 1)).ofLp i

Entry formula for the projection matrix. The (i, j) entry of orthProjMatrix K equals the i-th coordinate of the orthogonal projection K.starProjection applied to the standard basis vector EuclideanSpace.single j 1.

theorem Oseledets.measurable_orthProjMatrix_iff {X : Type u_1} [MeasurableSpace X] {d : ℕ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} : (Measurable fun (x : X) => orthProjMatrix (V x)) ↔ ∀ (j : Fin d), Measurable fun (x : X) => (V x).starProjection (EuclideanSpace.single j 1)

The reduction. x ↦ orthProjMatrix (V x) is measurable iff for every standard basis index j, the EuclideanSpace-valued map x ↦ (V x).starProjection (single j 1) is measurable.

Matrix-algebra measurability (a polynomial in a measurable matrix is measurable)

instance Oseledets.instMeasurableAdd₂Matrix {m : Type u_2} {α : Type u_3} [MeasurableSpace α] [Add α] [MeasurableAdd₂ α] : MeasurableAdd₂ (Matrix m m α)

Matrix addition is measurable in both arguments (entrywise Pi addition); the additive counterpart of Oseledets.instMeasurableMul₂Matrix.

theorem Oseledets.measurable_matrix_pow {d : ℕ} (n : ℕ) : Measurable fun (a : Matrix (Fin d) (Fin d) ℝ) => a ^ n

a ↦ a ^ n is measurable in the matrix a (iterated measurable multiplication).

theorem Oseledets.measurable_aeval_matrix {d : ℕ} (q : Polynomial ℝ) : Measurable fun (a : Matrix (Fin d) (Fin d) ℝ) => (Polynomial.aeval a) q

a ↦ aeval a q is measurable in the matrix a: a polynomial built from +, •, * of the (measurable) identity, using the matrix MeasurableMul₂/MeasurableAdd₂ instances.

Measurability of the CFC via a fixed interpolating polynomial

theorem Oseledets.measurable_cfc_eqOn_polynomial {X : Type u_1} [MeasurableSpace X] {d : ℕ} (g : ℝ → ℝ) (q : Polynomial ℝ) (M : X → Matrix (Fin d) (Fin d) ℝ) (hM : Measurable M) (hMsa : ∀ (x : X), IsSelfAdjoint (M x)) (hagree : ∀ (x : X), Set.EqOn g (fun (x : ℝ) => Polynomial.eval x q) (spectrum ℝ (M x))) : Measurable fun (x : X) => cfc g (M x)

The CFC polynomial bypass. Let M : X → Matrix (Fin d) (Fin d) ℝ be measurable with each M x self-adjoint (Hermitian). Suppose a fixed polynomial q agrees with g : ℝ → ℝ on the spectrum of every M x. Then x ↦ cfc g (M x) is measurable.

This is the situation in the intended application: M x = Λ x (the a.e.-existing Oseledets limit matrix, measurable as a limit of measurable matrices), g = gᵢ the continuous gap function, and on the a.e. good set the spectrum is the fixed gapped Lyapunov set, on which gᵢ equals an interpolating polynomial q. It uses only the bare Hermitian CFC instance — no IsometricContinuousFunctionalCalculus (which does not synthesize for real matrices), no continuousOn_cfc, no measurable selection, no analytic sets.

Measurability of the CFC for a continuous function (Weierstrass bypass)

The polynomial bypass measurable_cfc_eqOn_polynomial needs a single polynomial agreeing with g on the spectrum of every M x. For the Oseledets root t ↦ t^{1/(2n)} the spectra (the squared singular values) range over an unbounded family, so no single polynomial works globally. The remedy is a per-point Weierstrass approximation: for each k pick a polynomial qₖ agreeing with g to within 1/(k+1) on the compact interval [-k, k]. For a fixed x the (finite) spectrum of M x lies in some [-R, R], so qₖ → g uniformly on spectrum (M x), whence cfc qₖ (M x) → cfc g (M x) by tendsto_cfc_fun. Each x ↦ cfc qₖ (M x) = aeval (M x) qₖ is measurable, and matrix-entrywise measurable_of_tendsto_metrizable upgrades the pointwise limit to measurability of x ↦ cfc g (M x). This needs only the bare Hermitian CFC instance (the generic tendsto_cfc_fun, not the absent-for-real-matrices isometric CFC).

theorem Oseledets.exists_poly_approx (f : ℝ → ℝ) (hf : Continuous f) (k : ℕ) : ∃ (q : Polynomial ℝ), ∀ t ∈ Set.Icc (-↑k) ↑k, |Polynomial.eval t q - f t| ≤ 1 / (↑k + 1)

Weierstrass polynomial approximation on [-k, k]. For a continuous f : ℝ → ℝ and each k : ℕ there is a polynomial q with |q(t) − f(t)| ≤ 1/(k+1) on [-k, k].

theorem Oseledets.exists_spectrum_subset_Icc {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) : ∃ (R : ℝ), spectrum ℝ M ⊆ Set.Icc (-R) R

The spectrum of a matrix is finite, hence contained in some symmetric interval [-R, R].

theorem Oseledets.continuous_matrix_entry {d : ℕ} (i j : Fin d) : Continuous fun (M : Matrix (Fin d) (Fin d) ℝ) => M i j

Continuity of the matrix-entry projection in the (L2 operator) matrix metric topology (a linear functional on a finite-dimensional space).

theorem Oseledets.measurable_cfc_continuous {X : Type u_1} [MeasurableSpace X] {d : ℕ} (f : ℝ → ℝ) (hf : Continuous f) (M : X → Matrix (Fin d) (Fin d) ℝ) (hM : Measurable M) (hMsa : ∀ (x : X), IsSelfAdjoint (M x)) : Measurable fun (x : X) => cfc f (M x)

Continuous functional calculus of a measurable self-adjoint matrix family. If M : X → Matrix (Fin d) (Fin d) ℝ is measurable with each M x self-adjoint, and f : ℝ → ℝ is continuous, then x ↦ cfc f (M x) is measurable. Proved by the per-point Weierstrass approximation described above.