2.2 Choquet capacity

Definition 2.3 Choquet capacity

Lean: MeasureTheory.IsChoquetCapacity

A map \(I : \mathrm{Set}(\alpha ) \to \mathbb {R}_{\ge 0}^\infty \) is a Choquet capacity iff (i) it is monotone, (ii) continuous from below along increasing sequences, and (iii) continuous from above along antitone sequences of closed sets [ 6 ] , [ 14 , Defn 30.1 ] , [ 8 , III.1 ] . Every finite Borel measure on a Polish space is a Choquet capacity.

Definition 2.4 Compact capacity hull

Lean: MeasureTheory.compactCap

For \(\mu \) and \(S\) as above,

\[ \mathrm{compactCap}\, \mu \, S \; :=\; \sup \{ \mu (K) : K \subseteq S,\; K \text{ compact} \} . \]

Theorem 2.5 Every finite Borel measure is a Choquet capacity

Lean: MeasureTheory.measure_isChoquetCapacity

Every finite Borel measure on a Polish space satisfies the three axioms of Definition 2.3 [ 8 , III.7 ] , [ 14 , Thm 17.11 ] .

Theorem 2.6 Monotonicity of compactCap

Lean: MeasureTheory.compactCap_mono

\(S \subseteq T \Rightarrow \mathrm{compactCap}\, \mu \, S \le \mathrm{compactCap}\, \mu \, T\).

Theorem 2.7 Measurable inner approximation

Lean: MeasureTheory.MeasurableSet_compactCap_eq

If \(S\) is measurable then \(\mu (S) = \mathrm{compactCap}\, \mu \, S\) [ 14 , Thm 17.11 ] .

Theorem 2.8 Kechris 30.13: analytic capacitability

Lean: MeasureTheory.AnalyticSet.cap_eq_iSup_isCompact

Let \(I\) be a Choquet capacity on a Polish space \(\alpha \), and \(S\) an analytic subset of \(\alpha \). Then

\[ I(S) \; =\; \sup \{ I(K) : K \subseteq S,\; K \text{ compact} \} \]

[ 14 , Thm 30.13 ] , [ 6 ] , [ 8 , III.29–III.33 ] . Together with Definition 2.4 and Theorem 2.5, this specializes to \(\mu (S) = \mathrm{compactCap}\, \mu \, S\).

Theorem 2.9 Analytic compact-hull equality

Lean: MeasureTheory.AnalyticSet.compactCap_eq

For analytic \(S\), \(\mu (S) = \mathrm{compactCap}\, \mu \, S\). Corollary of Theorem 2.8 [ 14 , Thm 30.13 ] .