Total variation for vector-valued measures

This file contains the definition of variation for any VectorMeasure in an ENormedAddCommMonoid, in particular, any NormedAddCommGroup.

Given a vector-valued measure μ we consider the problem of finding a countably additive function f such that, for any set E, ‖μ(E)‖ ≤ f(E). This suggests defining f(E) as the supremum over partitions {Eᵢ} of E, of the quantity ∑ᵢ, ‖μ(Eᵢ)‖. Indeed any solution of the problem must be not less than this function. It turns out that this function is a measure.

Main definitions

• VectorMeasure.ennrealVariation — the variation as a VectorMeasure X ℝ≥0∞
• VectorMeasure.variation — the variation as a Measure X

References

• [Walter Rudin, Real and Complex Analysis.][Rud87]

theorem MeasureTheory.VectorMeasure.isSigmaSubadditiveSetFun_enorm {X : Type u_1} [MeasurableSpace X] {V : Type u_2} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] (μ : VectorMeasure X V) : IsSigmaSubadditiveSetFun fun (x : Set X) => ‖↑μ x‖ₑ

The norm of a vector measure is σ-subadditive on measurable sets.

noncomputable def MeasureTheory.VectorMeasure.ennrealVariation {X : Type u_1} [MeasurableSpace X] {V : Type u_2} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] (μ : VectorMeasure X V) : VectorMeasure X ENNReal

The variation of a VectorMeasure as an ℝ≥0∞-valued VectorMeasure.

noncomputable def MeasureTheory.VectorMeasure.variation {X : Type u_1} [MeasurableSpace X] {V : Type u_2} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] (μ : VectorMeasure X V) : Measure X

The variation of a VectorMeasure as a Measure.