Analytic sets are universally measurable

This file proves Lusin's universal-measurability theorem: every analytic subset of a metrizable space is measurable after completing any s-finite measure defined on a measurable space containing the Borel sets. Equivalently, it differs from a measurable set by a null set. It also records the generated-measurable-space consequence used by measurable selection.

The core proof is the capacity argument for finite measures. Write an analytic set as the range of a continuous map from Baire space. Successively bound the coordinates in the source while spending a geometric error budget; the image of the resulting compact product captures the range up to arbitrary outer-measure error. A countable union of these inner compact approximations then differs from the analytic set by a null set. For an s-finite measure, apply this construction to each finite component and take the union of the resulting measurable subsets.

The theorem is classically stated for Polish ambient spaces, but neither second countability nor completeness is used. An analytic set is by definition empty or a continuous image of Baire space, so it carries its own separability, and the ambient space is never completed: the argument needs only a metric, to extract a convergent subsequence of approximating points and to identify its limit. Accordingly the three universal-measurability statements below assume just TopologicalSpace.MetrizableSpace. analyticSet_setOf_iInf_lt keeps PolishSpace, which its appeal to measurable projection genuinely needs.

Main results

• TauCeti.MeasureTheory.analyticSet_setOf_iInf_lt: the strict sublevel of a pointwise infimum is analytic when the corresponding set before projection is measurable;
• TauCeti.MeasureTheory.AnalyticSet.nullMeasurableSet: an analytic subset of a metrizable space is null-measurable for every s-finite measure on a measurable space containing the Borel sets;
• TauCeti.MeasureTheory.NullMeasurableSet.of_generateFrom_analyticSet: the same holds for the measurable space generated by analytic sets;
• TauCeti.MeasureTheory.nullMeasurable_of_measurable_generateFrom_analyticSet: a function measurable for that generated measurable space is null-measurable for every such s-finite measure.

Provenance

The proof is adapted from Daniel Lyng's Apache-2.0 Econlib development, Econlib/Math/MeasureTheory/AnalyticNullMeasurable.lean, commit 003655ccf010cdf44c4f67d6675167b54ce0e9df. The implementation is reorganized so that proof-only capacity lemmas are private, while the three reusable consequences remain public.

References

• A. S. Kechris, Classical Descriptive Set Theory, Springer-Verlag, 1995, Theorem 29.7, which states the result for Polish ambient spaces.

theorem TauCeti.MeasureTheory.analyticSet_setOf_iInf_lt {X : Type u_1} {Y : Type u_2} {A : Type u_3} [MeasurableSpace X] [StandardBorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompleteLinearOrder A] (f : X × Y → A) (a : A) (h : MeasurableSet {z : X × Y | f z < a}) : MeasureTheory.AnalyticSet {y : Y | ⨅ (x : X), f (x, y) < a}

Let f take values in a complete linear order. If its strict sublevel is measurable on the product of a standard Borel space and a Polish Borel space, then the corresponding strict sublevel of the pointwise infimum over the first factor is analytic. This is the measurable-projection principle used by infimal transforms.

theorem TauCeti.MeasureTheory.AnalyticSet.nullMeasurableSet {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {S : Set X} (hS : MeasureTheory.AnalyticSet S) (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] : MeasureTheory.NullMeasurableSet S μ

Lusin's universal-measurability theorem. An analytic subset of a metrizable space is null-measurable with respect to every s-finite measure on a measurable space containing the Borel sets, equivalently measurable in the completion of that measure.

theorem TauCeti.MeasureTheory.NullMeasurableSet.of_generateFrom_analyticSet {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {S : Set X} (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] (hS : MeasurableSet S) : MeasureTheory.NullMeasurableSet S μ

Every set in the measurable space generated by the analytic subsets of a metrizable space is null-measurable for every s-finite measure on a measurable space containing the Borel sets.

theorem TauCeti.MeasureTheory.nullMeasurable_of_measurable_generateFrom_analyticSet {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {A : Type u_2} [MeasurableSpace A] {g : X → A} (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] (hg : Measurable g) : MeasureTheory.NullMeasurable g μ

A function measurable for the measurable space generated by analytic sets is null-measurable for every s-finite measure on a measurable space containing the Borel sets.