Analytic sets are NullMeasurableSet

Bridge from analytic sets to null-measurability via Choquet capacity theory. One atomic concept: the AnalyticSet → NullMeasurableSet bridge, consisting of an inner-approximation lemma and the main theorem.

Main results

• MeasureTheory.AnalyticSet.exists_isCompact_measureReal_gt: inner approximation of analytic sets by compacts, in real-valued measure
• MeasureTheory.AnalyticSet.nullMeasurableSet: analytic sets are null-measurable for finite Borel measures on Polish spaces

theorem MeasureTheory.AnalyticSet.exists_isCompact_measureReal_gt {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [PolishSpace α] {μ : Measure α} [IsFiniteMeasure μ] {s : Set α} (hs : AnalyticSet s) (ε : ℝ) : ε > 0 → ∃ (K : Set α), IsCompact K ∧ K ⊆ s ∧ μ.real s < μ.real K + ε

Inner regularity for analytic sets: any analytic subset of a Polish space can be approximated from inside by a compact subset in measure, by any slack ε > 0. Specialisation of Choquet capacitability (Kechris 30.13) to the measure-as-capacity instance.

theorem MeasureTheory.AnalyticSet.nullMeasurableSet {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [PolishSpace α] {μ : Measure α} [IsFiniteMeasure μ] {s : Set α} (hs : AnalyticSet s) : NullMeasurableSet s μ

Analytic sets are null-measurable. For any finite Borel measure on a Polish space, every analytic set is NullMeasurableSet. Proof inner- approximates the analytic set by compacts, takes the union of approximators (a Borel set), and shows the difference is contained in a Borel null set.

This is the abstract bridge that the entire Borel-analytic measurability layer of downstream learning-theory kernels rests on.