Choquet capacity: definition and instance on finite Borel measures

Defines the compact capacity functional and the bundled IsChoquetCapacity structure. Proves that every finite Borel measure on a Polish space is a Choquet 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.

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

Bundled record of the three Choquet capacity axioms: monotonicity, sequential continuity from below along increasing unions, and sequential continuity from above along decreasing intersections of closed sets. The third axiom distinguishes a capacity from a general outer measure.

• 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)

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.