Analytic sets are universally measurable (Choquet capacitability)

This module discharges the single classical measure-theoretic residual of the singular ("issue #6") multiplicative ergodic theorem: every analytic set in a standard Borel space is NullMeasurableSet for every s-finite (SFinite) measure — the classical universal-measurability theorem of Lusin, obtained via Choquet's capacitability theorem. (SFinite covers in particular every finite and σ-finite measure, hence every probability measure.)

Mathlib provides the analytic-set construction (MeasureTheory.AnalyticSet) and the Lusin separation / Suslin theorems (AnalyticSet.measurablySeparable, AnalyticSet.measurableSet_of_compl), but not universal measurability: Suslin's theorem needs the complement to be analytic too, which a Borel projection does not satisfy. The capacitability route used here needs no analytic complement.

The route

For a finite Borel measure μ on a Polish space, the compact capacity compactCap μ s = sSup {μ K | K compact, K ⊆ s} agrees with μ s on analytic sets — this is Choquet's capacitability theorem (AnalyticSet.compactCap_eq). The proof parametrises the analytic set as f(ℕ → ℕ) for continuous f, builds a coordinate-bound sequence N : ℕ → ℕ by induction (each coordinate via continuity of the capacity along increasing unions), and identifies the decreasing intersection of closures of cylinder images with the compact image f '' Bnd N (iInter_closure_image_cyl_eq, a truncation + sequential-compactness argument). See Kechris, Classical Descriptive Set Theory, Theorem 30.13.

From compactCap μ s = μ s (μ finite) an increasing union B of compact subsets of s has μ B = μ s < ∞; Carathéodory splitting μ s = μ B + μ (s \ B) then forces μ (s \ B) = 0, so s =ᵐ[μ] B with B Borel: NullMeasurableSet s μ (AnalyticSet.nullMeasurableSet_of_finite). The general s-finite case follows by dominating μ with a finite measure (AnalyticSet.nullMeasurableSet).

Main results

• MeasureTheory.IsChoquetCapacity: the three Choquet-capacity axioms.
• MeasureTheory.measure_isChoquetCapacity: finite Borel measures on Polish spaces are capacities.
• MeasureTheory.AnalyticSet.cap_eq_iSup_isCompact: Choquet's capacitability theorem (abstract).
• MeasureTheory.AnalyticSet.compactCap_eq: for analytic sets, compact capacity = measure.
• MeasureTheory.AnalyticSet.nullMeasurableSet_of_finite: an analytic set is NullMeasurableSet for every finite measure.
• MeasureTheory.AnalyticSet.nullMeasurableSet: the deliverable — an analytic set is NullMeasurableSet for every s-finite (SFinite) measure.

References

• G. Choquet, Theory of capacities, Annales de l'Institut Fourier 5 (1954), 131–295.
• A. S. Kechris, Classical Descriptive Set Theory, Theorem 30.13.
• S. M. Srivastava, A Course on Borel Sets, Theorem 4.3.1.

The Choquet-capacity infrastructure (definitions, measure_isChoquetCapacity, cap_eq_iSup_isCompact, compactCap_eq and their helper lemmas) is adapted from the formal-learning-theory-kernel project by Dhruv Gupta, an explicitly Mathlib-candidate file.

Compact capacity

noncomputable def MeasureTheory.compactCap {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] (μ : Measure α) (s : Set α) : ENNReal

Compact capacity of a set s relative to a measure μ: the supremum of μ K over compact subsets K ⊆ s. The inner-regularity functional whose equality with μ s characterises measurability for analytic sets.

Equations

• MeasureTheory.compactCap μ s = sSup {r : ENNReal | ∃ (K : Set α), IsCompact K ∧ K ⊆ s ∧ r = μ K}

theorem MeasureTheory.compactCap_mono {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : Measure α} {s t : Set α} (hst : s ⊆ t) : compactCap μ s ≤ compactCap μ t

Compact capacity is monotone in its set argument: enlarging s enlarges the family of compact subsets and so the supremum.

Choquet capacity structure

structure MeasureTheory.IsChoquetCapacity {α : Type u_1} [TopologicalSpace α] (cap : Set α → ENNReal) : Prop

Bundled record of the three Choquet capacity axioms for a functional cap : Set α → ℝ≥0∞: monotonicity, sequential continuity from below along increasing unions, and sequential continuity from above along decreasing intersections of closed sets. The third axiom is what distinguishes a capacity from a general outer measure; it is the asymmetry that makes the capacitability theorem possible. Every finite Borel measure on a Polish space is a Choquet capacity (measure_isChoquetCapacity).

