2.1 Analytic measurability

Theorem 2.1 Analytic null-measurability

Lean: MeasureTheory.AnalyticSet.nullMeasurableSet

Let \(\alpha \) be a Polish space, \(\mu \) a finite Borel measure on \(\alpha \), and \(S \subseteq \alpha \) analytic. Then \(S\) is \(\mu \)-null-measurable [ 14 , Thm 29.5 ] , [ 4 , § 7.4.11 ] .

Theorem 2.2 Inner approximation by compacts

Lean: MeasureTheory.AnalyticSet.exists_isCompact_measureReal_gt

Under the hypotheses of Theorem 2.1, for every \(\delta {\gt} 0\) there exists a compact \(K \subseteq S\) with \(\mu (S) - \mu (K) {\lt} \delta \) (in \(\mathbb {R}\)-valued form) [ 14 , Thm 17.11 ] .