Constructing a measure from an outer measure

Given m an outer measure over α, we construct a measure m.toMeasure for a measurable space ms ≤ m.caratheodory, by defining m.toMeasure s = m s when MeasurableSet s.

Main definition

• OuterMeasure.toMeasure: Obtain a measure by giving an outer measure where all sets in the σ-algebra are Carathéodory measurable.

measure, outer measure

noncomputable def MeasureTheory.OuterMeasure.toMeasure {α : Type u_1} [ms : MeasurableSpace α] (m : OuterMeasure α) (h : ms ≤ m.caratheodory) : Measure α

Obtain a measure by giving an outer measure where all sets in the σ-algebra are Carathéodory measurable.

Equations

• m.toMeasure h = MeasureTheory.Measure.ofMeasurable (fun (s : Set α) (x : MeasurableSet s) => m s) ⋯ ⋯

theorem MeasureTheory.le_toOuterMeasure_caratheodory {α : Type u_1} [ms : MeasurableSpace α] (μ : Measure α) : ms ≤ μ.caratheodory

@[simp]

theorem MeasureTheory.toMeasure_toOuterMeasure {α : Type u_1} [ms : MeasurableSpace α] (m : OuterMeasure α) (h : ms ≤ m.caratheodory) : (m.toMeasure h).toOuterMeasure = m.trim

@[simp]

theorem MeasureTheory.toMeasure_apply {α : Type u_1} [ms : MeasurableSpace α] (m : OuterMeasure α) (h : ms ≤ m.caratheodory) {s : Set α} (hs : MeasurableSet s) : (m.toMeasure h) s = m s

theorem MeasureTheory.le_toMeasure_apply {α : Type u_1} [ms : MeasurableSpace α] (m : OuterMeasure α) (h : ms ≤ m.caratheodory) (s : Set α) : m s ≤ (m.toMeasure h) s

theorem MeasureTheory.toMeasure_apply₀ {α : Type u_1} [ms : MeasurableSpace α] (m : OuterMeasure α) (h : ms ≤ m.caratheodory) {s : Set α} (hs : NullMeasurableSet s (m.toMeasure h)) : (m.toMeasure h) s = m s

@[simp]

theorem MeasureTheory.toOuterMeasure_toMeasure {α : Type u_1} [ms : MeasurableSpace α] {μ : Measure α} : μ.toMeasure ⋯ = μ

@[simp]

theorem MeasureTheory.boundedBy_measure {α : Type u_1} [ms : MeasurableSpace α] (μ : Measure α) : OuterMeasure.boundedBy ⇑μ = μ.toOuterMeasure