• mono {s t : Set α} : s ⊆ t → cap s ≤ cap t

  A capacity is monotone in its set argument.

• iUnion_nat (f : ℕ → Set α) : Monotone f → cap (⋃ (n : ℕ), f n) = ⨆ (n : ℕ), cap (f n)

  A capacity is continuous from below along increasing unions.

• iInter_closed (f : ℕ → Set α) : Antitone f → (∀ (n : ℕ), IsClosed (f n)) → cap (⋂ (n : ℕ), f n) = ⨅ (n : ℕ), cap (f n)

  A capacity is continuous from above along decreasing intersections of closed sets.

Finite Borel measures on Polish spaces are Choquet capacities

theorem MeasureTheory.measure_isChoquetCapacity {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [PolishSpace α] (μ : Measure α) [IsFiniteMeasure μ] : IsChoquetCapacity fun (s : Set α) => μ s

Every finite Borel measure on a Polish space is a Choquet capacity. Monotonicity and the increasing-union axiom are immediate from measure_mono and measure_iUnion; the decreasing-closed-intersection axiom uses Mathlib's Antitone.measure_iInter for finite measures on closed sets. The instance that lets the abstract capacitability machinery be applied to ordinary probability measures.

Measurable sets: compact capacity = measure

theorem MeasureTheory.MeasurableSet.compactCap_eq {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [PolishSpace α] {μ : Measure α} [IsFiniteMeasure μ] {s : Set α} (hs : MeasurableSet s) : compactCap μ s = μ s

For Borel-measurable sets, compactCap μ s = μ s. Two-sided bound: monotonicity gives ≤, and the existing inner regularity of finite Borel measures on Polish spaces (MeasurableSet.exists_isCompact_lt_add) gives ≥. The easy half of the capacitability statement; the analytic-set half requires the cylinder construction in the rest of the file.

iSup rewrite of compactCap

Choquet capacitability - infrastructure

Choquet capacitability theorem

theorem MeasureTheory.AnalyticSet.cap_eq_iSup_isCompact {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [PolishSpace α] {cap : Set α → ENNReal} (hcap : IsChoquetCapacity cap) {s : Set α} (hs : AnalyticSet s) : cap s = ⨆ (K : Set α), ⨆ (_ : IsCompact K), ⨆ (_ : K ⊆ s), cap K

Choquet capacitability: for analytic sets, capacity = supremum over compact subsets. Reference: Kechris, Classical Descriptive Set Theory, Theorem 30.13.

The proof parametrises the analytic set as f(ℕ → ℕ) for continuous f, builds N : ℕ → ℕ by induction using iUnion_nat at each coordinate, then uses iInter_closed on the closures of cylinder images and a truncation/compactness argument to show ⋂ closure(f '' Cyl N n) = f '' Bnd N (compact).

Analytic sets: compact capacity = measure

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

For analytic sets and a finite Borel measure on a Polish space, the compact capacity compactCap μ s (the supremum of μ K over compact K ⊆ s) equals μ s. This is the measure-theoretic form of Choquet's capacitability theorem.

From capacitability to null-measurability

theorem MeasureTheory.AnalyticSet.exists_measurableSet_subset_measure_eq {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [PolishSpace α] (μ : Measure α) [IsFiniteMeasure μ] {s : Set α} (hs : AnalyticSet s) : ∃ (B : Set α), MeasurableSet B ∧ B ⊆ s ∧ μ B = μ s

An analytic set in a Polish space has, for every finite Borel measure, a Borel subset of full measure: an increasing union of compact subsets whose measures approach μ s (Choquet capacitability, compactCap_eq).

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

An analytic set is NullMeasurableSet for every finite measure. From Choquet capacitability there is a Borel B ⊆ s with μ B = μ s < ∞; the Carathéodory splitting μ s = μ B + μ (s \ B) then forces μ (s \ B) = 0, so s =ᵐ[μ] B.

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

Analytic sets are universally measurable (the isolated classical residual, now proved). Every analytic set in a standard Borel (Polish) space is NullMeasurableSet with respect to every s-finite (SFinite) measure μ — the classical universal-measurability theorem of Lusin, via Choquet's capacitability theorem.

The finite case is nullMeasurableSet_of_finite. For a general s-finite μ, Mathlib's exists_isFiniteMeasure_absolutelyContinuous supplies a finite measure ν with μ ≪ ν; the finite case gives NullMeasurableSet s ν, and NullMeasurableSet.mono_ac transports it back along μ ≪ ν to NullMeasurableSet s μ. This covers in particular every finite and σ-finite measure, hence every probability measure (such as the measure of the multiplicative ergodic theorem).