The Jankov–von Neumann uniformization theorem

A uniformization of a relation R ⊆ X × Y is a function f : X → Y whose graph lies in R over the projection of R: (x, f x) ∈ R whenever (x, y) ∈ R for some y. Even a closed relation between Polish spaces need not have a Borel measurable uniformization, but the Jankov–von Neumann theorem shows that every analytic relation has a uniformization which is measurable for the σ-algebra generated by the analytic subsets of X. By Lusin's theorem that σ-algebra lies in the completion of every s-finite measure μ on X, so the uniformization agrees μ-almost everywhere with a function measurable for the given σ-algebra on X (which contains the open sets; when it is the Borel σ-algebra, this function is Borel measurable), and that function is itself a uniformization of R at μ-almost every point of the projection.

This is the measurable selection theorem for a choice depending on a parameter, when the admissible pairs of parameter and choice form an analytic set, for instance a closed or Borel one: say a geodesic joining two points of a Polish geodesic space, chosen measurably in the pair of endpoints relative to a fixed law of the endpoints.

Proof

Write the analytic relation as the range of a continuous map g : (ℕ → ℕ) → X × Y, and let p : (ℕ → ℕ) → X be its first component, so that the projection of R is the range of p. For x in that range the fibre p ⁻¹' {x} is a nonempty closed subset of Baire space, and the uniformization sends x to the second component of g at the lexicographically least point of that fibre. Whether the least point has prescribed first n + 1 coordinates is decided by whether x lies in the images under p of finitely many cylinders: those images are analytic, and the coordinates of the least point are therefore measurable for the σ-algebra generated by analytic sets.

Main results

• MeasureTheory.AnalyticSet.exists_measurable_uniformization: the Jankov–von Neumann uniformization theorem, for an analytic relation R ⊆ X × Y with X a T₁ space.
• MeasureTheory.AnalyticSet.exists_measurable_ae_uniformization: relative to an s-finite measure μ on a metrizable space X, an analytic relation has a uniformization at μ-almost every point of its projection that is measurable for the given σ-algebra on X.

References

• A. S. Kechris, Classical Descriptive Set Theory, Springer-Verlag, 1995, Theorem 18.1.
• S. M. Srivastava, A Course on Borel Sets, Springer-Verlag, 1998, Theorem 5.5.2.

theorem MeasureTheory.AnalyticSet.exists_measurable_uniformization {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] [MeasurableSpace Y] [BorelSpace Y] [Nonempty Y] {R : Set (X × Y)} (hR : AnalyticSet R) : ∃ (f : X → Y), Measurable f ∧ ∀ x ∈ Prod.fst '' R, (x, f x) ∈ R

The Jankov–von Neumann uniformization theorem. An analytic relation R ⊆ X × Y, with X a T₁ space, has a uniformization f : X → Y which is measurable for the σ-algebra generated by the analytic subsets of X: (x, f x) ∈ R for every x in the projection of R.

By TauCeti.MeasureTheory.nullMeasurable_of_measurable_generateFrom_analyticSet, such an f is null-measurable for every s-finite measure on a metrizable X; see MeasureTheory.AnalyticSet.exists_measurable_ae_uniformization.

theorem MeasureTheory.AnalyticSet.exists_measurable_ae_uniformization {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace.MetrizableSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [MeasurableSpace Y] [BorelSpace Y] [MeasurableSpace.CountablyGenerated Y] [Nonempty Y] {R : Set (X × Y)} (hR : AnalyticSet R) (μ : Measure X) [SFinite μ] : ∃ (g : X → Y), Measurable g ∧ ∀ᵐ (x : X) ∂μ, x ∈ Prod.fst '' R → (x, g x) ∈ R

Measurable uniformization almost everywhere. Relative to an s-finite measure μ on a metrizable space X, an analytic relation R ⊆ X × Y has a measurable uniformization at almost every point of its projection: a g : X → Y, measurable for the given σ-algebra on X (which contains the open sets, and is the Borel σ-algebra under [BorelSpace X]), with (x, g x) ∈ R for μ-almost every x in the projection of R.

The function g depends on μ; a uniformization that works for every μ at once is MeasureTheory.AnalyticSet.exists_measurable_uniformization, which is measurable only for the σ-algebra generated by analytic sets.