theorem MeasureTheory.OuterMeasure.ofFunction_addContent_eq {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (m : MeasureTheory.AddContent C) (m_sigma_subadd : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → m (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), m (f i)) (m_top : ∀ s ∉ C, m s = ⊤) {s : Set α} (hs : s ∈ C) : (MeasureTheory.OuterMeasure.ofFunction ⇑m ⋯) s = m s

theorem MeasureTheory.inducedOuterMeasure_addContent_of_subadditive {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (m : MeasureTheory.AddContent C) (m_sigma_subadd : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → m (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), m (f i)) {s : Set α} (hs : s ∈ C) : (MeasureTheory.inducedOuterMeasure (fun (x : Set α) (x_1 : x ∈ C) => m x) ⋯ ⋯) s = m s

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

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

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

noncomputable def MeasureTheory.Measure.ofAddContentCaratheodory {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (m : MeasureTheory.AddContent C) (m_sigma_subadd : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → m (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), m (f i)) : MeasureTheory.Measure α

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

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Measure.ofAddContentCaratheodory_eq_inducedOuterMeasure {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (m : MeasureTheory.AddContent C) (m_sigma_subadd : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → m (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), m (f i)) (s : Set α) : (MeasureTheory.Measure.ofAddContentCaratheodory hC m m_sigma_subadd) s = (MeasureTheory.inducedOuterMeasure (fun (x : Set α) (x_1 : x ∈ C) => m x) ⋯ ⋯) s

theorem MeasureTheory.Measure.ofAddContentCaratheodory_eq {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (m : MeasureTheory.AddContent C) (m_sigma_subadd : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → m (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), m (f i)) {s : Set α} (hs : s ∈ C) : (MeasureTheory.Measure.ofAddContentCaratheodory hC m m_sigma_subadd) s = m s

noncomputable def MeasureTheory.Measure.ofAddContent {α : Type u_1} {C : Set (Set α)} [mα : MeasurableSpace α] (hC : MeasureTheory.IsSetSemiring C) (hC_gen : MeasurableSpace.generateFrom C = mα) (m : MeasureTheory.AddContent C) (m_sigma_subadd : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → m (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), m (f i)) : MeasureTheory.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

• MeasureTheory.Measure.ofAddContent hC hC_gen m m_sigma_subadd = (MeasureTheory.Measure.ofAddContentCaratheodory hC m m_sigma_subadd).trim ⋯

theorem MeasureTheory.Measure.ofAddContent_eq {α : Type u_1} {C : Set (Set α)} [mα : MeasurableSpace α] (hC : MeasureTheory.IsSetSemiring C) (hC_gen : MeasurableSpace.generateFrom C = mα) (m : MeasureTheory.AddContent C) (m_sigma_subadd : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → m (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), m (f i)) {s : Set α} (hs : s ∈ C) : (MeasureTheory.Measure.ofAddContent hC hC_gen m m_sigma_subadd) s = m s