Analytic Sets are NullMeasurableSet

Bridge from analytic sets to null-measurability via Choquet capacity theory. This file is independent of learning theory and is a candidate for contribution to Mathlib.

Main results

• AnalyticSet.exists_isCompact_measureReal_gt: inner approximation for analytic sets
• analyticSet_nullMeasurableSet: analytic sets are null-measurable for finite Borel measures

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: every analytic subset of a Polish space can be approximated from inside by a compact subset, in measure. For any finite Borel measure μ, any analytic s, and any r < μ.real s, there is a compact K ⊆ s with μ.real K > r. The Choquet capacitability theorem (Kechris 30.13), specialised to the measure-as-capacity instance.

Main theorem: analytic → NullMeasurableSet

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

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

This is the abstract result that the entire Borel-analytic measurability layer of the kernel rests on. The learning-theoretic significance is that the symmetrization bad event, which is analytic in the Borel-parameterized setting, is automatically null-measurable; this is enough to run the symmetrization argument under NullMeasurableSet regularity, sidestepping the stronger MeasurableSet requirement of the existing literature. Candidate for upstream contribution to Mathlib.