Constructing a vector measure from an additive content

Consider a content defined on a semiring of sets. We investigate in this file whether it is possible to extend it to a (countably additive) vector measure on the whole sigma-algebra. We show that this is possible when the content is dominated by a finite measure, see exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom.

def MeasureTheory.VectorMeasure.of_additive_of_le_measure {α : Type u_1} {hα : MeasurableSpace α} {E : Type u_2} [NormedAddCommGroup E] {μ : Measure α} (m : Set α → E) (hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s) [IsFiniteMeasure μ] (h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) (h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0) : VectorMeasure α E

A finitely additive vector measure which is dominated by a finite positive measure is in fact countably additive.

Equations

• MeasureTheory.VectorMeasure.of_additive_of_le_measure m hm h'm h''m = { measureOf' := m, empty' := ⋯, not_measurable' := h''m, m_iUnion' := ⋯ }

theorem MeasureTheory.VectorMeasure.exists_extension_of_isSetRing_of_le_measure_of_dense {α : Type u_1} {hα : MeasurableSpace α} {E : Type u_2} [NormedAddCommGroup E] [CompleteSpace E] {μ : Measure α} [IsFiniteMeasure μ] {C : Set (Set α)} {m : AddContent E C} (hC : IsSetRing C) (hCmeas : ∀ s ∈ C, MeasurableSet s) (hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s) (h'C : ∀ (t : Set α) (ε : ENNReal), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (symmDiff s t) < ε) : ∃ (m' : VectorMeasure α E), (∀ s ∈ C, ↑m' s = m s) ∧ ∀ (s : Set α), ‖↑m' s‖ₑ ≤ μ s

Consider an additive content on a dense ring of sets. Assume that it is dominated by a finite positive measure. Then it extends to a countably additive vector measure.

theorem MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_dense {α : Type u_1} {hα : MeasurableSpace α} {E : Type u_2} [NormedAddCommGroup E] [CompleteSpace E] {μ : Measure α} [IsFiniteMeasure μ] {C : Set (Set α)} {m : AddContent E C} (hC : IsSetSemiring C) (hCmeas : ∀ s ∈ C, MeasurableSet s) (hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s) (h'C : ∀ (t : Set α) (ε : ENNReal), MeasurableSet t → 0 < ε → ∃ s ∈ supClosure C, μ (symmDiff s t) < ε) : ∃ (m' : VectorMeasure α E), (∀ s ∈ C, ↑m' s = m s) ∧ ∀ (s : Set α), ‖↑m' s‖ₑ ≤ μ s

Consider an additive content on a semi-ring of sets whose finite unions are dense. Assume that it is dominated by a finite positive measure. Then it extends to a countably additive vector measure.

theorem MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom {α : Type u_1} {hα : MeasurableSpace α} {E : Type u_2} [NormedAddCommGroup E] [CompleteSpace E] {μ : Measure α} [IsFiniteMeasure μ] {C : Set (Set α)} {m : AddContent E C} (hC : IsSetSemiring C) (hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s) (h'C : hα = MeasurableSpace.generateFrom C) : ∃ (m' : VectorMeasure α E), (∀ s ∈ C, ↑m' s = m s) ∧ ∀ (s : Set α), ‖↑m' s‖ₑ ≤ μ s

Consider an additive content m on a semi-ring of sets C, which is dominated by a finite measure μ. Assume that C generates the sigma-algebra. Then m extends to a countably additive vector measure which is dominated by μ.