Choquet Capacity Theory

Pure measure-theoretic infrastructure for proving analytic sets are universally measurable. This file is independent of learning theory and is a candidate for contribution to Mathlib.

Main definitions and results

• IsChoquetCapacity: abstract Choquet capacity axioms
• measure_isChoquetCapacity: finite Borel measures on Polish spaces are Choquet capacities
• compactCap: compact capacity (sup of measure over compact subsets)
• MeasurableSet.compactCap_eq: on measurable sets, compact capacity = measure
• AnalyticSet.cap_eq_iSup_isCompact: Choquet capacitability theorem
• AnalyticSet.compactCap_eq: for analytic sets, compact capacity = measure

References

• Choquet, "Theory of capacities", Annales de l'Institut Fourier, 1954
• Kechris, "Classical Descriptive Set Theory", Theorem 30.13

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
• iUnion_nat (f : ℕ → Set α) : Monotone f → cap (⋃ (n : ℕ), f n) = ⨆ (n : ℕ), cap (f n)
• iInter_closed (f : ℕ → Set α) : Antitone f → (∀ (n : ℕ), IsClosed (f n)) → cap (⋂ (n : ℕ), f n) = ⨅ (n : ℕ), cap (f n)

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 parametrizes 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, compact capacity = measure.