Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom

∀ {α : Type u_1} {hα : MeasurableSpace α} {E : Type u_2} [inst : NormedAddCommGroup E] [CompleteSpace E]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {C : Set (Set α)} {m : MeasureTheory.AddContent E C},
  MeasureTheory.IsSetSemiring C →
    (∀ s ∈ C, ‖m s‖ₑ ≤ μ s) →
      hα = MeasurableSpace.generateFrom C → ∃ m', (∀ 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 μ.

Defined in

Mathlib.MeasureTheory.VectorMeasure.AddContent

Cited by

1 results in Mathlib

Foundations

Depth 209 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupCompleteSpaceMeasureTheory.IsFiniteMeasure