Carathéodory's extension theorem

Let C be a semiring of sets and m an additive content on C, which is sigma-subadditive. Then all sets in the sigma-algebra generated by C are Carathéodory measurable with respect to the outer measure induced by m. The induced outer measure is equal to m on C.

Main declarations

• MeasureTheory.AddContent.measureCaratheodory: Construct a measure from a sigma-subadditive function on a semiring. This measure is defined on the associated Carathéodory sigma-algebra.
• MeasureTheory.AddContent.measure: Construct a measure from a sigma-subadditive content on a semiring, assuming the semiring generates a given measurable structure. The measure is defined on this measurable structure.

Main results

• MeasureTheory.AddContent.inducedOuterMeasure_eq: The outer measure induced by a sigma-subadditive content on a semiring is equal to the content on the sets of the semiring.
• MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure_of_mem: all sets of the semiring are Carathéodory measurable with respect to the outer measure induced by a sigma-subadditive content.
• MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure: all sets of the sigma-algebra generated by the semiring are Carathéodory measurable with respect to the outer measure induced by a sigma-subadditive content.
• MeasureTheory.AddContent.measureCaratheodory_eq: The measure MeasureTheory.AddContent.measureCaratheodory generated from an m : AddContent C on a IsSetSemiring C coincides with m on C.
• MeasureTheory.AddContent.measure_eq: The measure defined through a sigma-subadditive content on a semiring coincides with the content on the semiring.

theorem MeasureTheory.AddContent.ofFunction_eq {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : IsSetSemiring C) (m : AddContent ENNReal C) (m_sigma_subadd : m.IsSigmaSubadditive) (m_top : ∀ s ∉ C, m s = ⊤) (hs : s ∈ C) : (OuterMeasure.ofFunction ⇑m ⋯) s = m s

For m : AddContent C sigma-sub-additive, finite on C, the OuterMeasure given by m coincides with m on C.

theorem MeasureTheory.AddContent.inducedOuterMeasure_eq {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : IsSetSemiring C) (m : AddContent ENNReal C) (m_sigma_subadd : m.IsSigmaSubadditive) (hs : s ∈ C) : (inducedOuterMeasure (fun (x : Set α) (x_1 : x ∈ C) => m x) ⋯ ⋯) s = m s

For m : AddContent C sigma-sub-additive, finite on C, the inducedOuterMeasure given by m coincides with m on C.

theorem MeasureTheory.AddContent.isCaratheodory_ofFunction_of_mem {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : IsSetSemiring C) (m : AddContent ENNReal C) (m_top : ∀ s ∉ C, m s = ⊤) (hs : s ∈ C) : (OuterMeasure.ofFunction ⇑m ⋯).IsCaratheodory s

theorem MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure_of_mem {α : Type u_1} {C : Set (Set α)} (hC : IsSetSemiring C) (m : AddContent ENNReal C) {s : Set α} (hs : s ∈ C) : (inducedOuterMeasure (fun (x : Set α) (x_1 : x ∈ C) => m x) ⋯ ⋯).IsCaratheodory s

Every s ∈ C for an m : AddContent C with IsSetSemiring C is Carathéodory measurable with respect to the inducedOuterMeasure from m.

theorem MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure {α : Type u_1} {C : Set (Set α)} (hC : IsSetSemiring C) (m : AddContent ENNReal C) (s : Set α) (hs : MeasurableSet s) : (inducedOuterMeasure (fun (x : Set α) (x_1 : x ∈ C) => m x) ⋯ ⋯).IsCaratheodory s

noncomputable def MeasureTheory.AddContent.measureCaratheodory {α : Type u_1} {C : Set (Set α)} (m : AddContent ENNReal C) (hC : IsSetSemiring C) (m_sigma_subadd : m.IsSigmaSubadditive) : Measure α

Construct a measure from a sigma-subadditive content on a semiring. This measure is defined on the associated Carathéodory sigma-algebra.

Equations

• m.measureCaratheodory hC m_sigma_subadd = { toOuterMeasure := MeasureTheory.inducedOuterMeasure (fun (x : Set α) (x_1 : x ∈ C) => m x) ⋯ ⋯, m_iUnion := ⋯, trim_le := ⋯ }

theorem MeasureTheory.AddContent.measureCaratheodory_eq_inducedOuterMeasure {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : IsSetSemiring C) (m : AddContent ENNReal C) (m_sigma_subadd : m.IsSigmaSubadditive) : (m.measureCaratheodory hC m_sigma_subadd) s = (inducedOuterMeasure (fun (x : Set α) (x_1 : x ∈ C) => m x) ⋯ ⋯) s

The measure MeasureTheory.AddContent.measureCaratheodory generated from an m : AddContent C on a IsSetSemiring C coincides with the MeasureTheory.inducedOuterMeasure.

theorem MeasureTheory.AddContent.measureCaratheodory_eq {α : Type u_1} {C : Set (Set α)} {s : Set α} (m : AddContent ENNReal C) (hC : IsSetSemiring C) (m_sigma_subadd : m.IsSigmaSubadditive) (hs : s ∈ C) : (m.measureCaratheodory hC m_sigma_subadd) s = m s

noncomputable def MeasureTheory.AddContent.measure {α : Type u_1} {C : Set (Set α)} [mα : MeasurableSpace α] (m : AddContent ENNReal C) (hC : IsSetSemiring C) (hC_gen : mα ≤ MeasurableSpace.generateFrom C) (m_sigma_subadd : m.IsSigmaSubadditive) : Measure α

Construct a measure from a sigma-subadditive content on a semiring, assuming the semiring generates a given measurable structure. The measure is defined on this measurable structure.

Equations

• m.measure hC hC_gen m_sigma_subadd = (m.measureCaratheodory hC m_sigma_subadd).trim ⋯

theorem MeasureTheory.AddContent.measure_eq {α : Type u_1} {C : Set (Set α)} {s : Set α} [mα : MeasurableSpace α] (m : AddContent ENNReal C) (hC : IsSetSemiring C) (hC_gen : mα = MeasurableSpace.generateFrom C) (m_sigma_subadd : m.IsSigmaSubadditive) (hs : s ∈ C) : (m.measure hC ⋯ m_sigma_subadd) s = m s

The measure defined through a sigma-subadditive content on a semiring coincides with the content on the semiring.