Documentation

Oseledets.Singular.MeasurableProjection

Weak measurability of a subspace family from its measurable graph #

This module discharges the last genuinely measure-theoretic node of the singular ("issue #6") multiplicative ergodic theorem: from a measurable graph {(x, v) | v ∈ V x} of a subspace-valued family V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d)) over a standard Borel base X, the scalar distance maps x ↦ infDist c (V x) are μ-a.e. measurable (AEMeasurable). This is exactly the weak-measurability hypothesis consumed by the (sorry-free) polarisation converter of Oseledets.Singular.StarProjectionPolar (Oseledets.starProjection_apply_coord), now in its a.e. form.

The route: projection of a Borel set is analytic, analytic sets are universally measurable #

The sublevel set splits as a projection of the graph: {x | infDist c (V x) < r} = Prod.fst '' ({(x, v) | v ∈ V x} ∩ (Set.univ ×ˢ Metric.ball c r)) (infDist_lt_iff, using 0 ∈ V x for nonemptiness). The right-hand side is the image, under the continuous projection Prod.fst : X × EuclideanSpace ℝ (Fin d) → X, of a measurable subset of the standard Borel product X × EuclideanSpace ℝ (Fin d). By the Lusin–Souslin machinery in Mathlib (MeasurableSet.analyticSet_image) such an image is an analytic set.

Analytic sets in a standard Borel space are universally measurable: each is NullMeasurableSet with respect to (the completion of) every s-finite measure — the classical theorem of Lusin via Choquet capacitability. Mathlib has the analytic-set API but not this universal-measurability theorem (AnalyticSet.measurableSet_of_compl only delivers measurability for analytic sets whose complement is also analytic — Suslin's theorem — which does not apply to a projection in general). This fact is now proved in Oseledets.MeasureTheory.AnalyticUniversallyMeasurable (MeasureTheory.AnalyticSet.nullMeasurableSet, via the Choquet capacity machinery), and consumed here through nullMeasurableSet_infDist_lt.

Granted that classical fact, every sublevel set is NullMeasurableSet, hence x ↦ infDist c (V x) is NullMeasurable (via measurable_of_Iio on the NullMeasurableSpace σ-algebra), hence AEMeasurable (NullMeasurable.aemeasurable, ℝ being countably generated). This is the correct a.e. formulation for the (a.e.) multiplicative ergodic theorem.

Why this is the right reduction #

infDist c (V x) = ‖c − (V x).starProjection c‖ (Oseledets.infDist_eq_norm_sub_starProjection), so the weak measurability proved here is interderivable with measurability of the orthogonal projector itself: the node is irreducible, and reducing it to one universally-true classical measure-theory lemma (analytic ⟹ universally measurable) is the sharpest possible isolation — strictly tighter than the Arsenin–Kunugui "σ-compact sections" route, which the present analytic argument bypasses entirely.

Main results #

Literature: N. Lusin, Leçons sur les ensembles analytiques (1930); G. Choquet, Theory of capacities (1953); S. M. Srivastava, A Course on Borel Sets, Thm 4.3.1 (every analytic set is universally measurable). C. González-Tokman, A. Quas, A semi-invertible operator Oseledets theorem (ETDS 2014), Appendix B.

The sublevel set is the projection of the graph, hence analytic #

source
theorem Oseledets.image_fst_graph_inter_ball {X : Type u_1} {d : ℕ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (c : EuclideanSpace ℝ (Fin d)) (r : ℝ) :
{x : X | Metric.infDist c ↑(V x) < r} = Prod.fst '' ({p : X × EuclideanSpace ℝ (Fin d) | p.2 ∈ V p.1} ∩ Set.univ ×ˢ Metric.ball c r)

The distance sublevel set is the projection of the graph through a ball. For any c and r, {x | infDist c (V x) < r} equals the projection onto X of the graph intersected with the slab univ ×ˢ ball c r. The membership equivalence is Metric.infDist_lt_iff (the section V x is nonempty as 0 ∈ V x), turning infDist c (V x) < r into the existence of a graph point v ∈ V x with v ∈ ball c r.

source
theorem Oseledets.analyticSet_infDist_lt {X : Type u_1} [MeasurableSpace X] {d : ℕ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} [TopologicalSpace X] [PolishSpace X] [BorelSpace X] (hgraph : MeasurableSet {p : X × EuclideanSpace ℝ (Fin d) | p.2 ∈ V p.1}) (c : EuclideanSpace ℝ (Fin d)) (r : ℝ) :
MeasureTheory.AnalyticSet {x : X | Metric.infDist c ↑(V x) < r}

A measurable graph makes the distance sublevel set analytic. Over a standard Borel base X, if the graph {(x, v) | v ∈ V x} is measurable then {x | infDist c (V x) < r} is an AnalyticSet. By image_fst_graph_inter_ball it is the image, under the continuous projection Prod.fst, of a measurable subset of the standard Borel product X × EuclideanSpace ℝ (Fin d); MeasurableSet.analyticSet_image (Lusin–Souslin) makes the continuous image of a Borel set analytic.

Assembling a.e. weak measurability #

source
theorem Oseledets.nullMeasurableSet_infDist_lt {X : Type u_1} [MeasurableSpace X] {d : ℕ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} [TopologicalSpace X] [PolishSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] (hgraph : MeasurableSet {p : X × EuclideanSpace ℝ (Fin d) | p.2 ∈ V p.1}) (c : EuclideanSpace ℝ (Fin d)) (r : ℝ) :
MeasureTheory.NullMeasurableSet {x : X | Metric.infDist c ↑(V x) < r} μ

The distance sublevel sets are null measurable. Combining analyticSet_infDist_lt with the universal measurability of analytic sets MeasureTheory.AnalyticSet.nullMeasurableSet (Oseledets.MeasureTheory.AnalyticUniversallyMeasurable, via Choquet capacitability) for any s-finite μ.

source
theorem Oseledets.aemeasurable_infDist_of_measurableGraph {X : Type u_1} [MeasurableSpace X] {d : ℕ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} [TopologicalSpace X] [PolishSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] (hgraph : MeasurableSet {p : X × EuclideanSpace ℝ (Fin d) | p.2 ∈ V p.1}) (c : EuclideanSpace ℝ (Fin d)) :
AEMeasurable (fun (x : X) => Metric.infDist c ↑(V x)) μ

A measurable graph yields a.e. weak measurability (the deliverable, a.e. form). Over a standard Borel base X and for every s-finite measure μ (in particular every finite/probability measure, e.g. the measure of the multiplicative ergodic theorem), a measurable graph {(x, v) | v ∈ V x} makes x ↦ infDist c (V x) AEMeasurable for every c.

Each Iio-preimage {x | infDist c (V x) < r} is NullMeasurableSet (nullMeasurableSet_infDist_lt); measurable_of_Iio over the NullMeasurableSpace σ-algebra upgrades this to NullMeasurable (fun x => infDist c (V x)) μ, and NullMeasurable.aemeasurable (ℝ countably generated) to AEMeasurable. This is the a.e. analogue of pointwise weak measurability (x ↦ infDist c (V x) measurable), the correct hypothesis for the a.e. multiplicative ergodic theorem.