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.variation: the variation as a Measure X
• VectorMeasure.ennrealVariation: the variation as a VectorMeasure X ℝ≥0∞

References

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

theorem MeasureTheory.VectorMeasure.isSigmaSubadditiveSetFun_enorm {X : Type u_1} {mX : 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.variation {X : Type u_1} {mX : 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.

Equations

• μ.variation = MeasureTheory.preVariation (fun (x : Set X) => ‖μ x‖ₑ) ⋯ ⋯

noncomputable def MeasureTheory.VectorMeasure.ennrealVariation {X : Type u_1} {mX : 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.

Equations

• μ.ennrealVariation = μ.variation.toENNRealVectorMeasure