Vector-valued measures

This file defines vector-valued measures, which are σ-additive functions from a set to an additive monoid M such that it maps the empty set and non-measurable sets to zero. In the case that M = ℝ, we called the vector measure a signed measure and write SignedMeasure α. Similarly, when M = ℂ, we call the measure a complex measure and write ComplexMeasure α (defined in MeasureTheory/Measure/Complex).

Main definitions

• MeasureTheory.VectorMeasure is a vector-valued, σ-additive function that maps the empty and non-measurable sets to zero.
• MeasureTheory.SignedMeasure is a real-valued vector measure.

Implementation notes

We require all non-measurable sets to be mapped to zero in order for the extensionality lemma to only compare the underlying functions for measurable sets.

We use HasSum instead of tsum in the definition of vector measures in comparison to Measure since this provides summability.

Tags

vector measure, signed measure, complex measure

structure MeasureTheory.VectorMeasure (α : Type u_2) [MeasurableSpace α] (M : Type u_3) [AddCommMonoid M] [TopologicalSpace M] : Type (max u_2 u_3)

A vector measure on a measurable space α is a σ-additive M-valued function (for some M an additive monoid) such that the empty set and non-measurable sets are mapped to zero.

• measureOf' : Set α → M

  The measure of sets

• empty' : self.measureOf' ∅ = 0

  The empty set has measure zero

• not_measurable' ⦃i : Set α⦄ : ¬MeasurableSet i → self.measureOf' i = 0

  Non-measurable sets have measure zero

• m_iUnion' ⦃f : ℕ → Set α⦄ : (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Function.onFun Disjoint f) → HasSum (fun (i : ℕ) => self.measureOf' (f i)) (self.measureOf' (⋃ (i : ℕ), f i))

  The measure is σ-additive

@[reducible, inline]

abbrev MeasureTheory.SignedMeasure (α : Type u_2) [MeasurableSpace α] : Type u_2

A SignedMeasure is an ℝ-vector measure.

Equations

• MeasureTheory.SignedMeasure α = MeasureTheory.VectorMeasure α ℝ

@[instance_reducible]

instance MeasureTheory.VectorMeasure.instFunLikeSet {α : Type u_1} {m : MeasurableSpace α} {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] : FunLike (VectorMeasure α M) (Set α) M

Equations

• MeasureTheory.VectorMeasure.instFunLikeSet = { coe := MeasureTheory.VectorMeasure.measureOf', coe_injective := ⋯ }

@[simp]

theorem MeasureTheory.VectorMeasure.coe_mk {α : Type u_1} {m : MeasurableSpace α} {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] (v : Set α → M) (h₁ : v ∅ = 0) (h₂ : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → v i = 0) (h₃ : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Function.onFun Disjoint f) → HasSum (fun (i : ℕ) => v (f i)) (v (⋃ (i : ℕ), f i))) : ⇑{ measureOf' := v, empty' := h₁, not_measurable' := h₂, m_iUnion' := h₃ } = v