Finiteness and regularity of the variation of sums, scalar multiples and densities

The variation |μ| of a vector measure is subadditive, |μ + ν| ≤ |μ| + |ν| and |μ - ν| ≤ |μ| + |ν|, and homogeneous, |c • μ| = ‖c‖ • |μ|. Finiteness of the variation therefore passes to sums and differences.

Regularity passes too, on an R₁ space with its Borel σ-algebra, for example a compact Hausdorff space. If |μ| and |ν| are finite and regular, then so is |μ| + |ν|. The variation of μ + ν or μ - ν is dominated by it, hence absolutely continuous with respect to it, and is therefore regular by MeasureTheory.Measure.AbsolutelyContinuous.regular. Regularity of |c • μ| needs no hypothesis on the space. The variation of a vector measure with density μ.withDensity g B is finite and absolutely continuous with respect to |μ|, so it is regular whenever |μ| is finite and regular. For scalar measures this is the weighted measure g · μ. These are the closure properties used for scalar measures of finite regular variation, which are the dual of the space of continuous functions on a compact Hausdorff space and arise by polarizing positive measures.

Main results

• MeasureTheory.VectorMeasure.isFiniteMeasure_variation_add, MeasureTheory.VectorMeasure.isFiniteMeasure_variation_sub: finite variation is closed under sums and differences.
• MeasureTheory.VectorMeasure.regular_variation_smul: regular variation is closed under scalar multiplication.
• MeasureTheory.VectorMeasure.regular_variation_add, MeasureTheory.VectorMeasure.regular_variation_sub: finite regular variation is closed under sums and differences.
• MeasureTheory.VectorMeasure.regular_variation_withDensity: finite regular variation passes to vector measures with density.

References

• W. Rudin, Real and Complex Analysis, 3rd ed., McGraw-Hill (1987), §6.1 and §6.19.

instance MeasureTheory.VectorMeasure.isFiniteMeasure_variation_add {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] [ContinuousAdd V] {μ ν : VectorMeasure X V} [IsFiniteMeasure μ.variation] [IsFiniteMeasure ν.variation] : IsFiniteMeasure (μ + ν).variation

The sum of two vector measures of finite variation has finite variation.

instance MeasureTheory.VectorMeasure.regular_variation_add {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] [ContinuousAdd V] {μ ν : VectorMeasure X V} [TopologicalSpace X] [BorelSpace X] [R1Space X] [IsFiniteMeasure μ.variation] [IsFiniteMeasure ν.variation] [μ.variation.Regular] [ν.variation.Regular] : (μ + ν).variation.Regular

On an R₁ space with its Borel σ-algebra, the sum of two vector measures of finite regular variation has regular variation.

instance MeasureTheory.VectorMeasure.isFiniteMeasure_variation_sub {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [NormedAddCommGroup V] {μ ν : VectorMeasure X V} [IsFiniteMeasure μ.variation] [IsFiniteMeasure ν.variation] : IsFiniteMeasure (μ - ν).variation

The difference of two vector measures of finite variation has finite variation.

instance MeasureTheory.VectorMeasure.regular_variation_smul {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [NormedAddCommGroup V] {μ : VectorMeasure X V} [TopologicalSpace X] {𝕜 : Type u_3} [NormedField 𝕜] [NormedSpace 𝕜 V] {c : 𝕜} [μ.variation.Regular] : (c • μ).variation.Regular

A scalar multiple of a vector measure of regular variation has regular variation.

instance MeasureTheory.VectorMeasure.regular_variation_sub {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [NormedAddCommGroup V] {μ ν : VectorMeasure X V} [TopologicalSpace X] [BorelSpace X] [R1Space X] [IsFiniteMeasure μ.variation] [IsFiniteMeasure ν.variation] [μ.variation.Regular] [ν.variation.Regular] : (μ - ν).variation.Regular

On an R₁ space with its Borel σ-algebra, the difference of two vector measures of finite regular variation has regular variation.

instance MeasureTheory.VectorMeasure.regular_variation_withDensity {X : Type u_1} [MeasurableSpace X] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {g : X → E} {B : E →L[ℝ] F →L[ℝ] G} [TopologicalSpace X] [BorelSpace X] [R1Space X] [IsFiniteMeasure μ.variation] [μ.variation.Regular] : (μ.withDensity g B).variation.Regular

On an R₁ space with its Borel σ-algebra, a vector measure with density with respect to a vector measure of finite regular variation has regular variation.