Measures on a Borel space, viewed as outer measures

This instructional file explains how Borel regularity of a measure, viewed as an outer measure, is obtained in Mathlib. None of its declarations are used elsewhere in the project.

Let X be a topological space whose measurable structure is the Borel σ-algebra (BorelSpace X), and let μ be a measure on X. Viewing μ as an outer measure (μ.toOuterMeasure, which agrees with μ on every set), we prove:

1. every measurable, equivalently Borel, set is Carathéodory measurable for μ.toOuterMeasure;
2. every subset E ⊆ X is contained in a Borel set F with μ F = μ E.

Together these say that a measure on a Borel space is a Borel regular outer measure.

theorem measurableSet_caratheodory_toOuterMeasure {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {s : Set X} (hs : MeasurableSet s) : MeasurableSet s

Property 1. Every measurable set is Carathéodory measurable for the outer measure associated to a measure μ.

theorem measurableSpace_le_caratheodory {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} : inst✝ ≤ μ.caratheodory

Property 1, restated. The ambient σ-algebra of X is contained in the σ-algebra of Carathéodory-measurable sets of the outer measure μ.toOuterMeasure.

theorem borel_le_caratheodory {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [BorelSpace X] {μ : MeasureTheory.Measure X} : borel X ≤ μ.caratheodory

Every Borel set is Carathéodory measurable for μ.toOuterMeasure; here "Borel" is spelled out as measurability for the σ-algebra borel X generated by the open sets.

theorem exists_borel_superset_measure_eq {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [BorelSpace X] {μ : MeasureTheory.Measure X} (E : Set X) : ∃ (F : Set X), MeasurableSet F ∧ E ⊆ F ∧ μ F = μ E

Property 2. Every subset E of X is contained in a Borel set F with μ F = μ E.